×

Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL. (English) Zbl 1468.68298

Summary: We present a proof procedure for univariate real polynomial problems in Isabelle/HOL. The core mathematics of our procedure is based on univariate cylindrical algebraic decomposition. We follow the approach of untrusted certificates, separating solving from verifying: efficient external tools perform expensive real algebraic computations, producing evidence that is formally checked within Isabelle’s logic. This allows us to exploit highly-tuned computer algebra systems like Mathematica to guide our procedure without impacting the correctness of its results. We present experiments demonstrating the efficacy of this approach, in many cases yielding orders of magnitude improvements over previous methods.

MSC:

68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
12D10 Polynomials in real and complex fields: location of zeros (algebraic theorems)
68W30 Symbolic computation and algebraic computation
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Akbarpour, B., Paulson, L.: MetiTarski: an automatic theorem prover for real-valued special functions. J. Autom. Reason. 44(3), 175-205 (2010) · Zbl 1215.68206
[2] Basu, S., Pollack, R., Roy, M.F.: Algorithms in Real Algebraic Geometry (Algorithms and Computation in Mathematics). Springer, New York (2006) · Zbl 1102.14041
[3] Brown, C.W.: QEPCAD B: a program for computing with semi-algebraic sets using CADs. ACM SIGSAM Bull. 37(4), 97-108 (2003) · Zbl 1083.68148
[4] Chaieb, A., et al.: Automated methods for formal proofs in simple arithmetics and algebra. Dissertation, Technische Universität, München (2008)
[5] Cheng, J.S., Gao, X.S., Yap, C.K.: Complete numerical isolation of real zeros in zero-dimensional triangular systems. In: Proceedings of the 2007 International Symposium on Symbolic and Algebraic Computation, pp. 92-99. ACM (2007) · Zbl 1190.65082
[6] Cohen, C.: Formalized algebraic numbers: construction and first-order theory. Ph.D. thesis, École polytechnique (2012)
[7] Cohen, C., Mahboubi, A., et al.: Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. Log. Methods Comput. Sci. 8(1: 02), 1-40 (2012) · Zbl 1241.68096
[8] Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition: a synopsis. ACM SIGSAM Bull. 10(1), 10-12 (1976)
[9] De Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 337-340. Springer, Berlin (2008)
[10] De Moura, L., Passmore, G.O.: Computation in real closed infinitesimal and transcendental extensions of the rationals. In: International Conference on Automated Deduction, pp. 178-192. Springer, Berlin (2013) · Zbl 1381.68278
[11] Denman, W., Akbarpour, B., Tahar, S., Zaki, M.H., Paulson, L.C.: Formal verification of analog designs using MetiTarski. In: Formal Methods in Computer-Aided Design, 2009. FMCAD 2009, pp. 93-100. IEEE (2009)
[12] Denman, W., Muñoz, C.: Automated real proving in PVS via MetiTarski. In: FM 2014: Formal Methods, pp. 194-199. Springer (2014)
[13] Denman, W., Zaki, M.H., Tahar, S., Rodrigues, L.: Towards flight control verification using automated theorem proving. In: NASA Formal Methods, pp. 89-100. Springer (2011)
[14] Eberl, M.: A decision procedure for univariate real polynomials in Isabelle/HOL. In: Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP ’15, pp. 75-83. ACM, New York (2015). doi:10.1145/2676724.2693166
[15] Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Le Roux, S., Mahboubi, A., O’Connor, R., Ould Biha, S., Pasca, I., Rideau, L., Solovyev, A., Tassi, E., Théry, L.: A machine-checked proof of the odd order theorem. In: Blazy S., Paulin-Mohring C., Pichardie D. (eds.) Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes, France, July 22-26. Lecture Notes in Computer Science, vol. 7998, pp. 163-179. Springer, Berlin (2013) · Zbl 1317.68211
[16] Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: International Symposium on Functional and Logic Programming, pp. 103-117. Springer (2010) · Zbl 1284.68131
[17] Harrison, J.: Verifying nonlinear real formulas via sums of squares. In: K. Schneider, J. Brandt (eds.) Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2007, Lecture Notes in Computer Science, vol. 4732, pp. 102-118. Springer, Kaiserslautern (2007) · Zbl 1144.68357
[18] Hölzl, J.: Proving inequalities over reals with computation in Isabelle/HOL. In: International Workshop on Programming Languages for Mechanized Mathematics Systems, pp. 38-45 (2009)
[19] Hurd, J.: Metis first order prover. http://gilith.com/software/metis (2007)
[20] Li, W., Paulson, L.C.: A formal proof of Cauchy’s residue theorem. In: ITP 2016: Seventh International Conference on Interactive Theorem Proving (2016, to appear) · Zbl 1478.68440
[21] Li, W., Paulson, L.C.: A modular, efficient formalisation of real algebraic numbers. In: Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, pp. 66-75. ACM (2016)
[22] Mahboubi, A.: Implementing the cylindrical algebraic decomposition within the Coq system. Math. Struct. Comput. Sci. 17(1), 99-127 (2007) · Zbl 1121.03023
[23] Mishra, B.: Algorithmic Algebra. Springer, New York (1993) · Zbl 0804.13009
[24] Muñoz, C., Narkawicz, A.: Formalization of Bernstein polynomials and applications to global optimization. J. Autom. Reason. 51(2), 151-196 (2013). doi:10.1007/s10817-012-9256-3 · Zbl 1314.68286
[25] Narkawicz, A., Munoz, C., Dutle, A.: Formally-verified decision procedures for univariate polynomial computation based on Sturm’s and Tarski’s theorems. J. Autom. Reason. 54(4), 285-326 (2015) · Zbl 1356.68196
[26] Narkawicz, A.J., Muñoz, C.A.: A formally-verified decision procedure for univariate polynomial computation based on Sturm’s theorem. Technical Memorandum NASA/TM-2014-218548, NASA, Langley Research Center, Hampton VA 23681-2199, USA (2014)
[27] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer, Berlin (2002) · Zbl 0994.68131
[28] Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: International Conference on Automated Deduction, pp. 748-752. Springer (1992)
[29] Passmore, G.O., Paulson, L.C., De Moura, L.: Real algebraic strategies for MetiTarski proofs. In: International Conference on Intelligent Computer Mathematics, pp. 358-370. Springer (2012) · Zbl 1360.68764
[30] Paulson, L.C.: Real-valued special functions: upper and lower bounds. Archive of Formal Proofs (2014)
[31] Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: IWIL-2010, vol. 1 (2010)
[32] Rahman, Q., Schmeisser, G.: Analytic Theory of Polynomials. London Mathematical Society Monographs. Clarendon Press, Oxford (2002). https://books.google.co.uk/books?id=FzFEEVO3PXYC · Zbl 1072.30006
[33] Sagraloff, M.: A general approach to isolating roots of a bitstream polynomial. Math. Comput. Sci. 4(4), 481-506 (2010) · Zbl 1229.65077
[34] Solovyev, A., Hales, T.C.: Formal verification of nonlinear inequalities with Taylor interval approximations. In: NASA Formal Methods, pp. 383-397. Springer, Berlin (2013)
[35] Strzeboński, A.W.: Cylindrical algebraic decomposition using validated numerics. J. Symb. Comput. 41(9), 1021-1038 (2006) · Zbl 1124.68123
[36] Thiemann, R., Yamada, A.: Algebraic numbers in Isabelle/HOL. Archive of Formal Proofs (2015). http://isa-afp.org/entries/Algebraic_Numbers.shtml. Formal proof development · Zbl 1478.68443
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.