TPS: A hybrid automatic-interactive system for developing proofs
From MaRDI portal
Publication:865629
DOI10.1016/J.JAL.2005.10.002zbMATH Open1107.68091OpenAlexW1987549075MaRDI QIDQ865629FDOQ865629
Peter B. Andrews, Chad E. 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
first-order logictype theoryhigher-order logicTPSinteractive proofsautomatic proofsautomating mathematicsmathematics assistance systemsemi-automatic proofssemi-interactive proofstheorem proving system
Cites Work
- An introduction to mathematical logic and type theory: To truth through proof.
- Title not available (Why is that?)
- Title not available (Why is that?)
- IMPS: An interactive mathematical proof system
- Title not available (Why is that?)
- Title not available (Why is that?)
- Graph-Based Algorithms for Boolean Function Manipulation
- Isabelle. A generic theorem prover
- Gazing: An approach to the problem of definition and lemma use
- A unification algorithm for typed \(\bar\lambda\)-calculus
- TPS: A theorem-proving system for classical type theory
- Higher-order semantics and extensionality
- Eliminating dublication with the hyper-linking strategy
- On connections and higher-order logic
- A compact representation of proofs
- Resolution in type theory
- Title not available (Why is that?)
- Unifying Theories in ProofPower-Z
- Title not available (Why is that?)
- Theorem Proving via General Matings
- The foundation of a generic theorem prover
- Structural Analysis of Narratives with the Coq Proof Assistant
- Classical type theory
- Dissolution
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
- Automated deduction - CADE-16. 16th international conference, Trento, Italy, July 7--10, 1999. Proceedings
- SET-VAR
- 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
- A man-machine theorem-proving system
- Model generation for natural language interpretation and analysis.
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Presenting intuitive deductions via symmetric simplification
Cited In (24)
- Title not available (Why is that?)
- Theo: An interactive proof development system
- Extensional higher-order paramodulation in Leo-III
- Progress in the Development of Automated Theorem Proving for Higher-Order Logic
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- On the shape of mathematical arguments
- Iterative dialogues and automated proof.
- Verifying the Modal Logic Cube Is an Easy Task (For Higher-Order Automated Reasoners)
- Analytic Tableaux for Higher-Order Logic with Choice
- Combining and automating classical and non-classical logics in classical higher-order logics
- Teaching Automated Theorem Proving by Example: PyRes 1.2
- Title not available (Why is that?)
- Reducing higher-order theorem proving to a sequence of SAT problems
- Rewriting Strategies and Strategic Rewrite Programs
- Title not available (Why is that?)
- TPS
- Title not available (Why is that?)
- Analytic tableaux for higher-order logic with choice
- Quantified multimodal logics in simple type theory
- Limited second-order functionality in a first-order setting
- The CADE-28 Automated Theorem Proving System Competition – CASC-28
- IMPS: An interactive mathematical proof system
- Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems
- An overview of the Tecton proof system
Uses Software
Recommendations
This page was built for publication: TPS: A hybrid automatic-interactive system for developing proofs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q865629)
