@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ 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 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%