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 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Potential use in nonacademic contexts 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Impacts 
Description 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk 
Summary 

Date Materialised 


Sectors submitted by the Researcher 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Project URL: 
http://www.ags.unisb.de/~leo/index.html 
Further Information: 

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