Peter B. Andrews
Peter Bruce Andrews was an American mathematical logician. He is the creator of the mathematical logic Q0. He also received a patent on bandage for critical wounds.
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.. A Transfinite Type Theory with Type Variables. North Holland Publishing Company, Amsterdam.
- Andrews, Peter B.. "Resolution in type theory". Journal of Symbolic Logic 36, 414–432.
- Andrews, Peter B.. "Theorem proving via general matings". J. Assoc. Comput. March. 28, no. 2, 193–214.
- Andrews, Peter B.. 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.. "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. "TPS: a theorem-proving system for classical type theory". J. Automat. Reason. 16, no. 3, 321–353.
- Andrews, Peter B.. An introduction to mathematical logic and type theory: to truth through proof. Second edition. Applied Logic Series, 27.. Kluwer Academic Publishers, Dordrecht.