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 03002, 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), 7592.
 Doug Goldson, Steve Reeves & Richard Bornet,
A Review of Several Programs for the Teaching of Logic,
The Computer Journal 36 (1993), 373386
 Doug Goldson & Steve Reeves,
"Using Programs to Teach Logic to Computer Scientists,
Notices of the American Mathematical Society 40 (1993), 143148. (Excerpt:
"The system [ETPS] is robust and has many carefully thoughtout features. Given that it is a "linebased" 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), 321353.

Peter B. Andrews and Chad E. Brown,
TPS: A Hybrid AutomaticInteractive System for Developing Proofs,
Journal of Applied Logic 4 (2006), 367395.
Here are some additional papers related to TPS:
 Peter B. Andrews, Theorem Proving via General Matings,
Journal of the ACM 28 (1981), 193214.
 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, SpringerVerlag, 1982, 5069.
 Peter B. Andrews, On Connections and HigherOrder Logic,
Journal of Automated Reasoning 5 (1989), 257291.
 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, SpringerVerlag, 1990,
641642.
 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 CarlJohan H. Seger, Lecture Notes in Computer Science
780, SpringerVerlag, 1994, 366370.
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 94166A, 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 1517, 1996, edited by Pierangelo Miglioli, Ugo Moscato,
Daniele Mundici, Mario Ornaghi, Lecture Notes in Artificial
Intelligence 1071, Springer, 1996, 115.
SpringerLink
 Peter B. Andrews & Matthew Bishop,
TPS: A Tool for Proving Theorems
Theorem Proving in HigherOrder Logics, 1997, Murray Hill, New Jersey.

Matthew Bishop & Peter B. Andrews,
Selectively Instantiating Definitions,
Automated Deduction  CADE15;
15th International Conference on Automated Deduction,
Lindau, Germany, edited by Claude and Helene Kirchner,
Lecture Notes in Artificial Intelligence 1421, SpringerVerlag, 1998,
365380.
 Matthew Bishop,
A BreadthFirst Strategy for Mating Search,
16th International Conference on Automated Deduction
(CADE16),
edited by Harald Ganzinger, Trento, Italy,
Lecture Notes in Artificial Intelligence 1632, SpringerVerlag,
1999, 359373.
 Matthew Bishop,
Mating Search Without Path Enumeration,
Ph.D. Thesis, Department of Mathematical Sciences, Carnegie Mellon University 1999. (Also available
as Research Report 99223, 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 SpringVerlag),
Automated Deduction  CADE17;
17th International Conference on Automated Deduction,
Pittsburgh, PA, edited by David McAllester,
Lecture Notes in Artificial Intelligence 1831, SpringerVerlag, 2000,
164169.
 Peter B. Andrews & Chad E. Brown,
Tutorial: Using TPS for HigherOrder Theorem Proving and ETPS for Teaching Logic,
Automated Deduction  CADE17;
17th International Conference on Automated Deduction,
Pittsburgh, PA, edited by David McAllester,
Lecture Notes in Artificial Intelligence 1831, SpringerVerlag, 2000,
511512.

Chad E. Brown,
Solving for Set Variables in HigherOrder Theorem Proving
(copyright SpringerVerlag),
Automated Deduction  CADE18; 18th International Conference on Automated Deduction,
Copenhagen, Denmark, edited by Andrei Voronkov,
Lecture Notes in Computer Science 2392, Springer 2002,
408422.
Proceedings of CADE18.
 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 (AAAI05 / IAAI05),
AAAI Press, 2005, 16761677.

Peter B. Andrews and Chad E. Brown,
TPS 3.20080227,
The CADE22 ATP System Competition (CASC22),
edited by Geoff Sutcliffe,
The 22nd International Conference on Automated Deduction, 2009, 3233.
There are more TPSrelated papers on Peter Andrews' page