TPS: A hybrid automatic-interactive system for developing proofs

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

Peter B. Andrews, Chad Edward Brown

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 logichigher-order logicinteractive proofstype theoryTPSautomatic proofsautomating mathematicsmathematics assistance systemsemi-automatic proofssemi-interactive proofstheorem proving system

Mathematics Subject Classification ID

Related Items

The CADE-28 Automated Theorem Proving System Competition – CASC-28, Extensional higher-order paramodulation in Leo-III, Rewriting Strategies and Strategic Rewrite Programs, Quantified multimodal logics in simple type theory, Analytic tableaux for higher-order logic with choice, Combining and automating classical and non-classical logics in classical higher-order logics, LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description), Analytic Tableaux for Higher-Order Logic with Choice, Progress in the Development of Automated Theorem Proving for Higher-Order Logic, Verifying the Modal Logic Cube Is an Easy Task (For Higher-Order Automated Reasoners), Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems, Limited second-order functionality in a first-order setting, TPS, Reducing higher-order theorem proving to a sequence of SAT problems

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