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

From MaRDI portal
Publication:677553

DOI10.1007/s002000050055zbMath0867.03003OpenAlexW2040951317MaRDI QIDQ677553

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



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 linearizationParametric toricity of steady state varieties of reaction networksSMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT SolvingComputing Hopf Bifurcations in Chemical Reaction Networks Using Reaction CoordinatesDetection of Hopf bifurcations in chemical reaction networks using convex coordinatesThe Lee identities in topoi. IStability analysis for discrete biological models using algebraic methodsSatisfiability Checking: Theory and ApplicationsAn effective implementation of symbolic-numeric cylindrical algebraic decomposition for quantifier eliminationModular strategic SMT solving with \textbf{SMT-RAT}Experiments with automated reasoning in the classBetter answers to real questionsFast simplifications for Tarski formulas based on monomial inequalitiesSolving Nonlinear Integer Arithmetic with MCSATGenerating invariants for non-linear loops by linear algebraic methodsAdapting Real Quantifier Elimination Methods for Conflict Set ComputationA survey of some methods for real quantifier elimination, decision, and satisfiability and their applicationsCGSQE/SyNRACFast theorem-proving and Wu's methodQuantifier elimination for a class of exponential polynomial formulasQuantifier elimination in automatic loop parallelizationMultiple object semilinear motion planningOn a decision procedure for quantified linear programsWeak quantifier elimination for the full linear theory of the integersQuantifier elimination supported proofs in the numerical treatment of fluid flowsApplication of quantifier elimination to inverse buckling problemsI-RiSC: An SMT-Compliant Solver for the Existential Fragment of Real AlgebraThe Strategy Challenge in SMT SolvingDeciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coveringsFinding at least one point in each connected component of a real algebraic set defined by a single equationAn empirical analysis of algorithms for partially Clairvoyant schedulingAlgorithmic global criteria for excluding oscillationsSolution formulas for cubic equations without or with constraintsSimple CAD construction and its applicationsParametric 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 TestsInvestigating Generic Methods to Solve Hopf Bifurcation Problems in Algebraic BiologyReal World VerificationValidating numerical semidefinite programming solvers for polynomial invariantsIdentifying the parametric occurrence of multiple steady states for some biological networksEfficiently and effectively recognizing toricity of steady state varietiesA logic based approach to finding real singularities of implicit ordinary differential equationsCylindrical algebraic decomposition using local projectionsCertified Reasoning with InfinityAlgorithmic reduction of biological networks with multiple time scales$$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic ComputationCombined Decision Techniques for the Existential Theory of the RealsEditorial: Symbolic computation and satisfiability checkingCombining logical and algebraic techniques for natural style proving in elementary analysisEffective Quantifier Elimination for Presburger Arithmetic with InfinityA Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer ArithmeticAutomatic derivation of positivity conditions inside boundary elements with the help of the REDLOG computer logic package.Template polyhedra and bilinear optimizationQuantifier elimination for trigonometric polynomials by cylindrical trigonometric decompositionDeciding Hopf bifurcations by quantifier elimination in a software-component architectureEndomorphisms for Non-trivial Non-linear Loop Invariant GenerationDiscussion on: ``Stabilisability and stability for explicit and implicit polynomial systems: A symbolic computation approach by D. Nešić and I. M. Y. MareelsCooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)Quantified constraints under perturbationGenerating invariants for non-linear hybrid systems


Uses Software



This page was built for publication: Quantifier elimination for real algebra -- the quadratic case and beyond