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: This has similar issues to the idea of a separate ControversialEsolangs, if less so.
gollark: CGNAT is quite apioform, yes.
gollark: I wonder if some sort of dynamically-switchable channel content warning thing would be remotely doable.
gollark: Also this.
gollark: I mean, if I were being more consistent, which I probably should be, we should maybe... not have rule 4, in its current form? Probably the imagery bit due to things I already outlined, but better methods for handling "textual conversation which makes me uncomfortable" than just not having it which would generalize to other things.

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.