Real quantifier elimination is doubly exponential
From MaRDI portal
Publication:1114669
The authors show that quantifier elimination over the first-order theory of real-closed fields can require doubly-exponential space (and hence time) and show that this doubly-exponential behaviour is intrinsic to the problem. This result has already been proved by Weispfenning by a completely different method in 1985, but the method of the paper is of independent interest.
Recommendations
- scientific article; zbMATH DE number 1302474
- Quantifier elimination for the reals with a predicate for the powers of two
- Real quantifier elimination in the RegularChains library
- OVERCONVERGENT REAL CLOSED QUANTIFIER ELIMINATION
- scientific article; zbMATH DE number 4008374
- Variant real quantifier elimination: algorithm and application
- Counterexamples to quantifier elimination for fewnomial and exponential expressions
- Quantifier elimination for real algebra -- the quadratic case and beyond
- scientific article; zbMATH DE number 1794361
- A Quantifier Elimination Algorithm for Linear Real Arithmetic
Cites work
- Computer algebra applied to itself
- Definability and fast quantifier elimination in algebraically closed fields
- scientific article; zbMATH DE number 3497890 (Why is no real title available?)
- scientific article; zbMATH DE number 3068536 (Why is no real title available?)
- The complexity of elementary algebra and geometry
Cited in
(only showing first 100 items - show all)- A bibliography of quantifier elimination for real closed fields
- A singly exponential stratification scheme for real semi-algebraic varieties and its applications
- Partial cylindrical algebraic decomposition for quantifier elimination
- Comprehensive Gröbner bases
- On the parallel complexity of the polynomial ideal membership problem
- Separation of complexity classes in Koiran's weak model
- Bellerophon: tactical theorem proving for hybrid systems
- raSAT: an SMT solver for polynomial constraints
- A survey of some methods for real quantifier elimination, decision, and satisfiability and their applications
- Automatic generation of bounds for polynomial systems with application to the Lorenz system
- Lower bounds for arithmetic networks
- Automatically discovering relaxed Lyapunov functions for polynomial dynamical systems
- Using machine learning to improve cylindrical algebraic decomposition
- Efficiently and effectively recognizing toricity of steady state varieties
- Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)
- Solving parametric systems of polynomial equations over the reals through Hermite matrices
- The saddle point problem of polynomials
- An approximate characterisation of the set of feasible trajectories for constrained flat systems
- On quantified linear implications
- Cylindrical algebraic decomposition with equational constraints
- Special algorithm for stability analysis of multistable biological regulatory systems
- Computing real witness points of positive dimensional polynomial systems
- Erratum to: ``Analyzing restricted fragments of the theory of linear arithmetic
- Subquadratic algorithms for algebraic 3SUM
- Can one design a geometry engine? Can one design a geometry engine? On the (un)decidability of certain affine Euclidean geometries
- Parallel running of a modular simulation scheme
- Positive dimensional parametric polynomial systems, connectivity queries and applications in robotics
- \textsf{SC}\(^2\): satisfiability checking meets symbolic computation. (Project paper)
- Need polynomial systems be doubly-exponential?
- The complexity of cylindrical algebraic decomposition with respect to polynomial degree
- Efficient simplification techniques for special real quantifier elimination with applications to the synthesis of optimal numerical algorithms
- Synthesizing switching controllers for hybrid systems by generating invariants
- Polynomial Bell inequalities
- Adapting real quantifier elimination methods for conflict set computation
- Encoding OCL data types for SAT-based verification of UML/OCL models
- Virtual substitution for SMT-solving
- Recent advances in real geometric reasoning
- Detection of Hopf bifurcations in chemical reaction networks using convex coordinates
- Recent advances in program verification through computer algebra
- A decision procedure for probability calculus with applications
- Parametric Qualitative Analysis of Ordinary Differential Equations: Computer Algebra Methods for Excluding Oscillations (Extended Abstract) (Invited Talk)
- Supporting global numerical optimization of rational functions by generic symbolic convexity tests
- A symbolic-numeric approach to multi-objective optimization in manufacturing design
- Combined Decision Techniques for the Existential Theory of the Reals
- scientific article; zbMATH DE number 3920550 (Why is no real title available?)
- scientific article; zbMATH DE number 4008374 (Why is no real title available?)
- An effective implementation of symbolic-numeric cylindrical algebraic decomposition for quantifier elimination
- On the complexity of quantified linear systems
- scientific article; zbMATH DE number 1302474 (Why is no real title available?)
- Computing the shape of the image of a multi-linear mapping is possible but computationally intractable: Theorems
- A complex analogue of Toda's theorem
- Computational tools for solving a marginal problem with applications in Bell non-locality and causal modeling
- Sur la complexité du principe de Tarski-Seidenberg
- scientific article; zbMATH DE number 1383827 (Why is no real title available?)
- Cylindrical algebraic sub-decompositions
- A complexity perspective on entailment of parameterized linear constraints
- Proving inequalities and solving global optimization problems via simplified CAD projection
- A probabilistic higher-order fixpoint logic
- scientific article; zbMATH DE number 7559240 (Why is no real title available?)
- From LP to LP: Programming with constraints
- An elementary recursive bound for effective Positivstellensatz and Hilbert's 17th problem
- Analyzing restricted fragments of the theory of linear arithmetic
- On the complexity of computing a random Boolean function over the reals
- Can an A.I. win a medal in the mathematical olympiad? -- Benchmarking mechanized mathematics on pre-university problems
- A search-based procedure for nonlinear real arithmetic
- Real World Verification
- Direct formal verification of liveness properties in continuous and hybrid dynamical systems
- Elementary recursive quantifier elimination based on Thom encoding and sign determination
- Algorithmic global criteria for excluding oscillations
- Globally optimizing small codes in real projective spaces
- Truth table invariant cylindrical algebraic decomposition
- A Unified Approach to Unimodality of Gaussian Polynomials
- Faster real root decision algorithm for symmetric polynomials
- Automated repair for timed systems
- Proving an execution of an algorithm correct?
- The complexity of the Hausdorff distance
- Punctually presented structures I: Closure theorems
- Explainable AI insights for symbolic computation: a case study on selecting the variable ordering for cylindrical algebraic decomposition
- Levelwise construction of a single cylindrical algebraic cell
- Completeness for the complexity class \(\forall \exists \mathbb{R}\) and area-universality
- Is computer algebra ready for conjecturing and proving geometric inequalities in the classroom?
- Constrained neural networks for interpretable heuristic creation to optimise computer algebra systems
- Lessons on datasets and paradigms in machine learning for symbolic computation: a case study on CAD
- Supporting proving and discovering geometric inequalities in GeoGebra by using Tarski
- Parametric root finding for supporting proving and discovering geometric inequalities in GeoGebra
- Faster one block quantifier elimination for regular polynomial systems of equations
- ModelPlex: verified runtime validation of verified cyber-physical system models
- Relatively complete and efficient partial quantifier elimination
- SMT and functional equation solving over the reals: challenges from the IMO
- Multistability of small zero-one reaction networks
- Quantifier elimination for normal cone computations
- Quantitative approximate definable choices
- SMT solving over finite field arithmetic
- Solving parameter-dependent semi-algebraic systems
- A decision method for first-order stream logic
- A geometric approach to cylindrical algebraic decomposition
- On the First Derivative Bounds for Rational Bézier Curves
- Explicit description of 2D parametric solution sets
- Definability and fast quantifier elimination in algebraically closed fields
- Testing binomiality of chemical reaction networks using comprehensive Gröbner systems
This page was built for publication: Real quantifier elimination is doubly exponential
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1114669)
