Better answers to real questions

DOI10.1016/J.JSC.2015.07.002zbMATH Open1346.68290arXiv1501.05098OpenAlexW2129922110MaRDI QIDQ898260FDOQ898260

Authors: Marek Košta, Thomas Sturm, Andreas Dolzmann 

Publication date: 8 December 2015

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1501.05098

Recommendations

• Quantifier elimination for real algebra -- the quadratic case and beyond
• Computer Science Logic
• scientific article; zbMATH DE number 1302474
• Variant quantifier elimination
• scientific article; zbMATH DE number 1263423

zbMATH Keywords

existential problemsextended quantifier eliminationvirtual substitution

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Quantifier elimination, model completeness, and related topics (03C10)

Cites Work

• Title not available (Why is that?)
• Toric ideals and graph theory to analyze Hopf bifurcations in mass action systems
• Simplification by Cooperating Decision Procedures
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Conflict Resolution
• The complexity of linear problems in fields
• Simplification of quantifier-free formulae over ordered fields
• Deciding Hopf bifurcations by quantifier elimination in a software-component architecture
• Detection of Hopf bifurcations in chemical reaction networks using convex coordinates
• Investigating Generic Methods to Solve Hopf Bifurcation Problems in Algebraic Biology
• On Proving the Absence of Oscillations in Models of Genetic Circuits
• Investigating algebraic and logical algorithms to solve Hopf bifurcation problems in algebraic biology
• Quantifier elimination for real algebra -- the quadratic case and beyond
• Weak quantifier elimination for the full linear theory of the integers
• Title not available (Why is that?)
• Efficient methods to compute Hopf bifurcations in chemical reaction networks using reaction coordinates
• Simulation and optimization by quantifier elimination
• Applying Linear Quantifier Elimination
• Title not available (Why is that?)
• A new approach for automatic theorem proving in real geometry
• Algorithmic global criteria for excluding oscillations
• Verification and synthesis using real quantifier elimination
• Linear and quadratic complexity bounds on the values of the positive roots of polynomials
• Reasoning over networks by symbolic methods
• Linear problems in valued fields
• Title not available (Why is that?)
• Parametric quantified SAT solving
• Title not available (Why is that?)
• Title not available (Why is that?)
• Semilinear motion planning in REDLOG

Cited In (4)

• Parametric toricity of steady state varieties of reaction networks
• Answers that Have Integrity
• A survey of some methods for real quantifier elimination, decision, and satisfiability and their applications
• Efficiently and effectively recognizing toricity of steady state varieties

Uses Software

• REDLOG

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)