Document Open Access Logo

A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm

Authors Katherine Cordwell , Yong Kiam Tan , André Platzer

PDF
Thumbnail PDF

File

LIPIcs.ITP.2021.14.pdf
  • Filesize: 1.08 MB
  • 20 pages

Document Identifiers

Author Details

Katherine Cordwell
  • Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, USA
Yong Kiam Tan
  • Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, USA
André Platzer
  • Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, USA

Funding

This material is based upon work supported by the National Science Foundation under Grant No. CNS-1739629 and by the AFOSR under grant number FA9550-16-1-0288. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation or of AFOSR.
  • Cordwell, Katherine: This material is based upon work supported by a National Science Foundation Graduate Research Fellowship under Grants Nos. DGE1252522 and DGE1745016.
  • Tan, Yong Kiam: The second author was supported by A*STAR, Singapore.

Acknowledgements

We thank Brandon Bohrer, Fabian Immler, and Wenda Li for useful discussions about Isabelle/HOL and its libraries. We also thank the ITP'21 anonymous reviewers and Magnus Myreen for helpful feedback on earlier drafts of this paper.

Cite AsGet BibTex

Katherine Cordwell, Yong Kiam Tan, and André Platzer. A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 14:1-14:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.ITP.2021.14

Abstract

We formalize the univariate fragment of Ben-Or, Kozen, and Reif’s (BKR) decision procedure for first-order real arithmetic in Isabelle/HOL. BKR’s algorithm has good potential for parallelism and was designed to be used in practice. Its key insight is a clever recursive procedure that computes the set of all consistent sign assignments for an input set of univariate polynomials while carefully managing intermediate steps to avoid exponential blowup from naively enumerating all possible sign assignments (this insight is fundamental for both the univariate case and the general case). Our proof combines ideas from BKR and a follow-up work by Renegar that are well-suited for formalization. The resulting proof outline allows us to build substantially on Isabelle/HOL’s libraries for algebra, analysis, and matrices. Our main extensions to existing libraries are also detailed.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • quantifier elimination
  • matrix
  • theorem proving
  • real arithmetic

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Saugata Basu, Richard Pollack, and Marie-Françoise Roy. Algorithms in Real Algebraic Geometry. Springer, Berlin, Heidelberg, second edition, 2006. URL: https://doi.org/10.1007/3-540-33099-2.
  2. Michael Ben-Or, Dexter Kozen, and John H. Reif. The complexity of elementary algebra and geometry. J. Comput. Syst. Sci., 32(2):251-264, 1986. URL: https://doi.org/10.1016/0022-0000(86)90029-2.
  3. John F. Canny. Improved algorithms for sign determination and existential quantifier elimination. Comput. J., 36(5):409-418, 1993. URL: https://doi.org/10.1093/comjnl/36.5.409.
  4. Cyril Cohen. Formalized algebraic numbers: construction and first-order theory. PhD thesis, École polytechnique, November 2012. URL: https://perso.crans.org/cohen/papers/thesis.pdf.
  5. Cyril Cohen and Assia Mahboubi. Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. Log. Methods Comput. Sci., 8(1), 2012. URL: https://doi.org/10.2168/LMCS-8(1:2)2012.
  6. George E. Collins. Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In H. Barkhage, editor, Automata Theory and Formal Languages, volume 33 of LNCS, pages 134-183. Springer, 1975. URL: https://doi.org/10.1007/3-540-07407-4_17.
  7. Katherine Cordwell, César Muñoz, and Aaron Dutle. Improving automated strategies for univariate quantifier elimination. Technical Memorandum NASA/TM-20205010644, NASA, Langley Research Center, Hampton VA 23681-2199, USA, January 2021. URL: https://ntrs.nasa.gov/citations/20205010644.
  8. Katherine Cordwell, Yong Kiam Tan, and André Platzer. The BKR decision procedure for univariate real arithmetic. Archive of Formal Proofs, 2021. , Formal proof development. URL: https://www.isa-afp.org/entries/BenOr_Kozen_Reif.html.
  9. Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, and Akihisa Yamada. A formalization of the Berlekamp-Zassenhaus factorization algorithm. In Yves Bertot and Viktor Vafeiadis, editors, CPP, pages 17-29. ACM, 2017. URL: https://doi.org/10.1145/3018610.3018617.
  10. Jose Divasón and Jesús Aransay. Rank-nullity theorem in linear algebra. Archive of Formal Proofs, 2013. , Formal proof development. URL: https://isa-afp.org/entries/Rank_Nullity_Theorem.html.
  11. Jose Divasón and Jesús Aransay. Gauss-Jordan algorithm and its applications. Archive of Formal Proofs, September 2014. , Formal proof development. URL: https://isa-afp.org/entries/Gauss_Jordan.html.
  12. Lionel Ducos. Optimizations of the subresultant algorithm. J. Pure Appl. Algebra, 145(2):149-163, 2000. URL: https://doi.org/10.1016/S0022-4049(98)00081-4.
  13. Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Hoang Le Truong, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, et al. A formal proof of the Kepler conjecture. Forum of Mathematics, Pi, 5, 2017. URL: https://doi.org/10.1017/fmp.2017.1.
  14. John Harrison. Floating-point verification using theorem proving. In Marco Bernardo and Alessandro Cimatti, editors, SFM, volume 3965 of LNCS, pages 211-242. Springer, 2006. URL: https://doi.org/10.1007/11757283_8.
  15. John Harrison. Verifying nonlinear real formulas via sums of squares. In Klaus Schneider and Jens Brandt, editors, TPHOLs, volume 4732 of LNCS, pages 102-118. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-74591-4_9.
  16. Johannes Hölzl. Proving inequalities over reals with computation in Isabelle/HOL. In Gabriel Dos Reis and Laurent Théry, editors, PLMMS, pages 38-45, Munich, August 2009. Google Scholar
  17. Wenda Li. The Sturm-Tarski theorem. Archive of Formal Proofs, 2014. , Formal proof development. URL: https://isa-afp.org/entries/Sturm_Tarski.html.
  18. Wenda Li, Grant Olney Passmore, and Lawrence C. Paulson. Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL. J. Autom. Reason., 62(1):69-91, 2019. URL: https://doi.org/10.1007/s10817-017-9424-6.
  19. Wenda Li and Lawrence C. Paulson. A modular, efficient formalisation of real algebraic numbers. In Jeremy Avigad and Adam Chlipala, editors, CPP, pages 66-75. ACM, 2016. URL: https://doi.org/10.1145/2854065.2854074.
  20. Wenda Li and Lawrence C. Paulson. Counting polynomial roots in Isabelle/HOL: a formal proof of the Budan-Fourier theorem. In Assia Mahboubi and Magnus O. Myreen, editors, CPP, pages 52-64. ACM, 2019. URL: https://doi.org/10.1145/3293880.3294092.
  21. Scott McCallum. Solving polynomial strict inequalities using cylindrical algebraic decomposition. Comput. J., 36(5):432-438, 1993. URL: https://doi.org/10.1093/comjnl/36.5.432.
  22. Sean McLaughlin and John Harrison. A proof-producing decision procedure for real arithmetic. In Robert Nieuwenhuis, editor, CADE, volume 3632 of LNCS, pages 295-314. Springer, 2005. URL: https://doi.org/10.1007/11532231_22.
  23. César A. Muñoz, Anthony J. Narkawicz, and Aaron Dutle. A decision procedure for univariate polynomial systems based on root counting and interval subdivision. J. Formaliz. Reason., 11(1):19-41, 2018. URL: https://doi.org/10.6092/issn.1972-5787/8212.
  24. Anthony Narkawicz, César A. Muñoz, and Aaron Dutle. Formally-verified decision procedures for univariate polynomial computation based on Sturm’s and Tarski’s theorems. J. Autom. Reason., 54(4):285-326, 2015. URL: https://doi.org/10.1007/s10817-015-9320-x.
  25. Tobias Nipkow. Linear quantifier elimination. J. Autom. Reason., 45(2):189-212, 2010. URL: https://doi.org/10.1007/s10817-010-9183-0.
  26. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. URL: https://doi.org/10.1007/3-540-45949-9.
  27. Lawrence C. Paulson. The foundation of a generic theorem prover. J. Autom. Reason., 5(3):363-397, 1989. URL: https://doi.org/10.1007/BF00248324.
  28. Lawrence C. Paulson and Jasmin Christian Blanchette. Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In Geoff Sutcliffe, Stephan Schulz, and Eugenia Ternovska, editors, IWIL, volume 2 of EPiC Series in Computing, pages 1-11. EasyChair, 2010. URL: https://easychair.org/publications/paper/wV.
  29. André Platzer. Logical Foundations of Cyber-Physical Systems. Springer, Cham, 2018. URL: https://doi.org/10.1007/978-3-319-63588-0.
  30. André Platzer, Jan-David Quesel, and Philipp Rümmer. Real world verification. In Renate A. Schmidt, editor, CADE, volume 5663 of LNCS, pages 485-501. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02959-2_35.
  31. T.V.H. Prathamesh. Tensor product of matrices. Archive of Formal Proofs, January 2016. , Formal proof development. URL: https://isa-afp.org/entries/Matrix_Tensor.html.
  32. James Renegar. On the computational complexity and geometry of the first-order theory of the reals, part III: Quantifier elimination. J. Symb. Comput., 13(3):329-352, 1992. URL: https://doi.org/10.1016/S0747-7171(10)80005-7.
  33. Alexey Solovyev. Formal Computations and Methods. PhD thesis, University of Pittsburgh, January 2013. URL: https://d-scholarship.pitt.edu/16721/.
  34. Christian Sternagel and René Thiemann. Executable matrix operations on matrices of arbitrary dimensions. Archive of Formal Proofs, 2010. , Formal proof development. URL: https://isa-afp.org/entries/Matrix.html.
  35. Thomas Sturm. A survey of some methods for real quantifier elimination, decision, and satisfiability and their applications. Math. Comput. Sci., 11(3-4):483-502, 2017. URL: https://doi.org/10.1007/s11786-017-0319-z.
  36. Alfred Tarski. A Decision Method for Elementary Algebra and Geometry. RAND Corporation, Santa Monica, CA, 1951. Prepared for publication with the assistance of J.C.C. McKinsey. URL: https://www.rand.org/pubs/reports/R109.html.
  37. René Thiemann and Akihisa Yamada. Formalizing Jordan normal forms in Isabelle/HOL. In Jeremy Avigad and Adam Chlipala, editors, CPP, pages 88-99. ACM, 2016. URL: https://doi.org/10.1145/2854065.2854073.
  38. René Thiemann and Akihisa Yamada. Matrices, Jordan normal forms, and spectral radius theory. Archive of Formal Proofs, 2015. , Formal proof development. URL: https://isa-afp.org/entries/Jordan_Normal_Form.html.
  39. René Thiemann, Akihisa Yamada, and Sebastiaan Joosten. Algebraic numbers in Isabelle/HOL. Archive of Formal Proofs, 2015. , Formal proof development. URL: https://isa-afp.org/entries/Algebraic_Numbers.html.
  40. Joachim von zur Gathen. Parallel algorithms for algebraic problems. SIAM J. Comput., 13(4):802-824, 1984. URL: https://doi.org/10.1137/0213050.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact