Verified quadratic virtual substitution for real arithmetic. (English) Zbl 1521.68246
Huisman, Marieke (ed.) et al., Formal methods. 24th international symposium, FM 2021, virtual event, November 20–26, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13047, 200-217 (2021).
Summary: This paper presents a formally verified quantifier elimination (QE) algorithm for first-order real arithmetic by linear and quadratic virtual substitution (VS) in Isabelle/HOL. The Tarski-Seidenberg theorem established that the first-order logic of real arithmetic is decidable by QE. However, in practice, QE algorithms are highly complicated and often combine multiple methods for performance. VS is a practically successful method for QE that targets formulas with low-degree polynomials. To our knowledge, this is the first work to formalize VS for quadratic real arithmetic including inequalities. The proofs necessitate various contributions to the existing multivariate polynomial libraries in Isabelle/HOL. Our framework is modularized and easily expandable (to facilitate integrating future optimizations), and could serve as a basis for developing practical general-purpose QE algorithms. Further, as our formalization is designed with practicality in mind, we export our development to SML and test the resulting code on 378 benchmarks from the literature, comparing to Redlog, Z3, Wolfram Engine, and SMT-RAT. This identified inconsistencies in some tools, underscoring the significance of a verified approach for the intricacies of real arithmetic.
For the entire collection see [Zbl 1509.68013].
For the entire collection see [Zbl 1509.68013].
MSC:
| 68V20 | Formalization of mathematics in connection with theorem provers |
| 03B35 | Mechanization of proofs and logical operations |
| 03C10 | Quantifier elimination, model completeness, and related topics |
| 03F30 | First-order arithmetic and fragments |
Software:
z3; KeYmaera; KeYmaera X; Archive Formal Proofs; Polynomials; Isabelle/HOL; dReal; REDLOG; SMT-RAT; Orbital library; CakeMLReferences:
| [1] | Bohrer, B., Rahli, V., Vukotic, I., Völp, M., Platzer, A.: Formally verified differential dynamic logic. In: Bertot, Y., Vafeiadis, V. (eds.) CPP, pp. 208-221. ACM, New York (2017). doi:10.1145/3018610.3018616 |
| [2] | Chaieb, A.: Automated methods for formal proofs in simple arithmetics and algebra. Ph.D. thesis, Technische Universität München (2008). mediatum.ub.tum.de/doc/649541/649541.pdf |
| [3] | Cohen, C., Mahboubi, A.: Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. Log. Methods Comput. Sci. 8(1) (2012). doi:10.2168/LMCS-8(1:2)2012 · Zbl 1241.68096 |
| [4] | Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Barkhage, H. (ed.) Automata Theory and Formal Languages. LNCS, vol. 33, pp. 134-183. Springer (1975). doi:10.1007/3-540-07407-4_17 · Zbl 0318.02051 |
| [5] | Corzilius, F., Kremer, G., Junges, S., Schupp, S., Ábrahám, E.: SMT-RAT: an open source C++ toolbox for strategic and parallel SMT solving. In: Heule, M., Weaver, S.A. (eds.) SAT. LNCS, vol. 9340, pp. 360-368. Springer (2015). doi:10.1007/978-3-319-24318-4_26 · Zbl 1471.68241 |
| [6] | Dolzmann, A.; Sturm, T., REDLOG: computer algebra meets computer logic, SIGSAM Bull., 31, 2, 2-9 (1997) · doi:10.1145/261320.261324 |
| [7] | Durán, A.J., Pérez, M., Varona, J.L.: The misfortunes of a trio of mathematicians using computer algebra systems. can we trust in them? Notices of the AMS 61(10), 1249-1252 (2014). doi:10.1090/noti1173 · Zbl 1338.68299 |
| [8] | Fulton, N., Mitsch, S., Quesel, J.D., Völp, M., Platzer, A.: KeYmaera X: An axiomatic tactical theorem prover for hybrid systems. In: Felty, A.P., Middeldorp, A. (eds.) CADE. LNCS, vol. 9195, pp. 527-538. Springer (2015). doi:10.1007/978-3-319-21401-6_36 · Zbl 1465.68281 |
| [9] | Gao, S., Kong, S., Clarke, E.M.: dReal: An SMT solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) CADE. LNCS, vol. 7898, pp. 208-214. Springer (2013). doi:10.1007/978-3-642-38574-2_14 · Zbl 1381.68268 |
| [10] | Hupel, L., Nipkow, T.: A verified compiler from Isabelle/HOL to CakeML. In: Ahmed, A. (ed.) ESOP. LNCS, vol. 10801, pp. 999-1026. Springer (2018). doi:10.1007/978-3-319-89884-1_35 · Zbl 1418.68045 |
| [11] | Jovanovic, D., de Moura, L.M.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR. LNCS, vol. 7364, pp. 339-354. Springer (2012). doi:10.1007/978-3-642-31365-3_27 · Zbl 1358.68257 |
| [12] | Košta, M.: New concepts for real quantifier elimination by virtual substitution. Ph.D. thesis, Universität des Saarlandes (2016) |
| [13] | McLaughlin, S., Harrison, J.: A proof-producing decision procedure for real arithmetic. In: Nieuwenhuis, R. (ed.) CADE. LNCS, vol. 3632, pp. 295-314. Springer (2005). doi:10.1007/11532231_22 · Zbl 1135.03329 |
| [14] | de Moura, L.M., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS. LNCS, vol. 4963, pp. 337-340. Springer (2008). doi:10.1007/978-3-540-78800-3_24 |
| [15] | Mulligan, C.B., Bradford, R.J., Davenport, J.H., England, M., Tonks, Z.: Quantifier elimination for reasoning in economics. CoRR (2018). arXiv:1804.10037 |
| [16] | Nipkow, T., Linear quantifier elimination, J. Autom. Reason., 45, 2, 189-212 (2010) · Zbl 1207.68339 · doi:10.1007/s10817-010-9183-0 |
| [17] | Passmore, G.O.: Combined decision procedures for nonlinear arithmetics, real and complex. Ph.D. thesis, School of Informatics, University of Edinburgh (2011) |
| [18] | Platzer, A.: Logical analysis of hybrid systems: proving theorems for complex dynamics. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14509-4 · Zbl 1211.68412 |
| [19] | Platzer, A.: Logical foundations of cyber-physical systems. Springer, Cham (2018). doi:10.1007/978-3-319-63588-0 · Zbl 1400.93003 |
| [20] | Platzer, A., Quesel, J.D., Rümmer, P.: Real world verification. In: Schmidt, R.A. (ed.) CADE. LNCS, vol. 5663, pp. 485-501. Springer, Berlin (2009). doi:10.1007/978-3-642-02959-2_35 · Zbl 1250.68197 |
| [21] | Ratschan, S., Smaus, J.: Verification-integrated falsification of non-deterministic hybrid systems. In: Cassandras, C.G., Giua, A., Seatzu, C., Zaytoon, J. (eds.) ADHS. IFAC Proceedings Volumes, vol. 39, pp. 371-376. Elsevier (2006). doi:10.3182/20060607-3-IT-3902.00068 |
| [22] | Scharager, M., Cordwell, K., Mitsch, S., Platzer, A.: Verified quadratic virtual substitution for real arithmetic. Archive of Formal Proofs, Formal proof development (2021). https://www.isa-afp.org/entries/Virtual_Substitution.html |
| [23] | Scharager, M., Cordwell, K., Mitsch, S., Platzer, A.: Verified quadratic virtual substitution for real arithmetic. CoRR (2021). arXiv:2105.14183 |
| [24] | Scharager, M., Cordwell, K., Mitsch, S., Platzer, A.: Verified quadratic virtual substitution for real arithmetic: benchmark examples and scripts. Zenodo (2021). doi:10.5281/zenodo.5189881 |
| [25] | Seidenberg, A.: A new decision method for elementary algebra. Annals Math. 60(2), 365-374 (1954) · Zbl 0056.01804 |
| [26] | Sternagel, C., Thiemann, R.: Executable multivariate polynomials. Archive of Formal Proofs, Formal proof development (2010). www.isa-afp.org/entries/Polynomials.html |
| [27] | Sturm, T.: A survey of some methods for real quantifier elimination, decision, and satisfiability and their applications. Math. Comput. Sci. 11(3-4), 483-502 (2017). doi:10.1007/s11786-017-0319-z · Zbl 1425.68380 |
| [28] | Sturm, T.: Thirty years of virtual substitution: foundations, techniques, applications. In: Kauers, M., Ovchinnikov, A., Schost, É. (eds.) ISSAC, pp. 11-16. ACM (2018). doi:10.1145/3208976.3209030 · Zbl 1460.03007 |
| [29] | Tarski, A.: A decision method for elementary algebra and geometry. RAND Corporation, Santa Monica (1951) · Zbl 0044.25102 |
| [30] | Weispfenning, V., The complexity of linear problems in fields, J. Symb. Comput., 5, 1-2, 3-27 (1988) · Zbl 0646.03005 · doi:10.1016/S0747-7171(88)80003-8 |
| [31] | Weispfenning, V.: Quantifier elimination for real algebra - the cubic case. In: MacCallum, M.A.H. (ed.) ISSAC, pp. 258-263. ACM (1994). doi:10.1145/190347.190425 · Zbl 0919.03030 |
| [32] | Weispfenning, V., Quantifier elimination for real algebra - the quadratic case and beyond, Appl. Algebra Eng. Commun. Comput., 8, 2, 85-101 (1997) · Zbl 0867.03003 · doi:10.1007/s002000050055 |
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.
