Partial cylindrical algebraic decomposition for quantifier elimination

DOI10.1016/S0747-7171(08)80152-6zbMath0754.68063OpenAlexW2007074311MaRDI QIDQ1186711

Publication date: 28 June 1992

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0747-7171(08)80152-6

zbMATH Keywords

quantifier elimination Cylindrical Algebraic Decomposition

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30)

Related Items

Erratum to: ``Analyzing restricted fragments of the theory of linear arithmetic, Parametric toricity of steady state varieties of reaction networks, Characterizing positively invariant sets: inductive and topological methods, Reachability and optimal control for linear hybrid automata: a quantifier elimination approach, Analysis and optimization of inner products for mimetic finite difference methods on a triangular grid, Geometry and topology of parameter space: Investigating measures of robustness in regulatory networks, Verification of Hybrid Systems, Applied Algebraic Geometry in Model Based Design for Manufacturing, Real quantifier elimination for the synthesis of optimal numerical algorithms (case study: square root computation), Recent advances in program verification through computer algebra, Stability analysis for discrete biological models using algebraic methods, The exact region of stability for MacCormack scheme, Termination of linear programs with nonlinear constraints, Positive root isolation for poly-powers by exclusion and differentiation, The maximum number and its distribution of singular points for parametric piecewise algebraic curves, A quantifier-elimination based heuristic for automatically generating inductive assertions for programs, An effective implementation of symbolic-numeric cylindrical algebraic decomposition for quantifier elimination, On the complexity of quantified linear systems, On the robustness and optimality of algebraic multilevel methods for reaction-diffusion type problems, Visually dynamic presentation of proofs in plane geometry. II: Automated generation of visually dynamic presentations with the full-angle method and the deductive database method, An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty, Bellerophon: tactical theorem proving for hybrid systems, Some geometric properties of successive difference substitutions, Computing integrals over polynomially defined regions and their boundaries in 2 and 3 dimensions, Change-of-bases abstractions for non-linear hybrid systems, Variant quantifier elimination, Adapting Real Quantifier Elimination Methods for Conflict Set Computation, A survey of some methods for real quantifier elimination, decision, and satisfiability and their applications, An algorithm for determining copositive matrices, On solving parametric polynomial systems, Discovering polynomial Lyapunov functions for continuous dynamical systems, Open weak CAD and its applications, Solving parametric piecewise polynomial systems, Computing equilibria of semi-algebraic economies using triangular decomposition and real solution classification, Cylindrical algebraic sub-decompositions, Global optimization of polynomials over real algebraic sets, Quantifier elimination for a class of exponential polynomial formulas, Cylindrical algebraic decomposition using validated numerics, A complexity perspective on entailment of parameterized linear constraints, Solving systems of strict polynomial inequalities, On using Lazard's projection in CAD construction, Proving inequalities and solving global optimization problems via simplified CAD projection, On the collision detection problem of two moving objects described by algebraic sets, Lack-of-contact conditions for a penny-shaped crack under a polynomial normal loading, Solution to the generalized champagne problem on simultaneous stabilization of linear systems, A note on dead-beat controllability of generalised Hammerstein systems, Testing elementary function identities using CAD, Quantifier elimination supported proofs in the numerical treatment of fluid flows, Application of quantifier elimination to inverse buckling problems, Computational complexity of determining which statements about causality hold in different space-time models, A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets, ModelPlex: verified runtime validation of verified cyber-physical system models, Analyzing restricted fragments of the theory of linear arithmetic, Construction of parametric barrier functions for dynamical systems using interval analysis, A search-based procedure for nonlinear real arithmetic, Algebraic analysis of stability and bifurcation of a self-assembling micelle system, A class of mechanically decidable problems beyond Tarski's model, Constructing invariants for hybrid systems, Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings, Automatic generation of bounds for polynomial systems with application to the Lorenz system, Validity proof of Lazard's method for CAD construction, Plane partitions. VI: Stembridge's TSPP theorem, Symbolic decision procedure for termination of linear programs, Using machine learning to improve cylindrical algebraic decomposition, Solution formulas for cubic equations without or with constraints, Optimally-stable second-order accurate difference schemes for nonlinear conservation laws in 3D, Root neighborhoods, generalized lemniscates, and robust stability of dynamic systems, Vector barrier certificates and comparison systems, Efficiently and effectively recognizing toricity of steady state varieties, A logic based approach to finding real singularities of implicit ordinary differential equations, An Incremental Algorithm for Computing Cylindrical Algebraic Decompositions, A Simple Quantifier-Free Formula of Positive Semidefinite Cyclic Ternary Quartic Forms, Reachability analysis of rational eigenvalue linear systems, Recent advances on determining the number of real roots of parametric polynomials, Algorithmic reduction of biological networks with multiple time scales, Need Polynomial Systems Be Doubly-Exponential?, Editorial: Symbolic computation and satisfiability checking, Fully incremental cylindrical algebraic decomposition, Cylindrical algebraic decomposition with equational constraints, A note on observability tests for general polynomial and simple Wiener-Hammerstein systems, The Complexity of Cylindrical Algebraic Decomposition with Respect to Polynomial Degree, Stability analysis by quantifier elimination., Parts of quantum states, A semi-algebraic approach for asymptotic stability analysis, Computing differential invariants of hybrid systems as fixed points, Differential dynamic logic for hybrid systems, Real zeros of the zero-dimensional parametric piecewise algebraic variety, Symbolic computation for the qualitative theory of differential equations, Quantifier elimination for trigonometric polynomials by cylindrical trigonometric decomposition, Deciding Hopf bifurcations by quantifier elimination in a software-component architecture, A computational method for determining strong stabilizability of \(n\)-D systems, Stabilisability and stability for explicit and implicit polynomial systems: A symbolic computation approach, Choosing better variable orderings for cylindrical algebraic decomposition via exploiting chordal structure, Constructing a single cell in cylindrical algebraic decomposition, Special algorithm for stability analysis of multistable biological regulatory systems, Quantified constraints under perturbation, A comparison of algorithms for proving positivity of linearly recurrent sequences, Interval arithmetic in cylindrical algebraic decomposition, Polynomial optimization with applications to stability analysis and control -- alternatives to sum of squares, A hypergeometric inequality, Deciding first-order formulas involving univariate mixed trigonometric-polynomials, Using Symbolic Computation to Analyze Zero-Hopf Bifurcations of Polynomial Differential Systems, VerifyRealRoots: a Matlab package for computing verified real solutions of polynomials systems of equations and inequalities, Non-monotonic spatial reasoning with answer set programming modulo theories, Explainable AI insights for symbolic computation: a case study on selecting the variable ordering for cylindrical algebraic decomposition, Levelwise construction of a single cylindrical algebraic cell, Is computer algebra ready for conjecturing and proving geometric inequalities in the classroom?, Computing Differential Invariants of Hybrid Systems as Fixedpoints, Tarski’s Influence on Computer Science, KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description), Algebraic stability criteria and symbolic derivation of stability conditions for feedback control systems, Integrating Systems around the User: Combining Isabelle, Maple, and QEPCAD in the Proverʼs Palette, A parameter space approach to fixed-order robust controller synthesis by quantifier elimination, Computing Switching Surfaces in Optimal Control Based on Triangular Decomposition, Simple CAD construction and its applications, Supporting Global Numerical Optimization of Rational Functions by Generic Symbolic Convexity Tests, Symbolic reachability computation for families of linear vector fields, Algebraic Analysis of Bifurcation and Limit Cycles for Biological Systems, Investigating Generic Methods to Solve Hopf Bifurcation Problems in Algebraic Biology, Real World Verification, Improved projection for cylindrical algebraic decomposition, Validating numerical semidefinite programming solvers for polynomial invariants, Truth table invariant cylindrical algebraic decomposition, Problem Formulation for Truth-Table Invariant Cylindrical Algebraic Decomposition by Incremental Triangular Decomposition, Applying Machine Learning to the Problem of Choosing a Heuristic to Select the Variable Ordering for Cylindrical Algebraic Decomposition, Combining Isabelle and QEPCAD-B in the Prover’s Palette, Algebraic Analysis of Bifurcations and Chaos for Discrete Dynamical Systems, Improved Cross-Validation for Classifiers that Make Algorithmic Choices to Minimise Runtime Without Compromising Output Correctness

Uses Software

QEPCAD

Cites Work