Peter B. Andrews

From Wikipedia, the free encyclopedia
(Redirected from Theorem Proving System)

Template:Short description Script error: No such module "Other people". Script error: No such module "Template wrapper".Script error: No such module "Check for conflicting parameters".

Peter Bruce Andrews (November 1, 1937 – April 21, 2025)[1] was an American mathematical logician. He is the creator of the mathematical logic Q0. He also received a patent on bandage for critical wounds.[2]

Theorem Proving System

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

Selected publications

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

  • 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. Template:ISBN. 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. Template:ISBN. Kluwer Academic Publishers, Dordrecht.

References

Page Template:Reflist/styles.css has no content.

  1. ^ Page Module:Citation/CS1/styles.css has no content.Peter Bruce Andrews Obituary, archived from the original on 2025-06-06, retrieved 2025-06-06
  2. ^ Page Template:Citation/styles.css has no content.US granted US11324638B2, Peter B. Andrews, "Bandage which enables examining or treating a wound without removing the adhesive", published Script error: No such module "auto date formatter"., issued Script error: No such module "auto date formatter". 
  3. ^ Page Module:Citation/CS1/styles.css has no content.TPS and ETPS, archived from the original on 2022-03-27, retrieved 2025-06-06
  4. ^ Page Module:Citation/CS1/styles.css has no content.TPS source code, retrieved 2025-06-06
  5. ^ Page Module:Citation/CS1/styles.css has no content.Peter B. Andrews, archived from the original on 2022-01-19, retrieved 2025-06-06

Lua error in package.lua at line 80: module 'Module:Authority control/config' not found.

Template:Asbox