Peter B. Andrews Explained
| Peter Bruce Andrews |
| Birth Date: | 1 November 1937 |
| Birth Place: | New York City |
| Death Place: | Burlington, NC |
| Known For: | Q0 (mathematical logic), TPS |
|
| Spouse: | Catherine Clair “Cate” Andrews |
| Children: | Lyle, Bruce (Tobi) |
| Parents: | Frank Emerson, Edith Lilian Severance[1] |
| Awards: | Herbrand Award, 2003 [2] |
| Education: | Ph.D. in Mathematics [3] |
| Alma Mater: | Princeton University |
| Thesis Title: | A Transfinite Type Theory with Type Variables |
| Thesis Url: | https://archive.org/details/transfinitetypet0000andr/mode/2up |
| Thesis Year: | 1964 |
| Doctoral Advisor: | Alonzo Church |
| Doctoral Students: | |
| Influenced: | Wolfgang Bibel[4] |
Peter Bruce Andrews (November 1, 1937 – April 21, 2025) was an American mathematical logician. He is the creator of the mathematical logic Q0. He also received a patent on bandage for critical wounds.[5]
Theorem Proving System
His research group designed the TPS, 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.
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 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.
Notes and References
- News: Saxon. Wolfgang. 1978-08-09. F. E. ANDREWS DIES; FOUNDATION EXPERT. New York Times. 2025-06-08.
- Andrews. Peter B.. 2003-10-01. Herbrand Award Acceptance Speech. Journal of Automated Reasoning. en. 31. 2. 169–187. 10.1023/b:jars.0000009552.54063.f3. 0168-7433. 10.1.1.69.5121. 9542444.
- Web site: Peter Bruce Andrews - The Mathematics Genealogy Project. 2025-06-06.
- Bibel . Wolfgang . 1983 . Matings in matrices . . 26. 11 . 844–852. 10.1145/182.183 .
- US . US11324638B2 . Peter B. Andrews . . . granted . Bandage which enables examining or treating a wound without removing the adhesive . 2021-05-28 . 2022-05-10 . . . . .
