Computer Laboratory, University of Cambridge

- Funded by the EPSRC: Grant reference EP/D070511/1
- Value £92,512; duration October 2006 to October 2007
- Visit Christoph Benzmüller's LEO-II page
- Read the full case for support.
- Project publications
- Poster

- Lawrence C. Paulson (Principal investigator)
- Christoph Benzmüller (Research associate and lead developer)

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 TPTP—set of hard problems, graded by difficulty—will be a natural by-product of this project.

- Christoph Benzmüller, L. C. Paulson, Frank Theiss and Arnaud Fietzke. Progress Report on Leo-II, an Automatic Theorem Prover for Higher-Order Logic.
*In*: Klaus Schneider and Jens Brandt (editors), Theorem Proving in Higher Order Logics 2007 — Emerging Trends. - Christoph Benzmüller, Volker Sorge, Mateja Jamnik, and Manfred Kerber.
Combined Reasoning by Automated Cooperation.
*J. Applied Logic***6**(3) (2008), 318–342. - Christoph Benzmüller and Frank Theiß. Term Indexing for the LEO-II Prover. In Christoph Benzmüller, Bernd Fischer, and Geoff Sutcliffe, editors, 6th International Workshop on the Implementation of Logics, CEUR Workshop Proceedings, Vol. 212, 2006.
- Christoph Benzmüller. Cut Elimination with Xi-Functionality.
*In*: Chris Benzmueller, Chad Brown, Jörg Siekmann and Rick Statman (editors),*Reasoning in Simple Type Theory: Festschrift in Honor of Peter B. Andrews on His 70th Birthday*(College Publications, 2008), 97–114. - Christoph Benzmüller, Geoff Sutcliffe and Florian Rabe. THF0 — The Core TPTP Language for Classical Higher-Order Logic.
*In*: Alessandro Armando, Peter Baumgartner and Gilles Dowek (editors),*IJCAR 2008—Automated Reasoning, 4th International Joint Conference*(Springer LNCS 5195): 491–506 - Christoph Benzmüller and L. C. Paulson
**.**

Exploring Properties of Normal Multimodal Logics in Simple Type Theory with LEO-II.*In*: Chris Benzmueller, Chad Brown, Jörg Siekmann and Rick Statman (editors),*Reasoning in Simple Type Theory: Festschrift in Honor of Peter B. Andrews on His 70th Birthday*(College Publications, 2008), 401–422. - Christoph Benzmüller and L. C. Paulson
**.**

Quantified Multimodal Logics in Simple Type Theory. Logica Universalis (2012). Publisher's version at www.springerlink.com

Lawrence C. Paulson • Computer Laboratory • University of Cambridge