EPSRC Reference: 
EP/D070511/1 
Title: 
LEO II: An Effective HigherOrder Theorem Prover 
Principal Investigator: 
Paulson, Professor LC 
Other Investigators: 

Researcher CoInvestigators: 

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 firstorder 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 firstorder logic, especially if they refer to sets or functions.Higherorder logic resembles firstorder logic, but it has builtin 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 higherorder logic; it dates from the 1980s and its performance is poor by modern standards. An experimental higherorder 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 higherorder ATP. It is intended for applications in formal verification, but the project will also shed light on fundamental issues in the mechanization of higherorder logic.

Key Findings 
The purpose of this project was to investigate some new ideas for implementing an advanced automatic theorem prover for higherorder logic. Over the course of the year that this project ran, the basic architecture was designed and the theorem prover, entitled LEOII, was delivered. The appropriateness of this architecture is demonstrated by the high performance of LEOII compared with other systems of its general type. The key idea is cooperation between systems: LEOII deals with higherorder elements of a given problem, attempting to reduce it to a firstorder problem, whose solution of delegates to an external firstorder theorem prover.

Potential use in nonacademic 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.unisb.de/~leo/index.html 
Further Information: 

Organisation Website: 
http://www.cam.ac.uk 