Monday, October 20, 2003

# Carnegie Mellon Professor Peter Andrews Receives Herbrand Award for Advances in Automated Reasoning

PITTSBURGH—Peter Andrews, professor of mathematics at Carnegie Mellon University, received the Herbrand Award for Distinguished Contributions to Automated Reasoning at the 19th International Conference on Automated Deduction in August. The award, which recognizes a lifetime's contribution to this field, cited "his seminal contributions and pioneering research in type theory, mating-based theorem proving, automated deduction in higher-order logic, proof presentation, logic education and his many other contributions to the field of automated reasoning."

Andrews is widely recognized in the field 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.

Andrews' book, "An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof," is the only textbook on type theory.

Research in automated reasoning seeks to develop computer tools that can perform complex reasoning tasks and help people perform such tasks.

Much of the current research on automated reasoning focuses on automated theorem proving. Theorem proving systems implement knowledge about the structure of theorems and proofs, efficient methods of searching for proofs and rules of reasoning.

"Pure reasoning is very abstract, and computers are well suited to such tasks," explains Andrews. The potential applications of automated reasoning are broad, according to Andrews, who works primarily on developing techniques for proving simple mathematical theorems. Automated systems for verifying mathematical proofs could revolutionize publishing in mathematics. Currently, more than 90 percent of a referee's time is spent checking whether proofs in a paper are correct, while only a fraction of the referee's time is spent judging whether a paper is significant, well articulated and worthy of publication. Andrews notes that tools for checking proofs also could be used as research aids by mathematicians trying to prove new theorems.

Computer scientists have been working on applications of automated theorem proving techniques to hardware and software verification for many years. Other potential applications of automated reasoning include incorporating logical deduction into search engines, diagnostic medical programs, and robotics programs.

Over the past 30 years, Andrews and his research assistants have developed an automated theorem proving system called TPS (Theorem Proving System). This computer program 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. Support for this work has come from the National Science Foundation.

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 http://htps.math.cmu.edu:29090/.

The Herbrand Award is named after Jacques Herbrand, a brilliant French mathematician who developed what is now known as Herbrand's Theorem in 1929. Herbrand's Theorem plays a fundamental role in the theoretical foundations of many automated theorem proving systems. It was originally established for first-order logic, but contributions by a number of logicians, including Andrews and his former research assistant Dale Miller, have extended it to higher-order logic, and this work has been fundamental to the theoretical foundations of TPS.

By: Lauren Ward