Deciding Inductive Validity of Equations???

Abstract. Kapur and Subramaniam [11] defined syntactical classes of equations where inductive validity can be decided automatically. However, these classes are quite restrictive, since defined function symbols with recursive definitions may only appear on one side of the equations. In this paper, we expand the decidable class of equations significantly by allowing both sides of equations to be expressed using defined function symbols. The definitions of these function symbols must satisfy certain restrictions which can be checked mechanically. These results are crucial to increase the applicability of decision procedures for induction. 1 Introduction Mechanized induction often requires user interaction and is incomplete (provers fail for many valid conjectures). This is especially daunting to an application expert trying to use an induction prover in cases when conjectures are simple. Recently, there has been a surge of interest in the role of decision procedures in tools for reasoning about computations, especially because of the success of BDD-based tools and model checkers in hardware verification. However, because of the above-mentioned challenges in automating induction proofs, such tools lack support for inductive reasoning on recursively defined data structures