EPSRC logo

Details of Grant 

EPSRC Reference: EP/C013409/1
Title: Beyond Linear Arithmetic: Automatic Proof Procedures for the Reals
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: 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 well-known 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 well-known 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 stand-alone automatic theorem prover to solve problems involving mathematical functions over the real numbers.
Potential use in non-academic contexts
MetiTarski is potentially applicable in control engineering and in electronics design.
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