TPS: A Theorem-Proving System for Classical Type Theory
Authors: Andrews P.B.1; Bishop M.1; Issar S.2; Nesmith D.3; Pfenning F.4; Xi H.1
Source: Journal of Automated Reasoning, Volume 16, Number 3, June 1996 , pp. 321-353(33)
Publisher: Springer
- Free Content
- New Content
- Subscribed Content
- Free Trial Content
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
- Free Content
- New Content
- Subscribed Content
- Free Trial Content
Click here for Page Help