TPS: A theorem-proving system for classical type theory
type: Item
instance of: scholarly article
title: TPS: A theorem-proving system for classical type theory
zbMATH Open document ID: 0858.03017
DOI: 10.1007/BF00252180
author: Peter B. Andrews
author: Matthew Bishop
author: Sunil Issar
author: Dan Nesmith
author: Frank Pfenning
author: Hongwei Xi
published in: Journal of Automated Reasoning
publication date: 1996-11-25T00:00:00Z
review text: This paper describes the system TPS for classical type theory. TPS can be used as a fully automated theorem prover, or as an interactive proof checker. It accepts problems expressed as formulas in higher-order logic with types. Problems in first-order logic are accepted, but TPS is designed primarily for higher-order logic. The inner inference engine is based on the theory of matings and expansion proofs by P. B. Andrews and D. A. Miller. If the system is used in theorem-proving mode, it searches for an expansion proof of the theorem in a fully automated manner. Since expansion proofs are not readable, the proof is translated automatically into a natural deduction proof, which is displayed to the user. If the system is used in interactive proof-checking mode, the user submits a partial natural deduction proof, and the system verifies the steps and fills the gaps with the assistance of the user. The paper illustrates various functionalities of the system, and a number of examples of proofs produced by TPS in fully automated mode. Since this paper is dedicated to the system, it assumes previous knowledge of the underlying theory, i.e. the matings method and expansion proofs. The reader not familiar with this background is adviced to retrieve first the previous papers [e.g., \textit{P. B. Andrews}, J. Autom. Reasoning 5, No. 3, 257-291 (1989; Zbl 0694.03011)]. Other systems for higher-order logic include LCF, HOL, Nuprl, Coq, Isabelle, and IMPS. References for all these systems are given in the paper. The system PVS [\textit{S. Owre}, \textit{J. M. Rushby} and \textit{N. Shankar}, ``PVS: a prototype verification system'', in: D. Kapur (ed.), Automated Deduction -- CADE-11, Proceedings, Lect. Notes Comput. Sci., Lect. Notes Artif. Intell. 607, 748-752 (1992)] can also be applied to proof verification in higher-order logic.
reviewed by: Maria Paola Bonacina
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03B15
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 934091
zbMATH Keywords: theorem-proving
zbMATH Keywords: proof checking
zbMATH Keywords: system TPS for classical type theory
zbMATH Keywords: automated theorem prover
zbMATH Keywords: interactive proof checker
zbMATH Keywords: higher-order logic
zbMATH Keywords: natural deduction
describes a project that uses: TPS
describes a project that uses: ML
describes a project that uses: Nuprl
describes a project that uses: IMPS
describes a project that uses: Coq
describes a project that uses: ETPS
describes a project that uses: PVS
describes a project that uses: TPTP
describes a project that uses: HOL
MaRDI profile type: Publication
cites work: Resolution in type theory
cites work: Provability in Elementary Type Theory
cites work: Refutations by Matings
cites work: Q3880316
cites work: Theorem Proving via General Matings
cites work: Q4726218
cites work: On connections and higher-order logic
cites work: \({\mathcal Z}\)-match: An inference rule for incrementally elaborating set instantiations
cites work: Gazing: An approach to the problem of definition and lemma use
cites work: Q4692618
cites work: A man-machine theorem-proving system
cites work: SET-VAR
cites work: Set theory in first-order logic: Clauses for Gödel's axioms
cites work: Q3235339
cites work: A formulation of the simple theory of types
cites work: The calculus of constructions
cites work: IMPS: An interactive mathematical proof system
cites work: Theorem proving using equational matings and rigid E -unification
cites work: Edinburgh LCF. A mechanized logic of computation
cites work: Q5287513
cites work: Q4012878
cites work: A unification algorithm for typed \(\overline\lambda\)-calculus
cites work: Q3338232
cites work: A compact representation of proofs
cites work: A theory of type polymorphism in programming
cites work: Q3791114
cites work: The foundation of a generic theorem prover
cites work: Q3338233
cites work: A Machine-Oriented Logic Based on the Resolution Principle
cites work: Q3999539
description: scientific article; zbMATH DE number 934091