TPS: A Theorem-Proving System for Classical Type Theory

Authors: Andrews P.B.¹; Bishop M.¹; Issar S.²; Nesmith D.³; Pfenning F.⁴; Xi H.¹

Source: Journal of Automated Reasoning, Volume 16, Number 3, June 1996 , pp. 321-353(33)

Publisher: Springer

Buy & download fulltext article:

Price: $47.00 plus tax (Refund Policy)

Abstract:

This is description of {\bf TPS}, a theorem-proving system for classical type theory (Church's typed \lambda -calculus). {\bf TPS} has been designed to be a general research tool for manipulating wffs of first- and higher-order logic, and searching for proofs of such wffs interactively or automatically, or in a combination of these modes. An important feature of {\bf TPS} is the ability to translate between expansion proofs and natural deduction proofs. Examples of theorems that {\bf TPS} can prove completely automatically are given to illustrate certain aspects of {\bf TPS}'s behavior and problems of theorem proving in higher-order logic.

Keywords: higher-order logic; type theory; mating; connection; expansion proof; natural deduction

Language: English

Document Type: Regular paper

Affiliations: 1: Mathematics Department, Carnegie Mellon University, Pittsburgh, PA 15213, U.S.A. e-mail: andrews+@cmu.edu; mbishop@cs.cmu.edu; hwxi@cs.cmu.edu 2: School of Computer Science, Carnegie Mellon University, Pittsburgh, PA 15213, U.S.A. e-mail: si@cmu.edu 3: E-mail: nesmith@infinity.ccsi.com 4: Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA 15213, U.S.A. e-mail: fp+@cs.cmu.edu

Publication date: 1996-06-01