Real quantifier elimination is doubly exponential
From MaRDI portal
Publication:1114669
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
- scientific article; zbMATH DE number 3497890 (Why is no real title available?)
- scientific article; zbMATH DE number 3068536 (Why is no real title available?)
- Computer algebra applied to itself
- Definability and fast quantifier elimination in algebraically closed fields
- The complexity of elementary algebra and geometry
Cited in
(96)- Synthesizing switching controllers for hybrid systems by generating invariants
- On the complexity of quantified linear systems
- Combined Decision Techniques for the Existential Theory of the Reals
- Recent advances in real geometric reasoning
- 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
- The saddle point problem of polynomials
- scientific article; zbMATH DE number 7559240 (Why is no real title available?)
- Polynomial Bell inequalities
- Subquadratic algorithms for algebraic 3SUM
- Virtual substitution for SMT-solving
- Adapting real quantifier elimination methods for conflict set computation
- Using machine learning to improve cylindrical algebraic decomposition
- The complexity of the Hausdorff distance
- A bibliography of quantifier elimination for real closed fields
- Automatically discovering relaxed Lyapunov functions for polynomial dynamical systems
- Solving parametric systems of polynomial equations over the reals through Hermite matrices
- 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
- Testing binomiality of chemical reaction networks using comprehensive Gröbner systems
- Need polynomial systems be doubly-exponential?
- On the parallel complexity of the polynomial ideal membership problem
- Computational tools for solving a marginal problem with applications in Bell non-locality and causal modeling
- Cylindrical algebraic decomposition with equational constraints
- A survey of some methods for real quantifier elimination, decision, and satisfiability and their applications
- scientific article; zbMATH DE number 4008374 (Why is no real title available?)
- Partial cylindrical algebraic decomposition for quantifier elimination
- Sur la complexité du principe de Tarski-Seidenberg
- Automatic computation of the complete root classification for a parametric polynomial
- On quantified linear implications
- Parametric Qualitative Analysis of Ordinary Differential Equations: Computer Algebra Methods for Excluding Oscillations (Extended Abstract) (Invited Talk)
- Is computer algebra ready for conjecturing and proving geometric inequalities in the classroom?
- Direct formal verification of liveness properties in continuous and hybrid dynamical systems
- Real World Verification
- A singly exponential stratification scheme for real semi-algebraic varieties and its applications
- From LP to LP: Programming with constraints
- Automatic generation of bounds for polynomial systems with application to the Lorenz system
- Some lower bounds for the complexity of the linear programming feasibility problem over the reals
- Efficiently and effectively recognizing toricity of steady state varieties
- An effective implementation of symbolic-numeric cylindrical algebraic decomposition for quantifier elimination
- Can one design a geometry engine? Can one design a geometry engine? On the (un)decidability of certain affine Euclidean geometries
- Proving inequalities and solving global optimization problems via simplified CAD projection
- Quantifier elimination for the reals with a predicate for the powers of two
- The complexity of cylindrical algebraic decomposition with respect to polynomial degree
- Separation of complexity classes in Koiran's weak model
- Globally optimizing small codes in real projective spaces
- A complex analogue of Toda's theorem
- Parallel running of a modular simulation scheme
- Erratum to: ``Analyzing restricted fragments of the theory of linear arithmetic
- Efficient simplification techniques for special real quantifier elimination with applications to the synthesis of optimal numerical algorithms
- Definability and fast quantifier elimination in algebraically closed fields
- Special algorithm for stability analysis of multistable biological regulatory systems
- Algorithmic global criteria for excluding oscillations
- raSAT: an SMT solver for polynomial constraints
- Explicit description of 2D parametric solution sets
- Comprehensive Gröbner bases
- A new probabilistic constraint logic programming language based on a generalised distribution semantics
- Completeness for the complexity class \(\forall \exists \mathbb{R}\) and area-universality
- scientific article; zbMATH DE number 7471675 (Why is no real title available?)
- Computing the shape of the image of a multi-linear mapping is possible but computationally intractable: Theorems
- Faster real root decision algorithm for symmetric polynomials
- Cylindrical algebraic sub-decompositions
- An approximate characterisation of the set of feasible trajectories for constrained flat systems
- Constrained neural networks for interpretable heuristic creation to optimise computer algebra systems
- A complexity perspective on entailment of parameterized linear constraints
- Positive dimensional parametric polynomial systems, connectivity queries and applications in robotics
- Supporting global numerical optimization of rational functions by generic symbolic convexity tests
- Detection of Hopf bifurcations in chemical reaction networks using convex coordinates
- Recent advances in program verification through computer algebra
- Truth table invariant cylindrical algebraic decomposition
- A symbolic-numeric approach to multi-objective optimization in manufacturing design
- Computing real witness points of positive dimensional polynomial systems
- Lessons on datasets and paradigms in machine learning for symbolic computation: a case study on CAD
- Parametric root finding for supporting proving and discovering geometric inequalities in GeoGebra
- Supporting proving and discovering geometric inequalities in GeoGebra by using Tarski
- Encoding OCL data types for SAT-based verification of UML/OCL models
- A Unified Approach to Unimodality of Gaussian Polynomials
- Automated repair for timed systems
- Analyzing restricted fragments of the theory of linear arithmetic
- Lower bounds for arithmetic networks
- Faster one block quantifier elimination for regular polynomial systems of equations
- scientific article; zbMATH DE number 1383827 (Why is no real title available?)
- Computational complexity of determining which statements about causality hold in different space-time models
- Bellerophon: tactical theorem proving for hybrid systems
- \textsf{SC}\(^2\): satisfiability checking meets symbolic computation. (Project paper)
- A search-based procedure for nonlinear real arithmetic
- scientific article; zbMATH DE number 1302474 (Why is no real title available?)
- Testing elementary function identities using CAD
- An elementary recursive bound for effective Positivstellensatz and Hilbert's 17th problem
- scientific article; zbMATH DE number 3920550 (Why is no real title available?)
- Proving an execution of an algorithm correct?
- ModelPlex: verified runtime validation of verified cyber-physical system models
- Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)
- A decision procedure for probability calculus with applications
- Elementary recursive quantifier elimination based on Thom encoding and sign determination
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)
