×

TPS

swMATH ID: 973
Software Authors: Andrews, Peter B.; Brown, Chad E.
Description: 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).
Homepage: http://gtps.math.cmu.edu/tps-about.html
Keywords: TPS; theorem proving system; automatic proofs; semi-automatic proofs; semi-interactive proofs; interactive proofs; type theory; higher-order logic; first-order logic; automating mathematics; mathematics assistance system
Related Software: TPTP; ETPS; HOL; LEO-II; PVS; Nuprl; Isabelle/HOL; Satallax; E Theorem Prover; VAMPIRE; Coq; Isabelle; Leo; ML; OTTER; IMPS; SPASS; THF0; Sledgehammer; Automath
Referenced in: 75 Publications
all top 5

Referenced by 85 Authors

21 Benzmüller, Christoph Ewald
12 Brown, Chad Edward
7 Paulson, Lawrence Charles
6 Andrews, Peter B.
6 Sutcliffe, Geoff
4 Bishop, Matthew
4 Blanchette, Jasmin Christian
4 Meier, Andreas
4 Siekmann, Jörg H.
3 Farmer, William M.
3 Nipkow, Tobias
3 Sorge, Volker
3 Theiss, Frank
2 Autexier, Serge
2 Backes, Julian
2 Bentkamp, Alexander
2 Fiedler, Armin
2 Franke, Andreas
2 Issar, Sunil
2 Kirchner, Hélène
2 Kohlhase, Michael
2 Libal, Tomer
2 Nesmith, Dan
2 Pfenning, Frank
2 Pollet, Martin
2 Qian, Zhenyu
2 Sultana, Nik
2 Tourret, Sophie
2 Vukmirović, Petar
2 Waldmann, Uwe
2 Xi, Hongwei
1 Aydemir, Brian E.
1 Beeson, Michael J.
1 Belinfante, Johan Gijsbertus Frederik
1 Bohannon, Aaron
1 Corella, Francisco
1 Desharnais, Martin
1 Dietrich, Dominik
1 Dixon, Lucas
1 Fairbairn, Matthew W.
1 Fietzke, Arnaud
1 Fleuriot, Jacques D.
1 Foster, J. Nathan
1 Gabbay, Dov M.
1 Gabbay, Murdoch James
1 Galmiche, Didier
1 Genovese, Valerio
1 Gilmore, Paul C.
1 Guttman, Joshua D.
1 Hess, Stephan M.
1 Hou, Tie
1 Jung, Christoph G.
1 Kaufmann, Matt
1 Kerber, Manfred
1 Kirchner, Claude
1 Kirchner, Florent
1 Konrad, Karsten
1 Kreitz, Christoph
1 Mathijssen, Aad
1 Miglioli, Pierangelo
1 Miller, Dale Allen
1 Moore, J Strother
1 Moscato, Ugo
1 Mundici, Daniele
1 Normann, Immanuel
1 Novák, Vilém
1 Oppenheimer, Paul E.
1 Ornaghi, Mario
1 Pierce, Benjamin C.
1 Prehofer, Christian
1 Pym, David J.
1 Rabe, Florian
1 Rispoli, Daniele
1 Sewell, Peter
1 Shankar, Natarajan
1 Simpson, Carlos Tschudi
1 Smolka, Gert
1 Steen, Alexander
1 Villadsen, Jørgen
1 Vytiniotis, Dimitrios
1 Washburn, Geoffrey
1 Weirich, Stephanie
1 Wirth, Claus-Peter
1 Zalta, Edward N.
1 Zdancewic, Steve

Referencing Publications by Year