Computer Laboratory, University of Cambridge
The proposal is to build a new higher-order automatic theorem prover incorporating the lessons of recent research. The prover will be designed to solve problems of the sort that arise in verification. One design goal is that it should be easy to integrate with interactive verification tools such as HOL and Isabelle. Christoph Benzmüller will visit Cambridge for a year in order to undertake this project.
Automatic theorem provers (ATPs) based on the resolution principle, such as SPASS and Vampire, have reached a high degree of sophistication. They can often find long proofs even for problems having thousands of axioms. However, they are limited to first-order logic. Higher-order logic extends first-order logic with lambda notation for functions and with function and predicate variables. It supports reasoning in set theory, using the obvious representation of sets by predicates. Higher-order logic is a natural language for expressing mathematics, and it is also ideal for formal verification. Moving from first-order to higher-order logic requires a more complicated proof calculus, but it often allows much simpler problem statements. Higher-order logic's built-in support for functions and sets often leads to shorter proofs. Conversely, elementary identities (such as the distributive law for union and intersection) turn into difficult problems when expressed in first-order form.
Interactive verification tools such as Isabelle use higher-order logic. Automatic provers for higher-order logic, however, are rare: the chief ones are TPS and LEO. LEO is still an experimental prototype, while TPS is based on a 20-year-old architecture and can only cope with very small problems. LEO is a self-contained higher-order theorem prover, but can also co-operate with a first-order prover, and this combination has already yielded significant performance improvements. The system attempts to remove higher-order features from the problem so that it can be solved efficiently by a first-order prover. The higher-order prover does not have to duplicate the immensely complicated technologies used in first-order provers. These preliminary experiments demonstrate that the ideas are feasible, but the system requires further development to become generally useful.
First-order theorem provers can be compared through test data drawn from the Thousands of Problems for Theorem Provers (TPTP). A higher-order counterpart of the TPTPset of hard problems, graded by difficultywill be a natural by-product of this project.