Proof by consistency (Q1094888)

Advances of the past decade in methods and computer programs for showing consistency of proof systems based on first-order equations have made it feasible, in some settings, to use proof by consistency as an alternative to conventional rules of inference. Musser described the method applied to proof of properties of inductively defined objects. Refinements of this inductionless induction method were discussed by Kapur, Goguen, Huet and Hullot, Huet and Oppen, Lankford, Dershowitz, Paul, and more recently by \textit{J.-P. Jouannaud} and \textit{E. Kounalis} [Inf. Comput. 82, No. 1, 1--33 (1989; Zbl 0682.68032)] as well as by the first author, \textit{P. Narendran} and \textit{H. Zhang} [Automated deduction, Proc. 8th Int. Conf., Oxford/Engl. 1986, Lect. Notes Comput. Sci. 230, 99--117 (1986; Zbl 0642.68034)]. This paper gives a very general account of proof by consistency and inductionless induction, and shows how previous results can be derived simply from the general theory. New results include a theorem giving characterizations of an unambiguity property that is key to applicability of proof by consistency, and a theorem similar to the Birkhoff's completeness theorem for equational proof systems, but concerning inductive proof.