Peter B. Andrews

Professor of Mathematics
Department of Mathematical Sciences
Carnegie Mellon University
Pittsburgh, Pa. 15213
U.S.A.
412-268-2554 (office)
412-268-2545 (Math. Dept.)
412-268-6380 (Fax to Math. Dept.)
Email: andrews@cmu.edu

Ph.D., Princeton University, 1964. Advisor:Alonzo Church

Students

Herbrand Award, 2003.

Festschrift

An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Second Edition, Kluwer Academic Publishers, now published by Springer, 2002.

Research

My work has been motivated by the desire to help develop tools which will enhance the abilities of humans to reason. I look forward to the eventual formalization of virtually all mathematical, scientific, and technical knowledge, and the development of automated reasoning tools and automated information systems which use automated reasoning to assist in storing, developing, refining, verifying, finding, and applying this knowledge. Logical research will provide intellectual foundations for these developments.

My research has focused on automated deduction and Church's type theory, which is a rich and expressive formulation of higher-order logic in which statements from many disciplines, particularly those involving mathematics, can readily be expressed. The research has been directed toward enabling computers to construct and check proofs of theorems of mathematics and other disciplines formalized in type theory or first-order logic and to assist humans engaged in these tasks.

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.

The research is based on an approach to automated theorem proving involving expansion proofs and matings. Expansion proofs and matings for a theorem represent the essential combinatorial structure of various proofs of the theorem. They can be found by heuristic search, and natural deduction proofs can be constructed from them without further search. A computer implementation of these ideas called TPS (Theorem Proving System) handles theorems of type theory as well as theorems of first-order logic. The system can be used in automatic or interactive mode, and is available to interested parties. It runs in Common Lisp. A subsystem of TPS called ETPS (Educational Theorem Proving System) is used as an interactive aid in logic courses. Research topics include the mathematical theory of matings and expansion proofs, improvements in heuristics used in searching for proofs and constructing elegant proofs, methods of finding appropriate substitutions for higher-order variables, and related questions.


Selected Publications

References are also available in bibtex format.

Burton Dreben, Peter Andrews, and Stal Aanderaa, False Lemmas in Herbrand, Bulletin of the American Mathematical Society 69 (1963), 699-706.

Peter B. Andrews, A Reduction of the Axioms for the Theory of Propositional Types, Fundamenta Mathematicae 52 (1963), 345-350.

Peter B. Andrews, A Transfinite Type Theory with Type Variables, North-Holland Series on Logic and the Foundations of Mathematics, North-Holland Publishing Company (1965), xv + 143 pp.

Peter B. Andrews, On Simplifying the Matrix of a Wff, Journal of Symbolic Logic 33 (1968), 180-192. Archived in JSTOR.

Peter B. Andrews, Resolution with Merging, Journal of the ACM 15 (1968), 367-381.

Peter B. Andrews, Resolution in Type Theory, Journal of Symbolic Logic 36 (1971), 414-432. Reprinted in Reasoning in Simple Type Theory. Festschrift in Honour of Peter B. Andrews on his 70th Birthday. Archived in JSTOR.

Peter B. Andrews, General Models, Descriptions, and Choice in Type Theory Journal of Symbolic Logic 37 (1972), 385-394. Reprinted in Reasoning in Simple Type Theory. Festschrift in Honour of Peter B. Andrews on his 70th Birthday. Archived in JSTOR.

Peter B. Andrews, General Models and Extensionality, Journal of Symbolic Logic 37 (1972), 395-397. Reprinted in Reasoning in Simple Type Theory. Festschrift in Honour of Peter B. Andrews on his 70th Birthday. Archived in JSTOR.

Peter B. Andrews, Resolution and the Consistency of Analysis, Notre Dame Journal of Formal Logic XV (1974), 73-84. Reprinted in Reasoning in Simple Type Theory. Festschrift in Honour of Peter B. Andrews on his 70th Birthday.

Peter B. Andrews, Provability in Elementary Type Theory, Zeitschrift fur Mathematische Logic und Grundlagen der Mathematik 20 (1974), 411-418.

Peter B. Andrews, Refutations by Matings, IEEE Transactions on Computers C-25 (1976), 801-807.

Peter B. Andrews, Transforming Matings into Natural Deduction Proofs, 5th Conference on Automated Deduction, Les Arcs, France, edited by W. Bibel and R. Kowalski, Lecture Notes in Computer Science 87, Springer-Verlag, 1980, 281-292.

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, Dale A. Miller, Eve Longini Cohen, Frank Pfenning, Automating Higher-Order Logic, in Automated Theorem Proving: After 25 Years, edited by W. W. Bledsoe and D. W. Loveland, Contemporary Mathematics series, vol. 29, American Mathematical Society, 1984, 169-192.

Peter B. Andrews, On Connections and Higher-Order Logic, Journal of Automated Reasoning 5 (1989), 257-291. Reprinted in Reasoning in Simple Type Theory. Festschrift in Honour of Peter B. Andrews on his 70th Birthday.

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, More on the Problem of Finding a Mapping between Clause Representation and Natural-Deduction Representation, Journal of Automated Reasoning 7 (1991), 285-286.

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, Carnegie Mellon University Department of Mathematics Research Report 94-166A, February, 1995 (postscript format) (pdf format).

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 16 (1996), 321-353. Reprinted in Reasoning in Simple Type Theory. Festschrift in Honour of Peter B. Andrews on his 70th Birthday.

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

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.

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.

Peter B. Andrews, Classical Type Theory, Chapter 15 of Handbook of Automated Reasoning, edited by Alan Robinson and Andrei Voronkov, Elsevier Science, 2001, Volume 2, 965-1007. You may download this as a postscript or a gzipped postscript file. More Handbook information is here.

Peter B. Andrews, An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Second Edition, Kluwer Academic Publishers, now published by Springer, 2002.

Peter B. Andrews, A Universal Automated Information System for Science and Technology .ps .pdf, Proceedings of the Cade-19 Workshop: Challenges and Novel Applications for Automated Reasoning, edited by Simon Colton, Jeremy Gow, Volker Sorge, and Toby Walsh. Miami, USA, 28th July 2003, 13-18. (Also see Looking Ahead below.)

Peter B. Andrews, Matthew Bishop, Chad E. Brown, Sunil Issar, Frank Pfenning, Hongwei Xi, ETPS: A System to Help Students Write Formal Proofs, Carnegie Mellon University Department of Mathematical Sciences Research Report 03-002, April 2003 (postscript format) (pdf format).

Peter B. Andrews, Herbrand Award Acceptance Speech, Carnegie Mellon University Department of Mathematical Sciences Research Report 03-003, October 2003.

Peter B. Andrews, Herbrand Award Acceptance Speech, Journal of Automated Reasoning 31 (2003), 169-187.

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.

Peter B. Andrews, Some Reflections on Proof Transformations, Mechanizing Mathematical Reasoning: Essays in Honor of Jörg H. Siekmann on the Occasion of His 60th Birthday, D. Hutter and W. Stephan (Eds.), Lecture Notes in Artificial Intelligence 2605, Springer-Verlag, 2005, 14-29.

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, Church's Type Theory, The Stanford Encyclopedia of Philosophy, Edward N. Zalta (ed.), 2006.

Peter B. Andrews and Chad E. Brown, TPS: A Hybrid Automatic-Interactive System for Developing Proofs, Journal of Applied Logic 4 (2006), 367-395.

Peter B. Andrews, Some Historical Reflections, Reasoning in Simple Type Theory. Festschrift in Honour of Peter B. Andrews on his 70th Birthday, edited by Christoph Benzmuller, Chad E. Brown, Jorg Siekmann, and Richard Statman, College Publications, 2008, 3-34.

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, 31-32.

Peter B. Andrews, Looking Ahead, lecture presented to IJCAR 2012, the 6th International Joint Conference on Automated Reasoning, in Manchester, United Kingdom, on June 27, 2012 (postscript format) (pdf format).

Other Information

See the home page for the interdisciplinary doctoral program in Pure and Applied Logic.

Some Useful Links