| EPSRC Reference: |
EP/I011005/1 |
| Title: |
Automatic Proof Procedures for Polynomials and Special Functions |
| Principal Investigator: |
Paulson, Professor LC |
| Other Investigators: |
|
| Researcher Co-investigators: |
|
| Project Partners: |
|
| Department: |
Computer Laboratory |
| Organisation: |
University of Cambridge |
| Scheme: |
Standard Research |
| Starts: |
01 November 2010 |
Ends: |
31 October 2014 |
Value (£): |
533,183
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
Software Engineering |
| System on Chip |
|
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
| Panel Date | Panel Name | Outcome |
|
07 Sep 2010
|
ICT Prioritisation Panel (Sept 2010)
|
Announced
|
|
|
Summary on Grant Application Form |
|
An engineering design is expected to satisfy safety constraints, many of which can be expressed as mathematical and logical formulas. Computer software exists that can check some such formulas automatically, but although they can have a large and complicated logical structure, the mathematical component currently has to be linear: in other words, involving nothing more complicated than addition. Real-world engineering problems involve sophisticated mathematical concepts, such as polynomials and transcendental functions.The investigators have developed software (called MetiTarski and RAHD) that can solve such problems in many cases. The current project will extend the scope of this software, increasing its power and targeting it at specific real-world application areas. One such application is analogue circuitry, which is widespread in consumer electronics. The project will investigate many other potential applications In engineering and the mathematical sciences.
|
|
Key Findings |
One of our primary goals is to deliver our technology in the form of software tools, in particular, our theorem-prover MetiTarski. Version 1.9 was released to the research community in August 2011, and a dramatically more powerful Version 2.0 will be released in the first half of 2012.
We have made fundamental discoveries about how such software should be built for best performance, in particular through our investigations of backtracking and through special modifications of the decision procedures that we call. We are also making progress on applications of this software in control engineering, for example, to prove stability.
The research is still in its second year, so our findings are necessarily preliminary.
|
|
Potential use in non-academic contexts |
|
No information has been submitted for this grant.
|
|
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/~lp15/papers/Arith/index.html |
| Further Information: |
|
| Organisation Website: |
http://www.cam.ac.uk |