Deciding inductive validity of equations

Abstract

Kapur and Subramaniam [12] 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.