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 project was originally conceived to identify very simple techniques for proving facts about some wellknown mathematical functions, such as logarithms, sine and cosine. The initial intention was that these techniques would then be integrated with Isabelle, an interactive theorem prover.
In the course of the research, much more powerful and ambitious techniques came to light. Rather than implementing them within Isabelle, we built a separate piece of software, called MetiTarski. This is a standalone automatic theorem prover to solve problems involving mathematical functions over the real numbers.

Potential use in nonacademic contexts 
MetiTarski is potentially applicable in control engineering and in electronics design.

Impacts 
No information has been submitted for this grant.

Sectors submitted by the Researcher 
Electronics; Information & Communication Technologies

Project URL: 
http://www.cl.cam.ac.uk/~lp15/papers/Arith/index.html 
Further Information: 

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