EPSRC logo

Details of Grant 

EPSRC Reference: GR/S57198/01
Title: Automation for Interactive Proof
Principal Investigator: Paulson, Professor LC
Other Investigators:
Researcher Co-Investigators:
Project Partners:
Department: Computer Laboratory
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