Proof by consistency
type: Item
instance of: scholarly article
title: Proof by consistency
zbMATH Open document ID: 0631.68073
DOI: 10.1016/0004-3702(87)90017-8
author: Deepak Kapur
author: David R. Musser
published in: Artificial Intelligence
publication date: 1987-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03F25
zbMATH DE Number: 4026859
zbMATH Keywords: consistency of proof systems
zbMATH Keywords: first-order equations
zbMATH Keywords: proof by consistency
zbMATH Keywords: inductionless induction
MaRDI profile type: Publication
full work available at URL: 0004-3702(87)90017-8
OpenAlex ID: W2001026998
cites work: Q3880309
cites work: The algebraic specification of abstract data types
cites work: Q5799431
cites work: Q3674088
cites work: Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
cites work: Automatic proofs by induction in theories without constructors
cites work: Final Data Types and Their Specification
cites work: Q3783519
cites work: Q5581665
cites work: Q3687693
cites work: Q3347863
cites work: Final algebra semantics and data type extensions
description: scientific article; zbMATH DE number 4026859