Monday, October 19, 2009

# Mathematics Professor Peter Andrews Honored at the 22nd International Conference on Automated Deduction

In honor of Peter Andrews’ distinguished career, and on the occasion of his 70th birthday, leading scholars in the field of Simple Type Theory contributed to a Festschrift. Andrews’ Festschrift is a collection of papers that includes reprints of eight seminal papers in Simple Type Theory as well as thirteen new articles, which were contributed by Andrews, his students and his collaborators as well as a number of researchers who have been influenced by his work. The book, “Reasoning in Simple Type Theory,” was presented to Andrews, professor of mathematics, at the 22nd International Conference on Automated Deduction (CADE-22) in August at McGill University in Montreal, Canada.

Andrews is widely recognized for his work on automated theorem proving in higher-order logic, which is also known as type theory. Type theory is a versatile and expressive formal language that is particularly well suited to the formalization of mathematics and other disciplines and to specifying and verifying hardware and software.

Over the past 30 years, Andrews and his research assistants have developed an automated theorem proving system called TPS (Theorem Proving System). Theorem proving systems implement knowledge about the structure of theorems and proofs, efficient methods of searching for proofs, and rules of reasoning. TPS proves theorems of first-order logic and higher-order logic interactively, semi-automatically and automatically. Its ability to prove theorems of higher-order logic automatically is unrivaled. In fact, in addition to Andrews receiving a Festschrift at CADE-22, his TPS won first place in the CADE Automated Theorem Proving System Competition in the Typed Higher-order Form demonstration division. This was the first competition between higher-order theorem proving systems ever held. Alumnus Chad Brown, who helped develop TPS, played a key role in setting up TPS for the competition.

The purely interactive facilities of TPS are used in a program called ETPS (Educational Theorem Proving System), which is designed to help students in logic courses construct formal proofs. Since 1983 ETPS has been used by hundreds of students at Carnegie Mellon in certain logic courses, and it has been used at the University of Birmingham in England. Both ETPS and TPS are accessible online.

By: Amy Pavlak