More Web Proxy on the site http://driver.im/

research-article

Open access

A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL

Authors:

Katherine Kosaian,

André PlatzerAuthors Info & Claims

CPP 2023: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs

Pages 211 - 224

https://doi.org/10.1145/3573105.3575672

Published: 11 January 2023 Publication History

Abstract

We formalize a multivariate quantifier elimination (QE) algorithm in the theorem prover Isabelle/HOL. Our algorithm is complete, in that it is able to reduce any quantified formula in the first-order logic of real arithmetic to a logically equivalent quantifier-free formula. The algorithm we formalize is a hybrid mixture of Tarski’s original QE algorithm and the Ben-Or, Kozen, and Reif algorithm, and it is the first complete multivariate QE algorithm formalized in Isabelle/HOL.

References

[1]

Saugata Basu, Richard Pollack, and Marie-Françoise Roy. 2006. Algorithms in Real Algebraic Geometry (second ed.). Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-33099-2

[2]

Michael Ben-Or, Dexter Kozen, and John H. Reif. 1986. The Complexity of Elementary Algebra and Geometry. J. Comput. Syst. Sci., 32, 2 (1986), 251–264. https://doi.org/10.1016/0022-0000(86)90029-2

Digital Library

[3]

Christopher W. Brown. 2001. Improved Projection for Cylindrical Algebraic Decomposition. J. Symb. Comput., 32, 5 (2001), 447–465. https://doi.org/10.1006/jsco.2001.0463

Digital Library

[4]

Christopher W. Brown. 2003. QEPCAD B: a program for computing with semi-algebraic sets using CADs. SIGSAM Bull., 37, 4 (2003), 97–108. https://doi.org/10.1145/968708.968710

Digital Library

[5]

John F. Canny. 1993. Improved Algorithms for Sign Determination and Existential Quantifier Elimination. Comput. J., 36, 5 (1993), 409–418. https://doi.org/10.1093/comjnl/36.5.409

[6]

Cyril Cohen. 2012. Formalized algebraic numbers: construction and first-order theory. Ph. D. Dissertation. École polytechnique. https://perso.crans.org/cohen/papers/thesis.pdf

[7]

Cyril Cohen. 2021. Formalization of a sign determination algorithm in real algebraic geometry. Preprint on webpage at https://hal.inria.fr/hal-03274013/document

[8]

Cyril Cohen and Assia Mahboubi. 2012. Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. Log. Methods Comput. Sci., 8, 1 (2012), https://doi.org/10.2168/LMCS-8(1:2)2012

[9]

George E. Collins. 1975. Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In Automata Theory and Formal Languages, H. Barkhage (Ed.) (LNCS, Vol. 33). Springer, 134–183. https://doi.org/10.1007/3-540-07407-4_17

[10]

George E. Collins and H. Hong. 1991. Partial Cylindrical Algebraic Decomposition for Quantifier Elimination. J. Symb. Comput., 12, 3 (1991), 299–328. https://doi.org/10.1016/S0747-7171(08)80152-6

Digital Library

[11]

Katherine Cordwell, Yong Kiam Tan, and André Platzer. 2021. The BKR Decision Procedure for Univariate Real Arithmetic. Archive of Formal Proofs, April, https://www.isa-afp.org/entries/BenOr_Kozen_Reif.html

[12]

Katherine Cordwell, Yong Kiam Tan, and André Platzer. 2021. A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm. In ITP, Liron Cohen and Cezary Kaliszyk (Eds.) (LIPIcs, Vol. 193). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 14:1–14:20. https://doi.org/10.4230/LIPIcs.ITP.2021.14

[13]

Felipe Cucker, Hervé Lanneau, Bud Mishra, Paul Pedersen, and Marie-Françoise Roy. 1992. NC Algorithms for Real Algebraic Numbers. Appl. Algebra Eng. Commun. Comput., 3 (1992), 79–98. https://doi.org/10.1007/BF01387193

Digital Library

[14]

James H. Davenport and Joos Heintz. 1988. Real Quantifier Elimination is Doubly Exponential. J. Symb. Comput., 5, 1/2 (1988), 29–35. https://doi.org/10.1016/S0747-7171(88)80004-X

Digital Library

[15]

Leonardo Mendonça de Moura and Grant Olney Passmore. 2013. Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals. In CADE, Maria Paola Bonacina (Ed.) (LNCS, Vol. 7898). Springer, 178–192. https://doi.org/10.1007/978-3-642-38574-2_12

Digital Library

[16]

Andreas Dolzmann, Andreas Seidl, and Thomas Sturm. 2004. Efficient projection orders for CAD. In ISSAC, Jaime Gutierrez (Ed.). ACM, 111–118. https://doi.org/10.1145/1005285.1005303

Digital Library

[17]

Manuel Eberl. 2015. A Decision Procedure for Univariate Real Polynomials in Isabelle/HOL. In CPP, Xavier Leroy and Alwen Tiu (Eds.). ACM, 75–83. https://doi.org/10.1145/2676724.2693166

Digital Library

[18]

Manuel Eberl and René Thiemann. 2021. Factorization of Polynomials with Algebraic Coefficients. Archive of Formal Proofs, November, issn:2150-914x https://isa-afp.org/entries/Factor_Algebraic_Polynomial.html

[19]

John Harrison. 2007. Verifying Nonlinear Real Formulas Via Sums of Squares. In TPHOLs, Klaus Schneider and Jens Brandt (Eds.) (LNCS, Vol. 4732). Springer, 102–118. https://doi.org/10.1007/978-3-540-74591-4_9

[20]

Joos Heintz, Marie-Françoise Roy, and Pablo Solernó. 1993. On the Theoretical and Practical Complexity of the Existential Theory of Reals. Comput. J., 36, 5 (1993), 427–431. https://doi.org/10.1093/comjnl/36.5.427

[21]

Hoon Hong. 1991. Comparison of Several Decision Algorithms for the Existential Theory of the Reals. RISC. https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.30.8707

[22]

Lars Hupel and Tobias Nipkow. 2018. A Verified Compiler from Isabelle/HOL to CakeML. In ESOP, Amal Ahmed (Ed.) (LNCS, Vol. 10801). Springer, 999–1026. https://doi.org/10.1007/978-3-319-89884-1_35

[23]

Katherine Kosaian, Yong Kiam Tan, and André Platzer. 2022. A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL. Archive of Formal Proofs, Dec., https://www.isa-afp.org/entries/Quantifier_Elimination_Hybrid.html

[24]

Wenda Li. 2014. The Sturm-Tarski Theorem. Archive of Formal Proofs, Sept., issn:2150-914x https://isa-afp.org/entries/Sturm_Tarski.html

[25]

Wenda Li, Grant Olney Passmore, and Lawrence C. Paulson. 2019. Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL. J. Autom. Reason., 62, 1 (2019), 69–91. https://doi.org/10.1007/s10817-017-9424-6

Digital Library

[26]

Wenda Li and Lawrence C. Paulson. 2016. A modular, efficient formalisation of real algebraic numbers. In CPP, Jeremy Avigad and Adam Chlipala (Eds.). ACM, 66–75. https://doi.org/10.1145/2854065.2854074

Digital Library

[27]

Assia Mahboubi. 2007. Implementing the cylindrical algebraic decomposition within the Coq system. Math. Struct. Comput. Sci., 17, 1 (2007), 99–127. https://doi.org/10.1017/S096012950600586X

Digital Library

[28]

Scott McCallum. 1985. An Improved Projection Operation for Cylindrical Algebraic Decomposition. In EUROCAL, B. F. Caviness (Ed.) (LNCS, Vol. 204). Springer, 277–278. https://doi.org/10.1007/3-540-15984-3_277

[29]

Sean McLaughlin and John Harrison. 2005. A Proof-Producing Decision Procedure for Real Arithmetic. In CADE, Robert Nieuwenhuis (Ed.) (LNCS, Vol. 3632). Springer, 295–314. https://doi.org/10.1007/11532231_22

Digital Library

[30]

César A. Muñoz, Anthony J. Narkawicz, and Aaron Dutle. 2018. A Decision Procedure for Univariate Polynomial Systems Based on Root Counting and Interval Subdivision. J. Formaliz. Reason., 11, 1 (2018), 19–41. https://doi.org/10.6092/issn.1972-5787/8212

[31]

Anthony Narkawicz, César A. Muñoz, and Aaron Dutle. 2015. Formally-Verified Decision Procedures for Univariate Polynomial Computation Based on Sturm’s and Tarski’s Theorems. J. Autom. Reason., 54, 4 (2015), 285–326. https://doi.org/10.1007/s10817-015-9320-x

Digital Library

[32]

Tobias Nipkow. 2010. Linear Quantifier Elimination. J. Autom. Reason., 45, 2 (2010), 189–212. https://doi.org/10.1007/s10817-010-9183-0

Digital Library

[33]

Lawrence C. Paulson and Jasmin Christian Blanchette. 2010. Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers. In IWIL, Geoff Sutcliffe, Stephan Schulz, and Eugenia Ternovska (Eds.) (EPiC Series in Computing, Vol. 2). EasyChair, 1–11.

[34]

André Platzer. 2018. Logical Foundations of Cyber-Physical Systems. Springer, Cham. isbn:978-3-319-63587-3 https://doi.org/10.1007/978-3-319-63588-0

[35]

André Platzer, Jan-David Quesel, and Philipp Rümmer. 2009. Real World Verification. In CADE, Renate A. Schmidt (Ed.) (LNCS, Vol. 5663). Springer, 485–501. https://doi.org/10.1007/978-3-642-02959-2_35

Digital Library

[36]

James Renegar. 1992. On the Computational Complexity and Geometry of the First-Order Theory of the Reals, Part III: Quantifier Elimination. J. Symb. Comput., 13, 3 (1992), 329–352. https://doi.org/10.1016/S0747-7171(10)80005-7

Digital Library

[37]

Matias Scharager, Katherine Cordwell, Stefan Mitsch, and André Platzer. 2021. Verified Quadratic Virtual Substitution for Real Arithmetic. In FM, Marieke Huisman, Corina S. Pasareanu, and Naijun Zhan (Eds.) (LNCS, Vol. 13047). Springer, 200–217. https://doi.org/10.1007/978-3-030-90870-6_11

Digital Library

[38]

Matias Scharager, Katherine Cordwell, Stefan Mitsch, and André Platzer. 2021. Verified Quadratic Virtual Substitution for Real Arithmetic. Archive of Formal Proofs, October, issn:2150-914x https://isa-afp.org/entries/Virtual_Substitution.html

[39]

Adam Strzeboński. 2000. Solving algebraic inequalities. The Mathematica Journal, 7, 4 (2000), 525–541.

[40]

Alfred Tarski. 1951. A Decision Method for Elementary Algebra and Geometry. RAND Corporation, Santa Monica, CA. https://www.rand.org/pubs/reports/R109.html

[41]

Volker Weispfenning. 1988. The Complexity of Linear Problems in Fields. J. Symb. Comput., 5, 1-2 (1988), 3–27. https://doi.org/10.1016/S0747-7171(88)80003-8

Digital Library

[42]

Makarius Wenzel. 2006. Structured Induction Proofs in Isabelle/Isar. In MKM, Jonathan M. Borwein and William M. Farmer (Eds.) (LNCS, Vol. 4108). Springer, 17–30. https://doi.org/10.1007/11812289_3

Digital Library

Cited By

Platzer A(2024)Hybrid Dynamical Systems Logic and Its RefinementsScience of Computer Programming10.1016/j.scico.2024.103179(103179)Online publication date: Jul-2024
https://doi.org/10.1016/j.scico.2024.103179
Platzer A(2023)Refinements of Hybrid Dynamical Systems LogicRigorous State-Based Methods10.1007/978-3-031-33163-3_1(3-14)Online publication date: 30-May-2023
https://dl.acm.org/doi/10.1007/978-3-031-33163-3_1

Index Terms

A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
1. Theory of computation
  1. Logic
    1. Logic and verification

Recommendations

Nominal Techniques in Isabelle/HOL

This paper describes a formalisation of the lambda-calculus in a HOL-based theorem prover using nominal techniques. Central to the formalisation is an inductive set that is bijective with the alpha-equated lambda-terms. Unlike de-Bruijn indices, however,...
Programming and verifying a declarative first-order prover in Isabelle/HOL

We certify in the proof assistant Isabelle/HOL the soundness of a declarative first-order prover with equality. The LCF-style prover is a translation we have made, to Standard ML, of a prover in John Harrison’s Handbook of Practical Logic and Automated ...
Completeness and Cut-elimination in the Intuitionistic Theory of Types

In this paper we define a model theory and give a semantic proof of cut-elimination for ICTT, an intuitionistic formulation of Church's theory of types defined by Miller et al. and the basis for the λProlog programming language. Our approach, extending ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CPP 2023: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs

January 2023

347 pages

ISBN:9798400700262

DOI:10.1145/3573105

General Chairs:
Robbert Krebbers
Radboud University Nijmegen, Netherlands
,
Dmitriy Traytel
University of Copenhagen, Denmark
,
Program Chairs:
Brigitte Pientka
McGill University, Canada
,
Steve Zdancewic
University of Pennsylvania, USA

Copyright © 2023 Owner/Author.

This work is licensed under a Creative Commons Attribution 4.0 International License.

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 January 2023

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Air Force Office of Scientific Research
Alexander von Humboldt Foundation
A*STAR, Singapore
National Science Foundation

Conference

CPP '23

Sponsor:

SIGPLAN

CPP '23: 12th ACM SIGPLAN International Conference on Certified Programs and Proofs

January 16 - 17, 2023

MA, Boston, USA

Acceptance Rates

Overall Acceptance Rate 18 of 26 submissions, 69%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
250
Total Downloads

Downloads (Last 12 months)103
Downloads (Last 6 weeks)19

Reflects downloads up to 31 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Platzer A(2024)Hybrid Dynamical Systems Logic and Its RefinementsScience of Computer Programming10.1016/j.scico.2024.103179(103179)Online publication date: Jul-2024
https://doi.org/10.1016/j.scico.2024.103179
Platzer A(2023)Refinements of Hybrid Dynamical Systems LogicRigorous State-Based Methods10.1007/978-3-031-33163-3_1(3-14)Online publication date: 30-May-2023
https://dl.acm.org/doi/10.1007/978-3-031-33163-3_1

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents