Quantifier elimination for real algebra -- the quadratic case and beyond

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

QEPCAD
REDUCE
REDLOG

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)