TPS: A hybrid automatic-interactive system for developing proofs

DOI10.1016/j.jal.2005.10.002zbMath1107.68091MaRDI QIDQ865629

Chad Edward Brown, Peter B. Andrews

Publication date: 20 February 2007

Published in: Journal of Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jal.2005.10.002

zbMATH Keywords

first-order logic; higher-order logic; interactive proofs; type theory; TPS; automatic proofs; automating mathematics; mathematics assistance system; semi-automatic proofs; semi-interactive proofs; theorem proving system

Mathematics Subject Classification ID

Related Items

TPS, LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)

Uses Software

• Isabelle
• ML
• PVS
• HOL
• ETPS
• Nuprl
• Twelf
• IMPS
• HOT
• Leo
• Lambda-Clam

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Eliminating dublication with the hyper-linking strategy
• On connections and higher-order logic
• A compact representation of proofs
• Gazing: An approach to the problem of definition and lemma use
• A unification algorithm for typed \(\bar\lambda\)-calculus
• Automated deduction - CADE-16. 16th international conference, Trento, Italy, July 7--10, 1999. Proceedings
• SET-VAR
• IMPS: An interactive mathematical proof system
• Isabelle. A generic theorem prover
• Automated deduction - CADE-15. 15th international conference, Lindau, Germany, July 5--10, 1998. Proceedings
• Automated deduction - CADE-18. 18th international conference, Copenhagen, Denmark, July 27--30, 2002. Proceedings
• The foundation of a generic theorem prover
• A man-machine theorem-proving system
• An introduction to mathematical logic and type theory: To truth through proof.
• TPS: A theorem-proving system for classical type theory
• Model generation for natural language interpretation and analysis.
• Structural Analysis of Narratives with the Coq Proof Assistant
• Dissolution
• Graph-Based Algorithms for Boolean Function Manipulation
• Theorem Proving via General Matings
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• Unifying Theories in ProofPower-Z
• Higher-order semantics and extensionality
• Resolution in type theory