TPS: A theorem-proving system for classical type theory

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)

zbMATH Keywords

higher-order logicnatural deductionautomated theorem proverproof checkingtheorem-provinginteractive proof checkersystem TPS for classical type theory

Mathematics Subject Classification ID

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

• Coq
• TPS
• ML
• PVS
• TPTP
• HOL
• ETPS
• Nuprl
• IMPS

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