Funded by the EPSRC (1/11/2005 to 31/10/2008)
Grant reference EP/C013409/1. Value £211,612
A primary goal of formal verification research is improved automation. Many verification tasks involve proving inequalities over the reals. Some of them also involve real-valued special functions such as exponentials and logarithms.
Linear arithmetic is well understood, and many proof tools provide efficient decision procedures, at least for the quantifier-free case. Such procedures can automatically prove propositional combinations of inequalities between linear combinations of variables. How can we extend this language?
The alternatives are to employ more general decision procedures or to seek heuristic methods. More general decision procedures do exist, because the theory of real closed fields is decidable: thus, our language can be extended with multiplication and quantifiers. Heuristic methods tend to be extensions of elementary variable elimination methods, and many have been deployed. For verification purposes, heuristic methods are typically broader in scope and more efficient than decision procedures.
This project will focus on heuristic procedures to prove arithmetic statements that may refer to transcendental functions and polynomials. The statements must be quantifier-free, with free variables being implicitly universally quantified.
The Project Objectives are pragmatic, and focus equally on interactive and automatic verification.
This project ended in October 2008. It delivered a new automatic theorem prover, called MetiTarski, for proving first-order formulas involving the real-valued special functions. It embodies a unique architecture that combines a resolution theorem prover with a decision procedure for the theory of real closed fields.