| 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 Science and Technology |
| 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 |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Potential use in non-academic 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.uni-sb.de/~leo/index.html |
| Further Information: |
|
| Organisation Website: |
http://www.cam.ac.uk |