Peter B. Andrews

For other people named Peter Andrews, see Peter Andrews (disambiguation).
Peter Bruce Andrews
Peter Andrews presenting lecture at IJCAR 2012
Born(1937-11-01)November 1, 1937
New York City
DiedApril 21, 2025(2025-04-21) (aged 87)
Burlington, NC
Known forQ0 (mathematical logic), TPS
SpouseCatherine Clair “Cate” Andrews
ChildrenLyle, Bruce (Tobi)
Parent(s)Frank Emerson, Edith Lilian Severance[4]
AwardsHerbrand Award, 2003 [5]
Academic background
EducationPh.D. in Mathematics [1]
Alma materPrinceton University
ThesisA Transfinite Type Theory with Type Variables (1964)
Doctoral advisorAlonzo Church
Academic work
DisciplineMathematical logic
Sub-disciplineType theory
InstitutionsCarnegie Mellon University [2]
Doctoral studentsFrank Pfenning, Dale Miller (academic)
InfluencedWolfgang Bibel [3]
WebsitePeter B. Andrews, archived from the original on 2022-01-19, retrieved 2025-06-06

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

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.

References

  1. ^ "Peter Bruce Andrews - The Mathematics Genealogy Project". Retrieved 2025-06-06.
  2. ^ Peter Bruce Andrews Faculty Page, archived from the original on 2024-12-09, retrieved 2025-06-06
  3. ^ Bibel, Wolfgang (1983). "Matings in matrices". Communications of the ACM. 26 (11): 844–852. doi:10.1145/182.183.
  4. ^ Saxon, Wolfgang (1978-08-09). "F. E. ANDREWS DIES; FOUNDATION EXPERT". New York Times. Retrieved 2025-06-08.
  5. ^ Andrews, Peter B. (2003-10-01). "Herbrand Award Acceptance Speech". Journal of Automated Reasoning. 31 (2): 169–187. CiteSeerX 10.1.1.69.5121. doi:10.1023/b:jars.0000009552.54063.f3. ISSN 0168-7433. S2CID 9542444.
  6. ^ Peter Bruce Andrews Obituary, archived from the original on 2025-06-06, retrieved 2025-06-06
  7. ^ US granted US11324638B2, Peter B. Andrews, "Bandage which enables examining or treating a wound without removing the adhesive", published 2021-05-28, issued 2022-05-10 
  8. ^ TPS and ETPS, archived from the original on 2022-03-27, retrieved 2025-06-06
  9. ^ TPS source code, retrieved 2025-06-06
  10. ^ Peter B. Andrews, archived from the original on 2022-01-19, retrieved 2025-06-06


This article is issued from Wikipedia. The text is available under Creative Commons Attribution-Share Alike 4.0 unless otherwise noted. Additional terms may apply for the media files.