Inductive Theorem Proving Using Refined Unfailing Completion Techniques

We present a brief overview on completion based inductive theorem proving techniques, point out the key concepts for the underlying "proof by consistency" - paradigm and isolate an abstract description of what is necessary for an algorithmic realization of such methods. In particular, we give several versions of proof orderings, which - under certain conditions - are well-suited for that purpose. Together with corresponding notions of (positive and negative) covering sets we get abstract "positive" and "negative" characterizations of inductive validity. As a consequence we can generalize known criteria for inductive validity, even for the cases where some of the conjectures may not be orientable or where the base system is terminating but not necessarily ground confluent. Furthermore we consider several refinements and optimizations of completion based inductive theorem proving techniques. In particular, sufficient criteria for being a covering set including restrictions of critical pairs (and the usage of non-equational inductive knowledge) are discussed. Moreover a couple of lemma generation methods are briefly summarized and classified. A new techniques of save generalization is particularly interesting, since it provides means for syntactic generalizations, i.e. simplifications, of conjectures without loosing semantic equivalence. Finally we present the main features and characteristics of UNICOM, an inductive theorem prover with refined unfailing completion techniques and built on top of TRSPEC, a term rewriting based system for investigating algebraic specifications