Peter B. Andrews
Born in New York City and raised in Tenafly, NJ, Andrews earned his Ph.D. from Princeton University in 1964 under the mentorship of Alonzo Church. He served as a Mathematics Professor at Carnegie Mellon University for 49 years and developed the mathematical logic Q0. In 2003, he was honored with the Herbrand Award. His research team created the TPS automated theorem prover, which includes the ETPS (Educational Theorem Proving System), designed to help students learn logic through interactive natural deduction proofs.
"In my 1978 application to the Mathematics Department at Carnegie Mellon, I mentioned that I had programming experience with LISP. I immediately became Peter's research assistant since he used that language in his theorem-proving project. During my first two weeks as his assistant, Peter gave me three papers to study (by Church, Huet, and himself). These papers were challenging, deep, and, most importantly for Peter's exacting standards, meticulous. I soon learned that the man who would eventually evaluate my Ph.D. dissertation had already found errors in Herbrand's influential Ph.D. thesis and Henkin's paper on general models. Needing to be rigorous with details became a survival strategy in Peter's team that has served me well throughout my career." — Dale Miller
Andrews' math genealogy