TPS: A hybrid automatic-interactive system for developing proofs
From MaRDI portal
Publication:865629
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
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
Related Items
Uses Software
Cites Work
- 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
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
