Abstract: We consider existential problems over the reals. Extended quantifier elimination generalizes the concept of regular quantifier elimination by providing in addition answers, which are descriptions of possible assignments for the quantified variables. Implementations of extended quantifier elimination via virtual substitution have been successfully applied to various problems in science and engineering. So far, the answers produced by these implementations included infinitesimal and infinite numbers, which are hard to interpret in practice. We introduce here a post-processing procedure to convert, for fixed parameters, all answers into standard real numbers. The relevance of our procedure is demonstrated by application of our implementation to various examples from the literature, where it significantly improves the quality of the results.
Recommendations
Cites work
- scientific article; zbMATH DE number 1574492 (Why is no real title available?)
- scientific article; zbMATH DE number 1189070 (Why is no real title available?)
- scientific article; zbMATH DE number 1262432 (Why is no real title available?)
- scientific article; zbMATH DE number 1263423 (Why is no real title available?)
- scientific article; zbMATH DE number 1302474 (Why is no real title available?)
- scientific article; zbMATH DE number 1878556 (Why is no real title available?)
- A new approach for automatic theorem proving in real geometry
- Algorithmic global criteria for excluding oscillations
- Applying Linear Quantifier Elimination
- Conflict Resolution
- Deciding Hopf bifurcations by quantifier elimination in a software-component architecture
- Detection of Hopf bifurcations in chemical reaction networks using convex coordinates
- Efficient methods to compute Hopf bifurcations in chemical reaction networks using reaction coordinates
- Investigating Generic Methods to Solve Hopf Bifurcation Problems in Algebraic Biology
- Investigating algebraic and logical algorithms to solve Hopf bifurcation problems in algebraic biology
- Linear and quadratic complexity bounds on the values of the positive roots of polynomials
- Linear problems in valued fields
- On Proving the Absence of Oscillations in Models of Genetic Circuits
- Parametric quantified SAT solving
- Quantifier elimination for real algebra -- the quadratic case and beyond
- Reasoning over networks by symbolic methods
- Semilinear motion planning in REDLOG
- Simplification by Cooperating Decision Procedures
- Simplification of quantifier-free formulae over ordered fields
- Simulation and optimization by quantifier elimination
- Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
- The complexity of linear problems in fields
- Toric ideals and graph theory to analyze Hopf bifurcations in mass action systems
- Verification and synthesis using real quantifier elimination
- Weak quantifier elimination for the full linear theory of the integers
Cited in
(4)
This page was built for publication: Better answers to real questions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q898260)
