Automatic proofs by induction in theories without constructors

AbstractInductionless induction consists of using pure equational reasoning for proving the validity of an equation in the initial algebra of a set of equational axioms, which would normally require some kind of induction. Under given hypotheses, the equation is valid iff adding it to the set of axioms does not result in an inconsistency. This inconsistency can be found by the Knuth-Bendix completion algorithm, provided that the signature of the algebra is split into free constructors and defined symbols, which must be completely defined in terms of constructors. This is the base of the so-called inductive completion algorithm of Huet and Hullot. Two key concepts, inductive reducibility and inductive co-reducibility, allow us to extend these techniques in various directions: incomplete specifications, nonfree constructors, no constructors specified, equational term rewriting systems. The method is adapted for proving the consistency property of an enrichment of a specification by new operators and new equations. In addition, we get also a simple algorithm to exhibit a set of constructors of a specification. Finally, inductive co-reducibility is reduced to inductive reducibility and an algorithm for deciding inductive reducibility is given for left linear term rewriting systems