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 ...
in
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 Q0. He received his Ph.D. from
Princeton University
Princeton University is a private research university in Princeton, New Jersey. Founded in 1746 in Elizabeth as the College of New Jersey, Princeton is the fourth-oldest institution of higher education in the United States and one of the ...
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 scien ...
. 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 con ...
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 m ...
. 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 ax ...
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'', Zentralb ...
'' 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