ETPS swMATH ID: 6302 Software Authors: Peter Andrews, Matthew Bishop, Chad E. Brown, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi 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). The interactive facilities of TPS for constructing natural deduction proofs have been used under the name ETPS in logic courses at Carnegie Mellon for a number of years. Students generally learn to use ETPS fairly quickly just by reading the manual (which contains some complete examples) and playing with the system. The student using ETPS issues commands to apply rules of inference in specified ways, and the computer handles the details of writing the appropriate lines of the proof and checking that the rules can be used in this way. The program thus allows students to concentrate on the essential logical problems underlying the proofs, and it gives them immediate feedback for both correct and incorrect actions. ETPS permits students to work forwards, backwards, or in a combination of these modes, and provides facilities for rearranging proofs, deleting parts of proofs, displaying only those parts of proofs under active consideration, saving incomplete proofs, and printing proofs on paper. The convenient formula editor permits the student to extract needed formulas which occur anywhere in the proof, and build new formulas from them. The rules of inference and predefined problems in ETPS are mostly taken from the textbook: Peter B. Andrews, An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Second Edition, Kluwer Academic Publishers, 2002. Descriptions of the rules of inference are available online. When the teacher permits it, the student can obtain hints from ETPS concerning what to try in various situations. Students can send remarks or questions to the teacher without leaving the program. A record of completed exercises is maintained by ETPS, and can be processed by the GRADER program which is also part of TPS, and which can be used to maintain and process numerical or letter grades for any course. For more information about ETPS, you can download the report ETPS: A System to Help Students Write Formal Proofs (postscript) (pdf). Homepage: http://gtps.math.cmu.edu/tps-about.html Keywords: Educational Theorem Proving Related Software: TPS; Isabelle/HOL; HOL; Isabelle; Nuprl; HOL Light; ML; Coq; IMPS; PVS; TPTP; LEO-II; Haskell; Mizar; E Theorem Prover; Leo; LCF; ACL2; VAMPIRE; Automath Cited in: 161 Publications Standard Articles 2 Publications describing the Software, including 2 Publications in zbMATH Year An introduction to mathematical logic and type theory: To truth through proof. 2nd. ed. Zbl 1002.03002Andrews, Peter B. 2002 An introduction to mathematical logic and type theory: to truth through proof. Zbl 0617.03001Andrews, Peter B. 1986 all top 5 Cited by 169 Authors 22 Novák, Vilém 10 Andrews, Peter B. 9 Benzmüller, Christoph Ewald 9 Murinová, Petra 8 Paulson, Lawrence Charles 7 Farmer, William M. 7 Wolff, Burkhart 6 Brown, Chad Edward 6 Brucker, Achim D. 5 Dowek, Gilles 4 Bishop, Matthew 4 Gallier, Jean H. 4 Kohlhase, Michael 4 Lloyd, John Wylie 4 Snyder, Wayne 3 Aderhold, Markus 3 Blanchette, Jasmin Christian 3 Issar, Sunil 3 Kerber, Manfred 3 Manzano, María 3 Nesmith, Dan 3 Ng, Kee Siong 3 Pfenning, Frank 3 Shankar, Natarajan 3 Sorge, Volker 3 Xi, Hongwei 2 Böhme, Sascha 2 El-Zekey, Moataz Saleh 2 Franke, Andreas 2 Gabbay, Murdoch James 2 Ghilardi, Silvio 2 Haxthausen, Anne Elisabeth 2 Krauss, Alexander 2 Narendran, Paliath 2 Paad, Akbar 2 Purdy, William C. 2 Rabe, Florian 2 Schiemer, Georg 2 Takahara, Yasuhiko 2 Uther, William T. B. 2 Wolfram, David A. 1 Aydemir, Brian E. 1 Baader, Franz 1 Bai, Mino 1 Banach, Richard 1 Beckert, Bernhard 1 Berghofer, Stefan 1 Billingsley, William 1 Blair, Howard A. 1 Bohannon, Aaron 1 Borzyszkowski, Tomasz 1 Brink, Chris 1 Britz, Katarina 1 Broy, Manfred 1 Buchberger, Bruno 1 Chakravarty, Manuel M. T. 1 Chen, Huowang 1 Daum, Matthias 1 De Baets, Bernard 1 Dörrenbächer, Jan 1 Dyba, Martin 1 Fairbairn, Matthew W. 1 Ferbas, Petr 1 Forster, Yannick 1 Foster, J. Nathan 1 Fulop, Sean A. 1 Gengelbach, Arve 1 Gentilini, Paolo 1 Goubault-Larrecq, Jean 1 Guttman, Joshua D. 1 Hähnle, Reiner 1 Hardin, Thérèse 1 Harland, James A. 1 Hasan, Osman 1 He, Xudong 1 Hess, Stephan M. 1 Hu, Baoqing 1 Huertas, Antonia 1 Humberstone, Lloyd 1 Hutter, Marcus 1 Indrzejczak, Andrzej 1 Jafari, Azam 1 Jamnik, Mateja 1 Jeske, Czeslaw 1 Jung, Christoph G. 1 Kahl, Wolfram 1 Kaliszyk, Cezary 1 Kaminski, Mark 1 Katsumata, Shin-ya 1 Kirchner, Claude 1 Klop, Jan Willem 1 Konrad, Karsten 1 Krieg-Brückner, Bernd 1 Kuncak, Viktor 1 Lapierre, Serge 1 Lee, John A. N. 1 Lehmke, Stephan 1 Li, Dafa 1 Li, Zhoujun 1 Lindegaard, Morten P. ...and 69 more Authors all top 5 Cited in 43 Serials 16 Journal of Automated Reasoning 15 Fuzzy Sets and Systems 5 Journal of Logic and Computation 5 Journal of Applied Logic 4 The Journal of Symbolic Logic 4 Information and Computation 3 Notre Dame Journal of Formal Logic 3 Theoretical Computer Science 3 Journal of Symbolic Computation 3 Annals of Mathematics and Artificial Intelligence 3 Logic Journal of the IGPL 3 Lecture Notes in Computer Science 3 Logica Universalis 2 Acta Informatica 2 Studia Logica 2 Formal Aspects of Computing 2 Erkenntnis 1 International Journal of General Systems 1 International Journal of Systems Science 1 International Journal of Theoretical Physics 1 Journal of the Association for Computing Machinery 1 Logique et Analyse. Nouvelle Série 1 Mathematica Slovaca 1 Synthese 1 Bulletin of the Section of Logic 1 Science of Computer Programming 1 History and Philosophy of Logic 1 Annals of Pure and Applied Logic 1 Journal of Computer Science and Technology 1 International Journal of Approximate Reasoning 1 MSCS. Mathematical Structures in Computer Science 1 Formal Methods in System Design 1 Journal of Logic, Language and Information 1 Journal of Applied Non-Classical Logics 1 Journal of Functional Programming 1 The Bulletin of Symbolic Logic 1 Journal of the IGPL 1 The Journal of Functional and Logic Programming 1 Journal of Universal Computer Science 1 Applied Logic Series 1 Logical Methods in Computer Science 1 Journal of Algebra and Related Topics 1 Cognitive Technologies all top 5 Cited in 11 Fields 111 Mathematical logic and foundations (03-XX) 101 Computer science (68-XX) 5 History and biography (01-XX) 5 Order, lattices, ordered algebraic structures (06-XX) 3 General and overarching topics; collections (00-XX) 2 Systems theory; control (93-XX) 1 Combinatorics (05-XX) 1 General algebraic systems (08-XX) 1 Ordinary differential equations (34-XX) 1 Quantum theory (81-XX) 1 Information and communication theory, circuits (94-XX) Citations by Year