Jump to content

Peter B. Andrews

From Wikipedia, the free encyclopedia
(Redirected from Theorem Proving System)
For other people named Peter Andrews, see Peter Andrews (disambiguation).
Peter Bruce Andrews
Peter Andrews in 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 Severance Andrews
AwardsHerbrand Award, 2003 [4]
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
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)[5] was an American mathematical logician. He is the creator of the mathematical logic Q0. He also received a patent on bandage for critical wounds.[6]

Theorem Proving System

[edit]

His research group designed the TPS[7], 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[8].

Selected Publications

[edit]

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

  • 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

[edit]
  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). doi:10.1145/182.183.
  4. ^ 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.
  5. ^ Peter Bruce Andrews Obituary, archived from the original on 2025-06-06, retrieved 2025-06-06
  6. ^ 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 
  7. ^ TPS and ETPS, archived from the original on 2022-03-27, retrieved 2025-06-06
  8. ^ TPS source code, retrieved 2025-06-06{{citation}}: CS1 maint: url-status (link)
  9. ^ Peter B. Andrews, archived from the original on 2022-01-19, retrieved 2025-06-06


Flag of United StatesScientist icon

This article about an American mathematician is a stub. You can help Wikipedia by expanding it.

Retrieved from "https://en.wikipedia.org/w/index.php?title=Peter_B._Andrews&oldid=1294354641#Theorem_Proving_System"