TPS
TPS and ETPS are, respectively, the Theorem Proving System and the Educational Theorem Proving System. The former is an automated theorem-prover for first-order logic and type theory. The latter is a cut-down version of TPS intended for use by students; it contains only commands relevant to proving theorems interactively. TPS and ETPS run in Common Lisp, and can be used on any system where Common Lisp runs. TPS and ETPS have been used extensively under Unix and Linux systems, and to some extent under Windows. Potential applications of automated theorem proving include hardware and software verification, partial automation of various mathematical activities, promoting development of formal theories in a wide variety of disciplines, deductive information systems for these disciplines, expert systems which can reason, and certain aspects of artificial intelligence. TPS can be used to prove theorems of first- and higher-order logic interactively, automatically, or in a mixture of these modes, though in automatic mode it is quite primitive in certain respects, such as in dealing with equality. It has facilities for searching for expansion proofs, translating these into natural deduction proofs, constructing natural deduction proofs, translating natural deduction proofs which do not contain cuts into expansion proofs, and solving unification problems in higher-order logic. It has a formula editor which facilitates constructing new formulas from others already known to TPS, and a library facility for saving formulas, definitions, and modes (groups of flag settings).
Keywords for this software
References in zbMATH (referenced in 70 articles , 2 standard articles )
Showing results 1 to 20 of 70.
Sorted by year (- Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar; Waldmann, Uwe: Superposition with lambdas (2019)
- Berger, Ulrich; Hou, Tie: A realizability interpretation of Church’s simple theory of types (2017)
- Benzmüller, Christoph; Sultana, Nik; Paulson, Lawrence C.; Theiß, Frank: The higher-order prover \textscLeo-II (2015)
- Kirchner, Hélene: Rewriting strategies and strategic rewrite programs (2015)
- Libal, Tomer: Regular patterns in second-order unification (2015)
- Benzmüller, Christoph; Paulson, Lawrence C.: Quantified multimodal logics in simple type theory (2013)
- Brown, Chad E.: Reducing higher-order theorem proving to a sequence of SAT problems (2013)
- Sultana, Nik; Blanchette, Jasmin Christian; Paulson, Lawrence C.: LEO-II and Satallax on the Sledgehammer test bench (2013)
- Benzmüller, Christoph; Gabbay, Dov; Genovese, Valerio; Rispoli, Daniele: Embedding and automating conditional logics in classical higher-order logic (2012)
- Backes, Julian; Brown, Chad Edward: Analytic tableaux for higher-order logic with choice (2011)
- Benzmüller, Christoph: Combining and automating classical and non-classical logics in classical higher-order logics (2011)
- Brown, Chad E.: Reducing higher-order theorem proving to a sequence of SAT problems (2011)
- Novák, Vilém: EQ-algebra-based fuzzy type theory and its extensions (2011)
- Oppenheimer, Paul E.; Zalta, Edward N.: Relations versus functions at the foundations of logic: type-theoretic considerations (2011)
- Backes, Julian; Brown, Chad E.: Analytic tableaux for higher-order logic with choice (2010)
- Benzmüller, Christoph: Verifying the modal logic cube is an easy task (for higher-order automated reasoners) (2010)
- Benzmüller, Christoph: Combining logics in simple type theory (2010)
- Benzmüller, Christoph; Paulson, Lawrence C.: Multimodal and intuitionistic logics in simple type theory (2010)
- Blanchette, Jasmin Christian; Nipkow, Tobias: Nitpick: a counterexample generator for higher-order logic based on a relational model finder (2010)
- Gabbay, Murdoch J.; Mathijssen, Aad: A nominal axiomatization of the lambda calculus (2010)