Deciding Inductive Validity of Equations
Jürgen Giesl, Deepak Kapur
Kapur and Subramaniam [CADE-00] 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.