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
The purpose of this project was to investigate whether two different types of mathematical reasoning tools (automatic theorem provers and interactive theorem provers) could be made to work together, making the latter easier to use. A number of technologies were developed to make this possible. The name chosen for the software output, Sledgehammer, gives a hint as to its power and effectiveness.
Potential use in non-academic contexts
Isabelle is already used in some research-oriented commercial firms, such as Galois Inc. Another non-academic user is the Kestrel Institute in Palo Alto, California.
Impacts
No information has been submitted for this grant.
Sectors submitted by the Researcher
Information & Communication Technologies
Project URL: http://www.cl.cam.ac.uk/research/hvg/isabelle/sledgehammer.html
Further Information:  
Organisation Website: http://www.cam.ac.uk