Quantifier elimination by cylindrical algebraic decomposition based on regular chains

DOI10.1016/j.jsc.2015.11.008zbMath1398.68695OpenAlexW1949239131MaRDI QIDQ5925208

Changbo Chen, Marc Moreno Maza

Publication date: 11 February 2016

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

Full work available at URL: https://doi.org/10.1016/j.jsc.2015.11.008

zbMATH Keywords

quantifier eliminationcylindrical algebraic decompositiontriangular decompositionregular chains

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Quantifier elimination, model completeness, and related topics (03C10)

Related Items (12)

Chordality Preserving Incremental Triangular Decomposition and Its Implementation ⋮ Variable Ordering Selection for Cylindrical Algebraic Decomposition with Artificial Neural Networks ⋮ A Machine Learning Based Software Pipeline to Pick the Variable Ordering for Algorithms with Polynomial Inputs ⋮ Parametric toricity of steady state varieties of reaction networks ⋮ VerifyRealRoots: a Matlab package for computing verified real solutions of polynomials systems of equations and inequalities ⋮ Revealing Bistability in Neurological Disorder Models By Solving Parametric Polynomial Systems Geometrically ⋮ Is computer algebra ready for conjecturing and proving geometric inequalities in the classroom? ⋮ Methodologies of Symbolic Computation ⋮ Computing with Tarski formulas and semi-algebraic sets in a web browser ⋮ Can an A.I. win a medal in the mathematical olympiad? – Benchmarking mechanized mathematics on pre-university problems1 ⋮ Using machine learning to improve cylindrical algebraic decomposition ⋮ On types of degenerate critical points of real polynomial functions

Uses Software

• Maple
• RegularChains
• CylindricalAlgebraicDecompose

Cites Work

• Unnamed Item
• Unnamed Item
• Variant quantifier elimination
• Thom's lemma, the coding of real algebraic numbers and the computation of the topology of semi-algebraic sets
• On the computational complexity and geometry of the first-order theory of the reals. I: Introduction. Preliminaries. The geometry of semi-algebraic sets. The decision problem for the existential theory of the reals
• Quantifier elimination and cylindrical algebraic decomposition. Proceedings of a symposium, Linz, Austria, October 6--8, 1993
• Quantifier elimination in automatic loop parallelization
• An Incremental Algorithm for Computing Cylindrical Algebraic Decompositions
• Real Quantifier Elimination in the RegularChains Library
• Cylindrical Algebraic Decomposition in the RegularChains Library
• Truth Table Invariant Cylindrical Algebraic Decomposition by Regular Chains
• Computing cylindrical algebraic decomposition via triangular decomposition
• Cylindrical algebraic decompositions for boolean combinations
• New results on quantifier elimination over real closed fields and applications to constraint databases
• Comprehensive Triangular Decomposition
• Quantifier elimination by cylindrical algebraic decomposition based on regular chains
• Algorithms in real algebraic geometry

This page was built for publication: Quantifier elimination by cylindrical algebraic decomposition based on regular chains