| EPSRC Reference: |
GR/S57198/01 |
| Title: |
Automation for Interactive Proof |
| Principal Investigator: |
Paulson, Professor LC |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science and Technology |
| Organisation: |
University of Cambridge |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
12 January 2004 |
Ends: |
11 May 2007 |
Value (£): |
249,905
|
| 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 |
|
The computer industry would like to eliminate faults in computer hardware and software. One approach to eliminating design errors is to prove the correctness of the design mathematically. As the required proofs are extremely complicated, they are often performed with the help of computer-based proof tools. These tools fall into two categories. (1) Interactive proof tools are expressive, which allows them to capture the most complex designs, but they require much guidance from a skilled user. (2) Theorem provers based on the resolution method are fully automatic, but are restricted to a much simpler formal logic. The project will investigate how to use a resolution prover's sophisticated inference mechanisms to prove the problems that arise during interactive proof. This task will require reconciling the many differences between the logics used by the two types of tool.The project will also develop and evaluate a new architecture for an interactive proof tool. It should run continuously, not waiting for the user to type something. It will run resolution provers in the background, possibly on several processors, attempting to prove any of the outstanding problems. This approach could yield great increases in productivity, particularly for novice users, thereby making interactive proof economic.
|
|
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.cl.cam.ac.uk/research/hvg/isabelle/sledgehammer.html |
| Further Information: |
|
| Organisation Website: |
http://www.cam.ac.uk |