Peter B. Andrews

For other people named Peter Andrews, see Peter Andrews (disambiguation).

Peter Bruce Andrews (November 1, 1937 – April 21, 2025)^[6] was an American mathematical logician. He is the creator of the mathematical logic Q₀. He also received a patent on bandage for critical wounds.^[7]

Peter Bruce Andrews
Peter Andrews presenting lecture at IJCAR 2012
Born	(1937-11-01)November 1, 1937 New York City
Died	April 21, 2025(2025-04-21) (aged 87) Burlington, NC
Known for	Q0 (mathematical logic), TPS
Spouse	Catherine Clair “Cate” Andrews
Children	Lyle, Bruce (Tobi)
Parent(s)	Frank Emerson, Edith Lilian Severance[1]
Awards	Herbrand Award, 2003 [2]
Academic background
Education	Ph.D. in Mathematics [3]
Alma mater	Princeton University
Thesis	A Transfinite Type Theory with Type Variables (1964)
Doctoral advisor	Alonzo Church
Academic work
Discipline	Mathematical logic
Sub-discipline	Type theory
Institutions	Carnegie Mellon University [4]
Doctoral students	Frank Pfenning, Dale Miller (academic)
Influenced	Wolfgang Bibel [5]
Website	Peter B. Andrews, archived from the original on 2022-01-19, retrieved 2025-06-06

Theorem Proving System

His research group designed the TPS^[8], an automated theorem proving system for first-order and higher-order logic. A subsystem ETPS of TPS is used to help students learn logic by interactively constructing natural deduction proofs. Source code of TPS is available on the Internet Archive^[9].

Selected Publications

A list is available on his personal web page^[10].

• Andrews, Peter B. (1965). A Transfinite Type Theory with Type Variables. North Holland Publishing Company, Amsterdam.
• Andrews, Peter B. (1971). "Resolution in type theory". Journal of Symbolic Logic 36, 414–432.
• Andrews, Peter B. (1981). "Theorem proving via general matings". J. Assoc. Comput. March. 28, no. 2, 193–214.
• Andrews, Peter B. (1986). An introduction to mathematical logic and type theory: to truth through proof. Computer Science and Applied Mathematics. ISBN 978-0-1205-8535-9. Academic Press, Inc., Orlando, FL.
• Andrews, Peter B. (1989). "On connections and higher-order logic". J. Automat. Reason. 5, no. 3, 257–291.
• Andrews, Peter B.; Bishop, Matthew; Issar, Sunil; Nesmith, Dan; Pfenning, Frank; Xi, Hongwei (1996). "TPS: a theorem-proving system for classical type theory". J. Automat. Reason. 16, no. 3, 321–353.
• Andrews, Peter B. (2002). An introduction to mathematical logic and type theory: to truth through proof. Second edition. Applied Logic Series, 27. ISBN 978-1-4020-0763-7. Kluwer Academic Publishers, Dordrecht.