Real quantifier elimination in practice
An interesting problem of quantifier elimination is defined in first order logic as follows: Given a formula \(\varphi\), find a quantifier-free formula \(\varphi'\) such that both \(\varphi\) and \(\varphi'\) are equivalent in the domain of real numbers. This paper surveys the following implemented real quantifier elimination methods: partial cylindrical algebraic decomposition, virtual substitution of test terms, and combination of Gröbner basis computations with multivariate root counting. The survey starts with Descartes' rule of signs and evolves into implementations in the available packages QEPCAD, QERRC, and especially REDLOG. The applications discussed are in constraint solving, optimization, scheduling, simulation, sizing, and diagnosis, control theory and stability, real implicitization, automatic theorem proving, computer aided design, computer vision, and solid modeling, collision detection and path finding. The examples used for illustration are all quadratic. None of the surveyed methods is universally superior to the others and it may take a combination of all three to solve particular problems. For the entire collection see [Zbl 0903.00035].
- Real quantifier elimination in the RegularChains library
- scientific article; zbMATH DE number 4008374
- Real quantifier elimination is doubly exponential
- Variant real quantifier elimination: algorithm and application
- OVERCONVERGENT REAL CLOSED QUANTIFIER ELIMINATION
- Quantifier elimination for the reals with a predicate for the powers of two
- scientific article; zbMATH DE number 1794361
- Relational Methods in Computer Science
- scientific article; zbMATH DE number 4039866
- Quantifier elimination for quasi-real closed fields
- Combining logical and algebraic techniques for natural style proving in elementary analysis
- A bibliography of quantifier elimination for real closed fields
- Quantifier elimination: Optimal solution for two classical examples
- Real quantifier elimination is doubly exponential
- Reasoning over networks by symbolic methods
- Testing stability by quantifier elimination
- Linear problems in valued fields
- New techniques for linear arithmetic: cubes and equalities
- A survey of some methods for real quantifier elimination, decision, and satisfiability and their applications
- On solving parametric polynomial systems
- Algorithmic reduction of biological networks with multiple time scales
- On generalizing Descartes' rule of signs to hypersurfaces
- On quantified linear implications
- Real quantifier elimination for the synthesis of optimal numerical algorithms (case study: square root computation)
- Efficient subformula orders for real quantifier elimination of non-prenex formulas
- Real quantifier elimination in the RegularChains library
- Variant real quantifier elimination: algorithm and application
- Adapting real quantifier elimination methods for conflict set computation
- Virtual substitution for SMT-solving
- Recent advances in real geometric reasoning
- Synthesis of optimal numerical algorithms using real quantifier elimination (case study: square root computation)
- Local quantifier elimination
- Extending a Resolution Prover for Inequalities on Elementary Functions
- Efficient Preprocessing Methods for Quantifier Elimination
- New Domains for Applied Quantifier Elimination
- Verifying Mixed Real-Integer Quantifier Elimination
- An effective implementation of symbolic-numeric cylindrical algebraic decomposition for quantifier elimination
- On the complexity of quantified linear systems
- Variant quantifier elimination
- scientific article; zbMATH DE number 1263329 (Why is no real title available?)
- scientific article; zbMATH DE number 1263423 (Why is no real title available?)
- Quantifier-free encoding of invariants for hybrid systems
- scientific article; zbMATH DE number 2090033 (Why is no real title available?)
- A complexity perspective on entailment of parameterized linear constraints
- Proving inequalities and solving global optimization problems via simplified CAD projection
- Solving geometric problems with real quantifier elimination
- Formula Simplification for Real Quantifier Elimination Using Geometric Invariance
- Analyzing restricted fragments of the theory of linear arithmetic
- An effective implementation of a special quantifier elimination for a sign definite condition by logical formula simplification
- Direct formal verification of liveness properties in continuous and hybrid dynamical systems
- Verification and synthesis using real quantifier elimination
- Quantifier Elimination for Quartics
- Algorithmic global criteria for excluding oscillations
- Automatic Discovery of Geometry Theorems Using Minimal Canonical Comprehensive Gröbner Systems
- Quantifier elimination on real closed fields and differential equations
- Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition
- MetiTarski: An Automatic Prover for the Elementary Functions
- Combining Isabelle and QEPCAD-B in the Prover’s Palette
- Timed Basic Parallel Processes
- Cylindrical algebraic decomposition using local projections
- Computing with Tarski formulas and semi-algebraic sets in a web browser
- Quantifier elimination for real algebra -- the quadratic case and beyond
- VIRAS: conflict-driven quantifier elimination for integer-real arithmetic
- On the number of real types of univariate polynomials
- Parametric toricity of steady state varieties of reaction networks
- Better answers to real questions
- Weak quantifier elimination for the full linear theory of the integers
- MetiTarski: An automatic theorem prover for real-valued special functions
This page was built for publication: Real quantifier elimination in practice
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4247790)
