The following technical report is available from
http://aib.informatik.rwth-aachen.de/:
Jürgen Giesl and Deepak Kapur
Deciding Inductive Validity of Equations
2003-03
Abstract:
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.
Regards,
Volker
--
http://www-i2.informatik.rwth-aachen.de/stolz/ *** PGP *** S/MIME
rage against the finite state machine
