Quantifier elimination for real algebra -- the quadratic case and beyond
From MaRDI portal
Publication:677553
DOI10.1007/s002000050055zbMath0867.03003OpenAlexW2040951317MaRDI QIDQ677553
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
REDUCEREDLOG packageconstraint solvingfirst-order theory of real numbersquantifier elimination method
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (60)
Optimization modulo non-linear arithmetic via incremental linearization ⋮ Parametric toricity of steady state varieties of reaction networks ⋮ SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving ⋮ Computing Hopf Bifurcations in Chemical Reaction Networks Using Reaction Coordinates ⋮ Detection of Hopf bifurcations in chemical reaction networks using convex coordinates ⋮ The Lee identities in topoi. I ⋮ Stability analysis for discrete biological models using algebraic methods ⋮ Satisfiability Checking: Theory and Applications ⋮ An effective implementation of symbolic-numeric cylindrical algebraic decomposition for quantifier elimination ⋮ Modular strategic SMT solving with \textbf{SMT-RAT} ⋮ Experiments with automated reasoning in the class ⋮ Better answers to real questions ⋮ Fast simplifications for Tarski formulas based on monomial inequalities ⋮ Solving Nonlinear Integer Arithmetic with MCSAT ⋮ Generating invariants for non-linear loops by linear algebraic methods ⋮ Adapting Real Quantifier Elimination Methods for Conflict Set Computation ⋮ A survey of some methods for real quantifier elimination, decision, and satisfiability and their applications ⋮ CGSQE/SyNRAC ⋮ Fast theorem-proving and Wu's method ⋮ Quantifier elimination for a class of exponential polynomial formulas ⋮ Quantifier elimination in automatic loop parallelization ⋮ Multiple object semilinear motion planning ⋮ On a decision procedure for quantified linear programs ⋮ Weak quantifier elimination for the full linear theory of the integers ⋮ Quantifier elimination supported proofs in the numerical treatment of fluid flows ⋮ Application of quantifier elimination to inverse buckling problems ⋮ I-RiSC: An SMT-Compliant Solver for the Existential Fragment of Real Algebra ⋮ The Strategy Challenge in SMT Solving ⋮ Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings ⋮ Finding at least one point in each connected component of a real algebraic set defined by a single equation ⋮ An empirical analysis of algorithms for partially Clairvoyant scheduling ⋮ Algorithmic global criteria for excluding oscillations ⋮ Solution formulas for cubic equations without or with constraints ⋮ Simple CAD construction and its applications ⋮ Parametric Qualitative Analysis of Ordinary Differential Equations: Computer Algebra Methods for Excluding Oscillations (Extended Abstract) (Invited Talk) ⋮ Supporting Global Numerical Optimization of Rational Functions by Generic Symbolic Convexity Tests ⋮ Investigating Generic Methods to Solve Hopf Bifurcation Problems in Algebraic Biology ⋮ Real World Verification ⋮ Validating numerical semidefinite programming solvers for polynomial invariants ⋮ Identifying the parametric occurrence of multiple steady states for some biological networks ⋮ Efficiently and effectively recognizing toricity of steady state varieties ⋮ A logic based approach to finding real singularities of implicit ordinary differential equations ⋮ Cylindrical algebraic decomposition using local projections ⋮ Certified Reasoning with Infinity ⋮ Algorithmic reduction of biological networks with multiple time scales ⋮ $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation ⋮ Combined Decision Techniques for the Existential Theory of the Reals ⋮ Editorial: Symbolic computation and satisfiability checking ⋮ Combining logical and algebraic techniques for natural style proving in elementary analysis ⋮ Effective Quantifier Elimination for Presburger Arithmetic with Infinity ⋮ A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic ⋮ Automatic derivation of positivity conditions inside boundary elements with the help of the REDLOG computer logic package. ⋮ Template polyhedra and bilinear optimization ⋮ Quantifier elimination for trigonometric polynomials by cylindrical trigonometric decomposition ⋮ Deciding Hopf bifurcations by quantifier elimination in a software-component architecture ⋮ Endomorphisms for Non-trivial Non-linear Loop Invariant Generation ⋮ Discussion on: ``Stabilisability and stability for explicit and implicit polynomial systems: A symbolic computation approach by D. Nešić and I. M. Y. Mareels ⋮ Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description) ⋮ Quantified constraints under perturbation ⋮ Generating invariants for non-linear hybrid systems
Uses Software
This page was built for publication: Quantifier elimination for real algebra -- the quadratic case and beyond