Peter Bruce Andrews (born 1937) is an American

mathematician A mathematician is someone who uses an extensive knowledge of mathematics in their work, typically to solve mathematical problems. Mathematicians are concerned with numbers, data, quantity, structure, space, models, and change. History On ...

and Professor of Mathematics, Emeritus at

Carnegie Mellon University Carnegie Mellon University (CMU) is a private research university in Pittsburgh, Pennsylvania. One of its predecessors was established in 1900 by Andrew Carnegie as the Carnegie Technical Schools; it became the Carnegie Institute of Technology ...

Pittsburgh, Pennsylvania Pittsburgh ( ) is a city in the Commonwealth (U.S. state), Commonwealth of Pennsylvania, United States, and the county seat of Allegheny County, Pennsylvania, Allegheny County. It is the most populous city in both Allegheny County and Wester ...

, and the creator of the mathematical logic Q₀. He received his Ph.D. from

Princeton University Princeton University is a private university, private research university in Princeton, New Jersey. Founded in 1746 in Elizabeth, New Jersey, Elizabeth as the College of New Jersey, Princeton is the List of Colonial Colleges, fourth-oldest ins ...

in 1964 under the tutelage of

Alonzo Church Alonzo Church (June 14, 1903 – August 11, 1995) was an American mathematician, computer scientist, logician, philosopher, professor and editor who made major contributions to mathematical logic and the foundations of theoretical computer scienc ...

. He received the

Herbrand Award The Herbrand Award for Distinguished Contributions to Automated Reasoning is an award given by the Conference on Automated Deduction (CADE), Inc., (although it predates the formal incorporation of CADE) to honour persons or groups for important cont ...

in 2003. His research group designed the TPS

automated theorem prover Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a maj ...

. A subsystem ETPS (Educational Theorem Proving System) of TPS is used to help students learn logic by interactively constructing

natural deduction In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning. This contrasts with Hilbert-style systems, which instead use axiom ...

proofs.

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 The '' Journal of Symbolic Logic'' is a peer-reviewed mathematics journal published quarterly by Association for Symbolic Logic. It was established in 1936 and covers mathematical logic. The journal is indexed by '' Mathematical Reviews'', Zentra ...

'' 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.

References

External links

Peter B. Andrews
1937 births Living people 20th-century American mathematicians 21st-century American mathematicians American logicians Mathematical logicians Carnegie Mellon University faculty Princeton University alumni {{US-mathematician-stub