Quantifier elimination for real algebra -- the quadratic case and beyond
From MaRDI portal
Publication:677553
DOI10.1007/S002000050055zbMATH Open0867.03003OpenAlexW2040951317MaRDI QIDQ677553FDOQ677553
Authors: Volker Weispfenning 
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
Recommendations
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 (only showing first 100 items - show all)
- Editorial: Symbolic computation and satisfiability checking
- Quantifier elimination by cylindrical algebraic decomposition based on regular chains
- Optimization modulo non-linear arithmetic via incremental linearization
- Parametric toricity of steady state varieties of reaction networks
- Improved Algorithms for Sign Determination and Existential Quantifier Elimination
- Better answers to real questions
- Solution formulas for cubic equations without or with constraints
- Fast simplifications for Tarski formulas based on monomial inequalities
- Title not available (Why is that?)
- A survey of some methods for real quantifier elimination, decision, and satisfiability and their applications
- Real World Verification
- Simple CAD construction and its applications
- A logic based approach to finding real singularities of implicit ordinary differential equations
- Dines-Fourier-Motzkin quantifier elimination and an application of corresponding transfer principles over ordered fields
- Quantified constraints under perturbation
- A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic
- Solving nonlinear integer arithmetic with MCSAT
- 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
- Real quantifier elimination in the RegularChains library
- Weak Integer Quantifier Elimination Beyond the Linear Case
- Formula Simplification for Real Quantifier Elimination Using Geometric Invariance
- Quantifier elimination for the reals with a predicate for the powers of two
- 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
- Computer Science Logic
- Generating invariants for non-linear hybrid systems
- New Domains for Applied Quantifier Elimination
- 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
- Quantifier elimination: Optimal solution for two classical examples
- Endomorphisms for Non-trivial Non-linear Loop Invariant Generation
- Semilinear motion planning in REDLOG
- Finding at least one point in each connected component of a real algebraic set defined by a single equation
- Quantifier elimination in automatic loop parallelization
- Combining logical and algebraic techniques for natural style proving in elementary analysis
- Title not available (Why is that?)
- Applying Linear Quantifier Elimination
- Verification and synthesis using real quantifier elimination
- Satisfiability checking: theory and applications
- On mechanical quantifier elimination for elementary algebra and geometry
- Quantifier elimination for a class of exponential polynomial formulas
- Generating invariants for non-linear loops by linear algebraic methods
- Computing Hopf bifurcations in chemical reaction networks using reaction coordinates
- Artificial Intelligence and Symbolic Computation
- Detection of Hopf bifurcations in chemical reaction networks using convex coordinates
- Variant real quantifier elimination: algorithm and application
- Real quantifier elimination by computation of comprehensive Gröbner systems
- Stability analysis for discrete biological models using algebraic methods
- Local quantifier elimination
- Weak quantifier elimination for the full linear theory of the integers
- Quantifier Elimination for Formulas Constrained by Quadratic Equations via Slope Resultants
- 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 Lee identities in topoi. I
- TheoryGuru: a Mathematica package to apply quantifier elimination technology to economics
- \textsf{SC}\(^2\): satisfiability checking meets symbolic computation. (Project paper)
- Quantifier elimination for trigonometric polynomials by cylindrical trigonometric decomposition
- \texttt{SMT-RAT}: an open source \texttt{C++} toolbox for strategic and parallel SMT solving
- Cylindrical algebraic decomposition using local projections
- An empirical analysis of algorithms for partially Clairvoyant scheduling
- Title not available (Why is that?)
- Quantifier elimination supported proofs in the numerical treatment of fluid flows
- Deciding Hopf bifurcations by quantifier elimination in a software-component architecture
- CGSQE/SyNRAC: a real quantifier elimination package based on the computation of comprehensive Gröbner systems
- Variant quantifier elimination
- Certified reasoning with infinity
- 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
- Elementary recursive quantifier elimination based on Thom encoding and sign determination
- Adapting real quantifier elimination methods for conflict set computation
- Towards fast one-block quantifier elimination through generalised critical values
- Effective Quantifier Elimination for Presburger Arithmetic with Infinity
- Efficient subformula orders for real quantifier elimination of non-prenex formulas
- On maps which preserve semipositivity and quantifier elimination theory for real numbers
- Application of quantifier elimination to inverse buckling problems
- A simple quantifier-free formula of positive semidefinite cyclic ternary quartic forms
- Parametric Qualitative Analysis of Ordinary Differential Equations: Computer Algebra Methods for Excluding Oscillations (Extended Abstract) (Invited Talk)
- Efficient Preprocessing Methods for Quantifier Elimination
- Multiple object semilinear motion planning
- Quantifier Elimination for Approximate Factorization of Linear Partial Differential Operators
- The strategy challenge in SMT solving
- Quantifier elimination by cylindrical algebraic decomposition based on regular chains
- Real quantifier elimination for the synthesis of optimal numerical algorithms (case study: square root computation)
- An effective implementation of a special quantifier elimination for a sign definite condition by logical formula simplification
- I-RiSC: an SMT-compliant solver for the existential fragment of real algebra
- Quantifier Elimination for Quartics
- On real roots counting for non-radical parametric ideals
- Supporting global numerical optimization of rational functions by generic symbolic convexity tests
- Verified Quadratic Virtual Substitution for Real Arithmetic
- Validating numerical semidefinite programming solvers for polynomial invariants
- Quantifier elimination theory and maps which preserve semipositivity
- Experiments with automated reasoning in the class
- QE software based on comprehensive Gröbner systems
- Local search for solving satisfiability of polynomial formulas
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)
