Some applications of Gentzen’s proof theory in automated deduction. (English) Zbl 1507.03069
Schroeder-Heister, Peter (ed.), Extensions of logic programming. International workshop, Tübingen, FRG, 8–10 December 1989. Proceedings. Berlin etc.: Springer-Verlag. Lect. Notes Comput. Sci. 475, 101-156 (1991).
This paper introduces the GENTZEN theorem-proving program based on Gentzen’s sequent calculus. It is shown to be (nondeterministically) sound and complete for the first-order intuitionistic predicate calculus, and to coincide with Prolog on the Horn clause fragment when considering successful computations.
The paper contains an extensive discussion of Prolog foundations in terms of Gentzen sequents and the associated proof-theoretical background, allowing for improvements on a previous treatment of this subject (by K. A. Bowen [Programming with full first-order logic. New York, NY: School of Computer and Information Sciences, Syracuse University (PhD Thesis) (1980)]). Choices taken in Prolog as far as efficiency is concerned are discussed in terms of this foundational analysis.
The second part introduces GENTZEN as a theorem-proving program written in Prolog (and actually running in Arity Prolog on personal computers). Theoretical properties of the (nondeterministic) program are extensively discussed together with practical examples of problems known to be particularly difficult to express or solve in Prolog or in other theorem-proving programs. The use of GENTZEN as either a theorem-proving program or an extension of Prolog is discussed, and almost 20 annotated references to related work are given.
For the entire collection see [Zbl 0770.68025].
The paper contains an extensive discussion of Prolog foundations in terms of Gentzen sequents and the associated proof-theoretical background, allowing for improvements on a previous treatment of this subject (by K. A. Bowen [Programming with full first-order logic. New York, NY: School of Computer and Information Sciences, Syracuse University (PhD Thesis) (1980)]). Choices taken in Prolog as far as efficiency is concerned are discussed in terms of this foundational analysis.
The second part introduces GENTZEN as a theorem-proving program written in Prolog (and actually running in Arity Prolog on personal computers). Theoretical properties of the (nondeterministic) program are extensively discussed together with practical examples of problems known to be particularly difficult to express or solve in Prolog or in other theorem-proving programs. The use of GENTZEN as either a theorem-proving program or an extension of Prolog is discussed, and almost 20 annotated references to related work are given.
For the entire collection see [Zbl 0770.68025].
Reviewer: Jiří Zlatuška (Brno)
MSC:
| 03B35 | Mechanization of proofs and logical operations |
| 68N17 | Logic programming |
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
