Automated Formal Proofs for Polynomial and Transcendental Problems

• Funded by the EPSRC: Grant reference EP/G002290/1
• Value £86,405; duration 1/9/2008 to 31/8/2009
• Read the full case for support.

Project Members

• Lawrence C. Paulson (Principal investigator)
• Amine Chaieb (Research associate)

Background to the Research

The proposal is to investigate methods for automating formal proofs about polynomials and transcendental functions, and to implement them within an interactive theorem prover, Isabelle. The problems are formulated as universal polynomial or transcendental properties or even as general first order arithmetic formulae. We expect a tremendous increase in automation for the universal case and for several cases of the general first order case as well. We also expect improved automation for proofs about power series and transcendental functions.

The problems we want to solve are inherently non-linear and arise in many applications: algorithm and program verification, hardware implementations of transcendental functions, etc. Although we know since Tarski (1951) that the first order theory of real closed fields admits quantifier elimination and is decidable, the intractable complexity of the problem and all known methods make it almost useless. The only procedures seriously integrated (by yielding a proof of their result) in an interactive theorem prover are very simple andthey have non-elementary complexity bounds, making them useless even for simple examples. Sophisticated algorithms like cylindrical algebraic decomposition (CAD) seem to be a serious challenge for theorem provers and might require several years to verify.

Our approach is to design and implement efficient methods for special and practical cases, and to have one simple complete algorithm as a fall-back solution to eliminate one quantifier. Chaieb has almost finished the implementation of Cohen's (1969) procedure. We intend to employ theorem proving and mathematical techniques, such as computational reflection and efficient quantifier elimination procedures for special cases, using expensive general procedures only as a last resort.

This project has also investigated the potential of the MetiTarski theorem prover to support the objectives named above, ultimately within interactive theorem provers. This involves formalising within Isabelle some of the approximations used by MetiTarski, while at the same time continuing to refine MetiTarski.

Project papers

1. Behzad Akbarpour and Lawrence C. Paulson.
   Applications of MetiTarski in the Verification of Control and Hybrid Systems. In: Rupak Majumdar and Paulo Tabuada (editors), Hybrid Systems: Computation and Control (Springer LNCS 5469, 2009), 1–15. Publisher's version
2. Behzad Akbarpour and Lawrence C. Paulson.
   MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions. J. Automated Reasoning 44 (3), 175–205 (2010). Publisher's version
3. Amine Chaieb.
   Formal Power Series.
   J. Automated Reasoning 47 (3), 291–318 (2010). Publisher's version