EPSRC Reference: 
EP/C013409/1 
Title: 
Beyond Linear Arithmetic: Automatic Proof Procedures for the Reals 
Principal Investigator: 
Paulson, Professor LC 
Other Investigators: 

Researcher CoInvestigators: 

Project Partners: 

Department: 
Computer Laboratory 
Organisation: 
University of Cambridge 
Scheme: 
Standard Research (PreFEC) 
Starts: 
01 November 2005 
Ends: 
31 October 2008 
Value (£): 
211,612

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 
Computers are increasingly being used to analyse mathematical formulas, for example to help certify the correctness of aerospace software. These formulas may contain standard arithmetic operations such as addition and multiplication, as well as transcendental functions such as sines, cosines, exponentials and logarithms. Such formulas may be complicated, but not intrinsically deep: they typically hold by wellknown mathematical results. The proposal is to develop new techniques for proving such formulas automatically. The most popular techniques work only for linear formulas, namely formulas that compare values expressed using addition and subtraction, allowing multiplication by constants only. More general algorithms (such as cylindrical algebraic decomposition) allow unrestricted multiplication, but can require immense amounts of computer power even in simple cases. No general algorithms are known that also handle transcendental functions. The new techniques will extend a classic algorithm for linear problems, due to Fourier and Motzkin. They will incorporate basic information about transcendental functions, such as linear upper or lower bounds. These techniques will not be able to solve all problems, but they will be able to solve a wide range of problems that arise in practice. Part of the project plan is to assemble a collection of typical problems, which will serve as a resource for future researchers.Disproof techniques will also be developed. They will work by generating random counterexamples, which will be checked using exact real arithmetic in order to avoid rounding errors. Disproof procedures identify invalid formulas, which presumably indicate flaws in the design that is under investigation. They will support the modern trend of using formal methods to debug designs.

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: 
http://www.cl.cam.ac.uk/~lp15/papers/Arith/index.html 
Further Information: 

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