TPS: A theorem-proving system for classical type theory (Q1923825)

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.