Real quantifier elimination is doubly exponential

Analysis of algorithms and problem complexity (68Q25) Symbolic computation and algebraic computation (68W30) Decidability and field theory (12L05) Quantifier elimination, model completeness, and related topics (03C10) Real and complex fields (12D99)

Related Items

Erratum to: ``Analyzing restricted fragments of the theory of linear arithmetic ⋮ Computing the shape of the image of a multi-linear mapping is possible but computationally intractable: Theorems ⋮ Testing binomiality of chemical reaction networks using comprehensive Gröbner systems ⋮ Separation of complexity classes in Koiran's weak model ⋮ Automatic computation of the complete root classification for a parametric polynomial ⋮ Recent Advances in Real Geometric Reasoning ⋮ 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 ⋮ A bibliography of quantifier elimination for real closed fields ⋮ The saddle point problem of polynomials ⋮ Detection of Hopf bifurcations in chemical reaction networks using convex coordinates ⋮ Recent advances in program verification through computer algebra ⋮ An approximate characterisation of the set of feasible trajectories for constrained flat systems ⋮ A symbolic-numeric approach to multi-objective optimization in manufacturing design ⋮ An effective implementation of symbolic-numeric cylindrical algebraic decomposition for quantifier elimination ⋮ Unnamed Item ⋮ From LP to LP: Programming with constraints ⋮ On the complexity of quantified linear systems ⋮ Subquadratic algorithms for algebraic 3SUM ⋮ Positive dimensional parametric polynomial systems, connectivity queries and applications in robotics ⋮ Bellerophon: tactical theorem proving for hybrid systems ⋮ raSAT: an SMT solver for polynomial constraints ⋮ A Unified Approach to Unimodality of Gaussian Polynomials ⋮ Faster real root decision algorithm for symmetric polynomials ⋮ A new probabilistic constraint logic programming language based on a generalised distribution semantics ⋮ Automated repair for timed systems ⋮ Proving an execution of an algorithm correct? ⋮ An Elementary Recursive Bound for Effective Positivstellensatz and Hilbert’s 17th problem ⋮ 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 ⋮ Polynomial Bell Inequalities ⋮ Is computer algebra ready for conjecturing and proving geometric inequalities in the classroom? ⋮ Adapting Real Quantifier Elimination Methods for Conflict Set Computation ⋮ A survey of some methods for real quantifier elimination, decision, and satisfiability and their applications ⋮ Automatically discovering relaxed Lyapunov functions for polynomial dynamical systems ⋮ A complex analogue of Toda's theorem ⋮ Unnamed Item ⋮ Cylindrical algebraic sub-decompositions ⋮ Computational tools for solving a marginal problem with applications in Bell non-locality and causal modeling ⋮ A singly exponential stratification scheme for real semi-algebraic varieties and its applications ⋮ Can an A.I. win a medal in the mathematical olympiad? – Benchmarking mechanized mathematics on pre-university problems1 ⋮ A complexity perspective on entailment of parameterized linear constraints ⋮ Proving inequalities and solving global optimization problems via simplified CAD projection ⋮ Partial cylindrical algebraic decomposition for quantifier elimination ⋮ Testing elementary function identities using CAD ⋮ Computational complexity of determining which statements about causality hold in different space-time models ⋮ Encoding OCL Data Types for SAT-Based Verification of UML/OCL Models ⋮ ModelPlex: verified runtime validation of verified cyber-physical system models ⋮ Analyzing restricted fragments of the theory of linear arithmetic ⋮ A search-based procedure for nonlinear real arithmetic ⋮ Comprehensive Gröbner bases ⋮ Automatic generation of bounds for polynomial systems with application to the Lorenz system ⋮ Elementary recursive quantifier elimination based on Thom encoding and sign determination ⋮ On quantified linear implications ⋮ A DECISION PROCEDURE FOR PROBABILITY CALCULUS WITH APPLICATIONS ⋮ Algorithmic global criteria for excluding oscillations ⋮ Using machine learning to improve cylindrical algebraic decomposition ⋮ 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 ⋮ Real World Verification ⋮ Unnamed Item ⋮ Some lower bounds for the complexity of the linear programming feasibility problem over the reals ⋮ Efficiently and effectively recognizing toricity of steady state varieties ⋮ Truth table invariant cylindrical algebraic decomposition ⋮ Direct Formal Verification of Liveness Properties in Continuous and Hybrid Dynamical Systems ⋮ Lower bounds for arithmetic networks ⋮ $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation ⋮ Sur la complexité du principe de Tarski-Seidenberg ⋮ Need Polynomial Systems Be Doubly-Exponential? ⋮ Virtual Substitution for SMT-Solving ⋮ Combined Decision Techniques for the Existential Theory of the Reals ⋮ Cylindrical algebraic decomposition with equational constraints ⋮ On the parallel complexity of the polynomial ideal membership problem ⋮ 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 ⋮ Explicit description of 2D parametric solution sets ⋮ Unnamed Item ⋮ Synthesizing Switching Controllers for Hybrid Systems by Generating Invariants ⋮ Globally Optimizing Small Codes in Real Projective Spaces ⋮ Special algorithm for stability analysis of multistable biological regulatory systems ⋮ 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 ⋮ Computing real witness points of positive dimensional polynomial systems

Cites Work