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

Theorem Proving System

His research group designed the

TPS TPS or Tps may refer to: In arts and entertainment *Télévision Par Satellite, a French satellite television company *Third-person shooter, a game genre * Torsonic Polarity Syndrome, in ''South Park'' animation * Trailer Park Sex, a band from ...

, an

automated theorem proving Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a majo ...

system for first-order and

higher-order logic In mathematics and logic, a higher-order logic (abbreviated HOL) is a form of logic that is distinguished from first-order logic by additional quantifiers and, sometimes, stronger semantics. Higher-order logics with their standard semantics are m ...

. A subsystem ETPS of TPS is used to help students learn logic by interactively constructing

natural deduction In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning. This contrasts with Hilbert-style systems, which instead use ...

proofs. Source code of TPS is available on the

Internet Archive The Internet Archive is an American 501(c)(3) organization, non-profit organization founded in 1996 by Brewster Kahle that runs a digital library website, archive.org. It provides free access to collections of digitized media including web ...

Selected Publications

A list is available on his personal web page. *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 The '' Journal of Symbolic Logic'' is a peer-reviewed mathematics journal published quarterly by Association for Symbolic Logic. It was established in 1936 and covers mathematical logic. The journal is indexed by '' Mathematical Reviews'', Zent ...

'' 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. . 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. . Kluwer Academic Publishers, Dordrecht.

References

1937 births 2025 deaths 20th-century American mathematicians 21st-century American mathematicians American logicians Mathematical logicians Carnegie Mellon University faculty Princeton University alumni {{US-mathematician-stub