@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
Name: TPS
Keywords: first-order, higher-order, automatic, semi-automatic, interactive
typed lambda-calculus, expansion proof
Description:
Semantics: ??
Deductive machinery: ??
Dynamics: ??
Persistence: ??
TPS is a theorem proving system for first- and higher-order logic
It can operate in automatic, semi-automatic, or interactive mode.
Logical language is that of the typed lambda-calculus.
Two proving components: search for an expansion proof, and meta language
for defining tactics and constructing natural deduction proofs.
Controlled by settings of over 150 [user settable] flags
Formula editor
Library facility for saving formulas, definitions, and modes.
Peter B. Andrews
On connections and higher-order logic
Journal of Automated Reasoning 5
pp 257--291
1989
Dale A. Miller
A compact representation of proofs
Studia Logica 46
pp. 347--370
1987
Frank Pfenning
Proof Transformations in Higher-Order Logic
PhD Thesis, CMU 1987
Contact persons:
Peter.Andrews@cs.cmu.edu
User group: ??
Pragmatics: ??
Documentation:
Much documentation is available on line
Applications: ??
Extensions/enhancements:
ETPS contains TPS facilites for constructing natrual deduction proofs and
many exercises is available for use in logic courses. Used at CMU
Resource requirements:
Runs in Common Lisp
Has Scribe and Tex interfaces for output of logical and mathematical symbols
Where-to-get-it:
TPS is available by ftp, but it no longer distributed by tape.
Interested persons should contact:
Professor Peter B. Andrews
Mathematics Department
Carnegie Mellon University
Pittsburgh, Pa. 15213-3890
U.S.A.
[Info source/date] CADE 9 + 10 andrews 3/92
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%