Quantifier elimination for real algebra -- the quadratic case and beyond
DOI10.1007/S002000050055zbMATH Open0867.03003OpenAlexW2040951317MaRDI QIDQ677553FDOQ677553
Publication date: 4 August 1997
Published in: Applicable Algebra in Engineering, Communication and Computing (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s002000050055
constraint solvingREDUCEfirst-order theory of real numbersquantifier elimination methodREDLOG package
Analysis of algorithms and problem complexity (68Q25) Symbolic computation and algebraic computation (68W30) Mechanization of proofs and logical operations (03B35) Quantifier elimination, model completeness, and related topics (03C10)
Cited In (66)
- Effective Quantifier Elimination for Presburger Arithmetic with Infinity
- Verified Quadratic Virtual Substitution for Real Arithmetic
- Experiments with automated reasoning in the class
- I-RiSC: An SMT-Compliant Solver for the Existential Fragment of Real Algebra
- Local search for solving satisfiability of polynomial formulas
- Satisfiability modulo finite fields
- Editorial: Symbolic computation and satisfiability checking
- Supporting Global Numerical Optimization of Rational Functions by Generic Symbolic Convexity Tests
- Optimization modulo non-linear arithmetic via incremental linearization
- Parametric toricity of steady state varieties of reaction networks
- Better answers to real questions
- Satisfiability Checking: Theory and Applications
- Solution formulas for cubic equations without or with constraints
- $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation
- Fast simplifications for Tarski formulas based on monomial inequalities
- Application of quantifier elimination to inverse buckling problems
- Parametric Qualitative Analysis of Ordinary Differential Equations: Computer Algebra Methods for Excluding Oscillations (Extended Abstract) (Invited Talk)
- A survey of some methods for real quantifier elimination, decision, and satisfiability and their applications
- Real World Verification
- Simple CAD construction and its applications
- SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
- A logic based approach to finding real singularities of implicit ordinary differential equations
- Multiple object semilinear motion planning
- Quantified constraints under perturbation
- Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
- Efficiently and effectively recognizing toricity of steady state varieties
- Algorithmic reduction of biological networks with multiple time scales
- An effective implementation of symbolic-numeric cylindrical algebraic decomposition for quantifier elimination
- Adapting Real Quantifier Elimination Methods for Conflict Set Computation
- Formula Simplification for Real Quantifier Elimination Using Geometric Invariance
- Investigating Generic Methods to Solve Hopf Bifurcation Problems in Algebraic Biology
- Identifying the parametric occurrence of multiple steady states for some biological networks
- Template polyhedra and bilinear optimization
- Generating invariants for non-linear hybrid systems
- On a decision procedure for quantified linear programs
- Discussion on: ``Stabilisability and stability for explicit and implicit polynomial systems: A symbolic computation approach by D. Nešić and I. M. Y. Mareels
- Algorithmic global criteria for excluding oscillations
- A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic
- Endomorphisms for Non-trivial Non-linear Loop Invariant Generation
- Finding at least one point in each connected component of a real algebraic set defined by a single equation
- Solving Nonlinear Integer Arithmetic with MCSAT
- Quantifier elimination in automatic loop parallelization
- Combining logical and algebraic techniques for natural style proving in elementary analysis
- Certified Reasoning with Infinity
- Quantifier elimination for a class of exponential polynomial formulas
- CGSQE/SyNRAC
- Generating invariants for non-linear loops by linear algebraic methods
- Detection of Hopf bifurcations in chemical reaction networks using convex coordinates
- Stability analysis for discrete biological models using algebraic methods
- Validating numerical semidefinite programming solvers for polynomial invariants
- Weak quantifier elimination for the full linear theory of the integers
- Automatic derivation of positivity conditions inside boundary elements with the help of the REDLOG computer logic package.
- Real quantifier elimination is doubly exponential
- A Quantifier Elimination Algorithm for Linear Real Arithmetic
- The Strategy Challenge in SMT Solving
- The Lee identities in topoi. I
- Fast theorem-proving and Wu's method
- Quantifier elimination for trigonometric polynomials by cylindrical trigonometric decomposition
- Cylindrical algebraic decomposition using local projections
- Computing Hopf Bifurcations in Chemical Reaction Networks Using Reaction Coordinates
- Modular strategic SMT solving with \textbf{SMT-RAT}
- An empirical analysis of algorithms for partially Clairvoyant scheduling
- Quantifier elimination supported proofs in the numerical treatment of fluid flows
- Deciding Hopf bifurcations by quantifier elimination in a software-component architecture
- Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)
- Combined Decision Techniques for the Existential Theory of the Reals
Uses Software
This page was built for publication: Quantifier elimination for real algebra -- the quadratic case and beyond
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q677553)