TPS: A theorem-proving system for classical type theory
From MaRDI portal
Publication:1923825
DOI10.1007/BF00252180zbMath0858.03017MaRDI QIDQ1923825
Peter B. Andrews, Dan Nesmith, Hongwei Xi, Frank Pfenning, Sunil Issar, Matthew Bishop
Publication date: 25 November 1996
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
higher-order logicnatural deductionautomated theorem proverproof checkingtheorem-provinginteractive proof checkersystem TPS for classical type theory
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (18)
The higher-order prover \textsc{Leo}-II ⋮ Reduction and unification in lambda calculi with a general notion of subtype ⋮ The CADE-28 Automated Theorem Proving System Competition – CASC-28 ⋮ Mathematical induction in Otter-lambda ⋮ TPS: A hybrid automatic-interactive system for developing proofs ⋮ A proof-centric approach to mathematical assistants ⋮ Computer supported mathematics with \(\Omega\)MEGA ⋮ The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0 ⋮ Combining and automating classical and non-classical logics in classical higher-order logics ⋮ THF0 – The Core of the TPTP Language for Higher-Order Logic ⋮ The seven virtues of simple type theory ⋮ MBase: Representing knowledge and context for the integration of mathematical software systems ⋮ 2004 Annual Meeting of the Association for Symbolic Logic ⋮ Superposition with lambdas ⋮ Superposition with lambdas ⋮ Supra-logic: using transfinite type theory with type variables for paraconsistency ⋮ Proof-search in type-theoretic languages: An introduction ⋮ Lash 1.0 (system description)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- On connections and higher-order logic
- Set theory in first-order logic: Clauses for Gödel's axioms
- A compact representation of proofs
- The calculus of constructions
- Gazing: An approach to the problem of definition and lemma use
- A unification algorithm for typed \(\overline\lambda\)-calculus
- A theory of type polymorphism in programming
- SET-VAR
- \({\mathcal Z}\)-match: An inference rule for incrementally elaborating set instantiations
- IMPS: An interactive mathematical proof system
- Edinburgh LCF. A mechanized logic of computation
- The foundation of a generic theorem prover
- A man-machine theorem-proving system
- Theorem Proving via General Matings
- Provability in Elementary Type Theory
- Refutations by Matings
- Theorem proving using equational matings and rigid E -unification
- A Machine-Oriented Logic Based on the Resolution Principle
- Resolution in type theory
- A formulation of the simple theory of types
This page was built for publication: TPS: A theorem-proving system for classical type theory
