Papers & Reviews About TPS and ETPS


References are also available in bibtex format.


Brief descriptions of ETPS can be found in these papers:
* Peter B. Andrews, Matthew Bishop, Chad E. Brown, Sunil Issar, Frank Pfenning, Hongwei Xi, ETPS: A System to Help Students Write Formal Proofs (postscript format) (pdf format), Carnegie Mellon University Department of Mathematical Sciences Research Report 03-002, April 2003.
* Peter B. Andrews, Matthew Bishop, Chad E. Brown, Sunil Issar, Frank Pfenning, Hongwei Xi, ETPS: A System to Help Students Write Formal Proofs, Journal of Automated Reasoning 32 (2004), 75-92.
* Doug Goldson, Steve Reeves & Richard Bornet, A Review of Several Programs for the Teaching of Logic, The Computer Journal 36 (1993), 373-386
* Doug Goldson & Steve Reeves, "Using Programs to Teach Logic to Computer Scientists, Notices of the American Mathematical Society 40 (1993), 143-148. (Excerpt: "The system [ETPS] is robust and has many carefully thought-out features. Given that it is a "line-based" system... it is nonetheless a very effective proof tool and surprisingly pleasant to use.")


The following papers provide general descriptions of TPS:
* Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning & Hongwei Xi, TPS: A Theorem Proving System for Classical Type Theory, Journal of Automated Reasoning, Vol. 16, No. 3 (1996), 321-353.
* Peter B. Andrews and Chad E. Brown, TPS: A Hybrid Automatic-Interactive System for Developing Proofs, Journal of Applied Logic 4 (2006), 367-395.


Here are some additional papers related to TPS:
* Peter B. Andrews, Theorem Proving via General Matings, Journal of the ACM 28 (1981), 193-214.
* Dale A. Miller, Eve Longini Cohen & Peter B. Andrews, A Look at TPS, 6th Conference on Automated Deduction, edited by Donald W. Loveland, Lecture Notes in Computer Science 138, Springer-Verlag, 1982, 50-69.
* Peter B. Andrews, On Connections and Higher-Order Logic, Journal of Automated Reasoning 5 (1989), 257-291.
* Peter B. Andrews, Sunil Issar, Dan Nesmith & Frank Pfenning, The TPS Theorem Proving System, 10th International Conference on Automated Deduction, edited by Mark E. Stickel, Lecture Notes in Artificial Intelligence 449, Springer-Verlag, 1990, 641-642.
* Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning & Hongwei Xi, TPS: An Interactive and Automatic Tool for Proving Theorems of Type Theory, Higher Order Logic Theorem Proving and Its Applications, 6th International Workshop, HUG '93, Vancouver, B.C., Canada, August 1993, Proceedings, edited by Jeffrey J. Joyce and Carl-Johan H. Seger, Lecture Notes in Computer Science 780, Springer-Verlag, 1994, 366-370. SpringerLink
* Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi, TPS: A Theorem Proving System for Classical Type Theory (postscript format) (pdf format), Carnegie Mellon University Department of Mathematics Research Report 94-166A, February, 1995.
* Peter B. Andrews & Matthew Bishop, On Sets, Types, Fixed Points, and Checkerboards, Theorem Proving with Analytic Tableaux and Related Methods. 5th International Workshop, TABLEAUX '96, Terrasini, Palermo, Italy, May 15-17, 1996, edited by Pierangelo Miglioli, Ugo Moscato, Daniele Mundici, Mario Ornaghi, Lecture Notes in Artificial Intelligence 1071, Springer, 1996, 1-15. SpringerLink
* Peter B. Andrews & Matthew Bishop, TPS: A Tool for Proving Theorems Theorem Proving in Higher-Order Logics, 1997, Murray Hill, New Jersey.
* Matthew Bishop & Peter B. Andrews, Selectively Instantiating Definitions, Automated Deduction - CADE-15; 15th International Conference on Automated Deduction, Lindau, Germany, edited by Claude and Helene Kirchner, Lecture Notes in Artificial Intelligence 1421, Springer-Verlag, 1998, 365-380.
* Matthew Bishop, A Breadth-First Strategy for Mating Search, 16th International Conference on Automated Deduction (CADE-16), edited by Harald Ganzinger, Trento, Italy, Lecture Notes in Artificial Intelligence 1632, Springer-Verlag, 1999, 359-373.
* Matthew Bishop, Mating Search Without Path Enumeration, Ph.D. Thesis, Department of Mathematical Sciences, Carnegie Mellon University 1999. (Also available as Research Report 99-223, Dept. of Mathematical Sciences, Carnegie Mellon University.)
* Peter B. Andrews, Matthew Bishop & Chad E. Brown, System Description: TPS: A Theorem Proving System for Type Theory (copyright Spring-Verlag), Automated Deduction - CADE-17; 17th International Conference on Automated Deduction, Pittsburgh, PA, edited by David McAllester, Lecture Notes in Artificial Intelligence 1831, Springer-Verlag, 2000, 164-169.
* Peter B. Andrews & Chad E. Brown, Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic, Automated Deduction - CADE-17; 17th International Conference on Automated Deduction, Pittsburgh, PA, edited by David McAllester, Lecture Notes in Artificial Intelligence 1831, Springer-Verlag, 2000, 511-512.
* Chad E. Brown, Solving for Set Variables in Higher-Order Theorem Proving (copyright Springer-Verlag), Automated Deduction - CADE-18; 18th International Conference on Automated Deduction, Copenhagen, Denmark, edited by Andrei Voronkov, Lecture Notes in Computer Science 2392, Springer 2002, 408--422. Proceedings of CADE-18.
* Chad E. Brown, Set Comprehension in Church's Type Theory, Ph.D. Thesis, Department of Mathematical Sciences, Carnegie Mellon University 2004.
* Chad E. Brown, 20 page summary of Ph.D. Dissertation.
* Peter B. Andrews, Proving Theorems of Type Theory Automatically with TPS, Proceedings of the Twentieth National Conference on Artificial Intelligence and the Seventeenth Innovative Applications of Artificial Intelligence Conference (AAAI-05 / IAAI-05), AAAI Press, 2005, 1676-1677.
* Peter B. Andrews and Chad E. Brown, TPS 3.20080227, The CADE-22 ATP System Competition (CASC-22), edited by Geoff Sutcliffe, The 22nd International Conference on Automated Deduction, 2009, 32-33.

There are more TPS-related papers on Peter Andrews' page


PrevTopNextNEW!