EPSRC Reference: 
EP/G002290/1 
Title: 
Automated Formal Proofs for Polynomial and Transcendental Problems 
Principal Investigator: 
Paulson, Professor LC 
Other Investigators: 

Researcher CoInvestigators: 

Project Partners: 

Department: 
Computer Science and Technology 
Organisation: 
University of Cambridge 
Scheme: 
Standard Research 
Starts: 
01 September 2008 
Ends: 
31 August 2009 
Value (£): 
86,405

EPSRC Research Topic Classifications: 
Fundamentals of Computing 


EPSRC Industrial Sector Classifications: 
No relevance to Underpinning Sectors 


Related Grants: 

Panel History: 
Panel Date  Panel Name  Outcome 
21 Apr 2008

ICT Prioritisation Panel (April 2008)

Announced


Summary on Grant Application Form 
Many applications in science and engineering involve mathematical formulas. Such formulas may involve polynomials, logarithms, exponentials and related functions, perhaps combined using logical symbols to express conditional statements. No automatic procedure exists for solving such problems in the general case. Where automatic procedures do exist, they are often far too expensive (in terms of computer time and memory requirements) to use in practice. However, a judicious selection of specialised procedures can yield efficient solutions for many problems that arise in practice. The proposal is to identify and implement variety of such procedures.This work will be undertaken in the context of software tools known as interactive theorem provers. These tools perform logical deductions to be very high degree of reliability; they are increasingly being utilised to help assure correctness for safety critical applications. A primary challenge of this project is to reconcile the detailed lowlevel checking used in interactive theorem provers with the highlevel reasoning typical of most approaches to solving mathematical formulas. One fruitful technique is to deliver evidence from the mathematical solver to the interactive theorem prover: for some types of problems, finding the solution is difficult, but verifying a claimed solution is easy.

Key Findings 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Potential use in nonacademic 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: 

Further Information: 

Organisation Website: 
http://www.cam.ac.uk 