Decidable classes of inductive theorems

Abstract

Kapur and Subramaniam [8] 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 of [8] were only restricted to equations. This paper extends the classes of conjectures considered in [8] to a larger class of arbitrary quantifier-free formulas (e.g., conjectures also containing negation, conjunction, disjunction, etc.). © Springer-Verlag Berlin Heidelberg 2001.