TPS: A hybrid automatic-interactive system for developing proofs
From MaRDI portal
Publication:865629
first-order logictype theoryhigher-order logicTPSinteractive proofsautomatic proofsautomating mathematicsmathematics assistance systemsemi-automatic proofssemi-interactive proofstheorem proving system
Recommendations
Cites work
- scientific article; zbMATH DE number 1614693 (Why is no real title available?)
- scientific article; zbMATH DE number 1696789 (Why is no real title available?)
- scientific article; zbMATH DE number 3871341 (Why is no real title available?)
- scientific article; zbMATH DE number 1301855 (Why is no real title available?)
- scientific article; zbMATH DE number 194631 (Why is no real title available?)
- scientific article; zbMATH DE number 1863374 (Why is no real title available?)
- scientific article; zbMATH DE number 2090295 (Why is no real title available?)
- scientific article; zbMATH DE number 2090316 (Why is no real title available?)
- scientific article; zbMATH DE number 234014 (Why is no real title available?)
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
- A compact representation of proofs
- A man-machine theorem-proving system
- A unification algorithm for typed \(\bar\lambda\)-calculus
- An introduction to mathematical logic and type theory: To truth through proof.
- Automated deduction - CADE-15. 15th international conference, Lindau, Germany, July 5--10, 1998. Proceedings
- Automated deduction - CADE-16. 16th international conference, Trento, Italy, July 7--10, 1999. Proceedings
- Automated deduction - CADE-18. 18th international conference, Copenhagen, Denmark, July 27--30, 2002. Proceedings
- Classical type theory
- Dissolution
- Eliminating dublication with the hyper-linking strategy
- Gazing: An approach to the problem of definition and lemma use
- Graph-Based Algorithms for Boolean Function Manipulation
- Higher-order semantics and extensionality
- IMPS: An interactive mathematical proof system
- Isabelle. A generic theorem prover
- Model generation for natural language interpretation and analysis.
- On connections and higher-order logic
- Presenting intuitive deductions via symmetric simplification
- Resolution in type theory
- SET-VAR
- Structural analysis of narratives with the Coq proof assistant
- TPS: A theorem-proving system for classical type theory
- The foundation of a generic theorem prover
- Theorem Proving via General Matings
- Unifying Theories in ProofPower-Z
Cited in
(35)- The CADE-28 Automated Theorem Proving System Competition – CASC-28
- The Theorema Environment for Interactive Proof Development
- An overview of the Tecton proof system
- scientific article; zbMATH DE number 1614721 (Why is no real title available?)
- Verifying the modal logic cube is an easy task (for higher-order automated reasoners)
- scientific article; zbMATH DE number 3922016 (Why is no real title available?)
- Iterative dialogues and automated proof.
- scientific article; zbMATH DE number 3878393 (Why is no real title available?)
- Tactic theorem proving with refinement-tree proofs and metavariables
- On the shape of mathematical arguments
- Extensional higher-order paramodulation in Leo-III
- Reducing higher-order theorem proving to a sequence of SAT problems
- scientific article; zbMATH DE number 1765686 (Why is no real title available?)
- Analytic tableaux for higher-order logic with choice
- scientific article; zbMATH DE number 3881901 (Why is no real title available?)
- Quantified multimodal logics in simple type theory
- Limited second-order functionality in a first-order setting
- Automated Reasoning
- Rewriting strategies and strategic rewrite programs
- scientific article; zbMATH DE number 1809864 (Why is no real title available?)
- Hybrid interactive theorem proving using Nuprl and HOL
- Theo: An interactive proof development system
- Analytic tableaux for higher-order logic with choice
- TPS
- One method of constructing a formal system
- Teaching Automated Theorem Proving by Example: PyRes 1.2
- A computer environment for writing ordinary mathematical proofs
- scientific article; zbMATH DE number 4076679 (Why is no real title available?)
- scientific article; zbMATH DE number 1629953 (Why is no real title available?)
- Progress in the Development of Automated Theorem Proving for Higher-Order Logic
- Combining and automating classical and non-classical logics in classical higher-order logics
- Reducing higher-order theorem proving to a sequence of SAT problems
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- IMPS: An interactive mathematical proof system
- \textit{Symlog}. Automated advice in Fitch-style proof construction
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)
