Inductive Theorem Proving by Consistency for First‐order Clauses

We show how the method of proof by consistency can be extended to proving \u000Aproperties of the perfect model of a set of first‐order clauses with equality. \u000ATechnically proofs by consistency will be similar to proofs by case analysis \u000Aover the term structure. As our method also allows to prove \u000Asufficient‐completeness of function definitions in parallel with proving an \u000Ainductive theorem we need not distinguish between constructors and defined \u000Afunctions. Our method is linear and refutationally complete with respect to the \u000Aperfect model, it supports lemmas in a natural way, and it provides for \u000Apowerful simplification and elimination techniques