Proof by consistency in conditional equational theories
Eddy Bevers, Johan Lewi · 1991
In this paper we deal with the problem of proving inductive theorems in conditional equational theories. We propose a proof by consistency method that can be employed when the theory is representable as a ground Church-Rosser conditional equational system. The method has a linear proof strategy and is shown to be sound and refutational complete, i.e. it refutes any conditional equation which is not an inductive theorem. Moreover it can handle rewrite rules as well as (unorientable) equations and therefore it will not fail when an unorientable equation comes up (as was the case in the earliest proof by consistency (inductionless induction) methods). The method extends the work on unconditional equational theories of [Bachmair 1988].