Partial cylindrical algebraic decomposition for quantifier elimination
From MaRDI portal
Publication:1186711
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
Related Items (only showing first 100 items - show all)
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 ⋮ Two Variants of Bézout Subresultants for Several Univariate Polynomials ⋮ Validating numerical semidefinite programming solvers for polynomial invariants ⋮ Local search for solving satisfiability of polynomial formulas ⋮ Truth table invariant cylindrical algebraic decomposition ⋮ Zero-Hopf bifurcation of limit cycles in certain differential systems ⋮ Subresultants of several univariate polynomials in Newton basis ⋮ Supporting proving and discovering geometric inequalities in GeoGebra by using Tarski ⋮ Parametric root finding for supporting proving and discovering geometric inequalities in GeoGebra ⋮ Faster one block quantifier elimination for regular polynomial systems of equations ⋮ Choosing the variable ordering for cylindrical algebraic decomposition via exploiting chordal structure ⋮ 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 ⋮ 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
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- On mechanical quantifier elimination for elementary algebra and geometry
- A cluster-based cylindrical algebraic decomposition algorithm
- Real quantifier elimination is doubly exponential
- Solving Polynomial Strict Inequalities Using Cylindrical Algebraic Decomposition
- Cylindrical Algebraic Decomposition I: The Basic Algorithm
This page was built for publication: Partial cylindrical algebraic decomposition for quantifier elimination
