Peter B. Andrews

Peter Bruce Andrews (born 1937) is an American mathematician and Professor of Mathematics, Emeritus at Carnegie Mellon University in Pittsburgh, Pennsylvania,[1] and the creator of the mathematical logic Q0. He received his Ph.D. from Princeton University in 1964 under the tutelage of Alonzo Church.[2] He received the Herbrand Award in 2003.[3] His research group designed the TPS automated theorem prover. A subsystem ETPS (Educational Theorem Proving System) of TPS is used to help students learn logic by interactively constructing natural deduction proofs.

Peter Andrews in 2012

Publications
  • 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.
gollark: It would be more practical to just make a trimmed Linux distro and not just use EFI, but this is cooler.
gollark: It's extremely cool despite lacking some features?
gollark: Thus no discord.
gollark: <@!209142270195138560> CraftOS-EFI can't do HTTP at all.
gollark: I wonder if I could somehow abuse the large, nice and quick-to-refresh display from my ancient kindle thing.

References
  1. "Peter B. Andrews". gtps.math.cmu.edu. Retrieved 2018-03-10.
  2. "Alonzo Church - The Mathematics Genealogy Project". www.genealogy.math.ndsu.nodak.edu. Retrieved 2018-03-10.
  3. 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.


This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.