Real quantifier elimination is doubly exponential
From MaRDI portal
Publication:1114669
DOI10.1016/S0747-7171(88)80004-XzbMATH Open0663.03015WikidataQ56455152 ScholiaQ56455152MaRDI QIDQ1114669FDOQ1114669
Authors: Joos Heintz, James H. Davenport 
Publication date: 1988
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
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
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)
Cites Work
Cited In (96)
- On the complexity of quantified linear systems
- Can an A.I. win a medal in the mathematical olympiad? -- Benchmarking mechanized mathematics on pre-university problems
- The saddle point problem of polynomials
- 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
- A bibliography of quantifier elimination for real closed fields
- Automatically discovering relaxed Lyapunov functions for polynomial dynamical systems
- Need polynomial systems be doubly-exponential?
- Cylindrical algebraic decomposition with equational constraints
- Testing binomiality of chemical reaction networks using comprehensive Gröbner systems
- On the parallel complexity of the polynomial ideal membership problem
- Title not available (Why is that?)
- Direct formal verification of liveness properties in continuous and hybrid dynamical systems
- A survey of some methods for real quantifier elimination, decision, and satisfiability and their applications
- Real World Verification
- On quantified linear implications
- 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
- Automatic generation of bounds for polynomial systems with application to the Lorenz system
- A singly exponential stratification scheme for real semi-algebraic varieties and its applications
- 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
- The complexity of cylindrical algebraic decomposition with respect to polynomial degree
- Proving inequalities and solving global optimization problems via simplified CAD projection
- Quantifier elimination for the reals with a predicate for the powers of two
- Separation of complexity classes in Koiran's weak model
- A complex analogue of Toda's theorem
- Special algorithm for stability analysis of multistable biological regulatory systems
- Definability and fast quantifier elimination in algebraically closed fields
- 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
- Cylindrical algebraic sub-decompositions
- A complexity perspective on entailment of parameterized linear constraints
- Truth table invariant cylindrical algebraic decomposition
- Detection of Hopf bifurcations in chemical reaction networks using convex coordinates
- Recent advances in program verification through computer algebra
- A symbolic-numeric approach to multi-objective optimization in manufacturing design
- Computing real witness points of positive dimensional polynomial systems
- Encoding OCL data types for SAT-based verification of UML/OCL models
- Lower bounds for arithmetic networks
- Analyzing restricted fragments of the theory of linear arithmetic
- Computational complexity of determining which statements about causality hold in different space-time models
- \textsf{SC}\(^2\): satisfiability checking meets symbolic computation. (Project paper)
- Bellerophon: tactical theorem proving for hybrid systems
- Title not available (Why is that?)
- An elementary recursive bound for effective Positivstellensatz and Hilbert's 17th problem
- A search-based procedure for nonlinear real arithmetic
- Title not available (Why is that?)
- Testing elementary function identities using CAD
- A decision procedure for probability calculus with applications
- Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)
- ModelPlex: verified runtime validation of verified cyber-physical system models
- Combined Decision Techniques for the Existential Theory of the Reals
- On the complexity of computing a random Boolean function over the reals
- Elementary recursive quantifier elimination based on Thom encoding and sign determination
- Title not available (Why is that?)
- 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
- Solving parametric systems of polynomial equations over the reals through Hermite matrices
- Computational tools for solving a marginal problem with applications in Bell non-locality and causal modeling
- Is computer algebra ready for conjecturing and proving geometric inequalities in the classroom?
- Parametric Qualitative Analysis of Ordinary Differential Equations: Computer Algebra Methods for Excluding Oscillations (Extended Abstract) (Invited Talk)
- From LP to LP: Programming with constraints
- Can one design a geometry engine? Can one design a geometry engine? On the (un)decidability of certain affine Euclidean geometries
- Globally optimizing small codes in real projective spaces
- 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
- Completeness for the complexity class \(\forall \exists \mathbb{R}\) and area-universality
- Title not available (Why is that?)
- Faster real root decision algorithm for symmetric polynomials
- Computing the shape of the image of a multi-linear mapping is possible but computationally intractable: Theorems
- 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
- Supporting global numerical optimization of rational functions by generic symbolic convexity tests
- Positive dimensional parametric polynomial systems, connectivity queries and applications in robotics
- 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
- A Unified Approach to Unimodality of Gaussian Polynomials
- Automated repair for timed systems
- Faster one block quantifier elimination for regular polynomial systems of equations
- Title not available (Why is that?)
- Proving an execution of an algorithm correct?
- Synthesizing switching controllers for hybrid systems by generating invariants
- Recent advances in real geometric reasoning
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)
