Carnegie Mellon University

Peter B. Andrews

Professor Emeritus

8130 Wean Hall
Department of Mathematical Sciences
Mellon College of Science
Carnegie Mellon University
5000 Forbes Avenue
Pittsburgh, PA 15213



Peter Andrews


Ph.D. in Mathematics, Princeton University


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.

Select Publications

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

Andrews, P. (1971). Resolution in Type Theory. Journal of Symbolic Logic, 36, 414-432.

Andrews, P. (1972). General Models, Descriptions, and Choice in Type Theory. Journal of Symbolic Logic, 37, 385-394.

Andrews, P. (1981). Theorem Proving via General Matings. Journal of the ACM, 28, 193-214.

Andrews, P. (1989). On Connections and Higher-Order Logic.  Journal of Automated Reasoning, 5, 257-291.

Andrews, P., Bishop, M., Issar, S., Nesmith, D., Pfenning, F., Xi, H. (1996). TPS: A Theorem Proving System for Classical Type Theory. Journal of Automated Reasoning ,16, 321-353.

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

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

Andrews, P., Bishop, M., Brown, C., Issar, S., Pfenning, F., Xi, H. (2004). ETPS: A System to Help Students Write Formal Proofs. Journal of Automated Reasoning, 32, 75-92.

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

Reasoning in Simple Type Theory. Festschrift in Honor of Peter B. Andrews on His 70th Birthday, edited by Christoph Benzmuller, Chad E. Brown, Jorg Siekmann, and Richard Statman, College Publications, 2008.

Andrews, P. (2014). "A Bit of History Related to Logic Based on Equality", The Life and Work of Leon Henkin. Essays on His Contributions, edited by Maria Manzano and Ildiko Sain and Enrique Alonso. Studies in Universal Logic, Birkhauser, 67-71.