EPSRC Reference: 
GR/S57198/01 
Title: 
Automation for Interactive Proof 
Principal Investigator: 
Paulson, Professor LC 
Other Investigators: 

Researcher CoInvestigators: 

Project Partners: 

Department: 
Computer Laboratory 
Organisation: 
University of Cambridge 
Scheme: 
Standard Research (PreFEC) 
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 computerbased 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 nonacademic contexts 
Isabelle is already used in some researchoriented commercial firms, such as Galois Inc. Another nonacademic 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 