Kapur and Subramaniam in their CADE-2000 paper, defined syntactical classes of equations where inductive validity is decidable. Thus, their validity can be checked without any user interaction and hence, this allows an integration of (a restricted form of) induction in fully automated reasoning tools such as model checkers. However, the results in Kapur and Subramaniam's paper were only restricted to equations. This paper extends the classes of conjectures considered in that paper to a larger class of arbitrary quantifier-free formulas (e.g., conjectures also containing negation, conjunction, disjunction, etc.).
To view the entire paper click here