EPSRC logo

Details of Grant 

EPSRC Reference: EP/D070511/1
Title: LEO II: An Effective Higher-Order Theorem Prover
Principal Investigator: Paulson, Professor LC
Other Investigators:
Researcher Co-investigators:
Project Partners:
Department: Computer Laboratory
Organisation: University of Cambridge
Scheme: Standard Research
Starts: 15 October 2006 Ends: 14 October 2007 Value (£): 92,512
EPSRC Research Topic Classifications:
Fundamentals of Computing
EPSRC Industrial Sector Classifications:
No relevance to Underpinning Sectors
Related Grants:
Panel History:  
Summary on Grant Application Form
An Automatic Theorem Prover (ATP) is a piece of software that can prove mathematical statements automatically. Modern ATPs are impressively powerful, often coping with problems that involve thousands of separate facts. ATPs can be applied to practical tasks such as finding faults in computer programs. In general, the use of mathematical logic to analyse computer designs is called formal verification.One limitation of most ATPs concerns the language in which the mathematical statements are expressed. Most ATPs accept first-order logic, which can express assertions about individual items, as in all integers are either even or odd . However, many statements in mathematics are difficult to express in first-order logic, especially if they refer to sets or functions.Higher-order logic resembles first-order logic, but it has built-in notions of sets and functions. It is widely used in formal verification, being especially convenient for expressing assertions about computer hardware designs. Unfortunately, there is only one ATP for higher-order logic; it dates from the 1980s and its performance is poor by modern standards. An experimental higher-order ATP, called LEO, has recently shown promise; in recent work, it has been combined with a conventional ATP so that it can benefit from the latter's high performance.The proposal is to take the ideas recently prototyped in LEO and use them as the basis for a robust new higher-order ATP. It is intended for applications in formal verification, but the project will also shed light on fundamental issues in the mechanization of higher-order logic.
Key Findings
The purpose of this project was to investigate some new ideas for implementing an advanced automatic theorem prover for higher-order logic. Over the course of the year that this project ran, the basic architecture was designed and the theorem prover, entitled LEO-II, was delivered. The appropriateness of this architecture is demonstrated by the high performance of LEO-II compared with other systems of its general type. The key idea is cooperation between systems: LEO-II deals with higher-order elements of a given problem, attempting to reduce it to a first-order problem, whose solution of delegates to an external first-order theorem prover.
Potential use in non-academic contexts
No information has been submitted for this grant.
Impacts
No information has been submitted for this grant.
Sectors submitted by the Researcher
Information & Communication Technologies
Project URL: http://www.ags.uni-sb.de/~leo/index.html
Further Information:  
Organisation Website: http://www.cam.ac.uk