Levelwise construction of a single cylindrical algebraic cell
From MaRDI portal
Publication:6149151
DOI10.1016/j.jsc.2023.102288arXiv2212.09309MaRDI QIDQ6149151
Matthew England, Jasper Nalbach, Christopher W. Brown, James H. Davenport, Erika Ábrahám, Philippe Specht
Publication date: 5 February 2024
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2212.09309
cylindrical algebraic decompositionformal proofssatisfiability modulo theoriesnonlinear real arithmeticmodel-constructing satisfiability calculus
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- On using Lazard's projection in CAD construction
- Real quantifier elimination is doubly exponential
- Partial cylindrical algebraic decomposition for quantifier elimination
- Quantifier elimination and cylindrical algebraic decomposition. Proceedings of a symposium, Linz, Austria, October 6--8, 1993
- Validity proof of Lazard's method for CAD construction
- Optimizations of the subresultant algorithm
- Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
- Flexible proof production in an industrial-strength SMT solver
- Enhancements to Lazard's method for cylindrical algebraic decomposition
- Cylindrical algebraic decomposition with equational constraints
- Constructing a single cell in cylindrical algebraic decomposition
- Open Non-uniform Cylindrical Algebraic Decompositions
- Solving Non-linear Arithmetic
- A Model-Constructing Satisfiability Calculus
- Solving Nonlinear Integer Arithmetic with MCSAT
- Constructing a single open cell in a cylindrical algebraic decomposition
- Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF
- SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
- Curtains in CAD: Why Are They a Problem and How Do We Fix Them?
- Applying Machine Learning to Heuristics for Real Polynomial Constraint Solving
- Projection and Quantifier Elimination Using Non-uniform Cylindrical Algebraic Decomposition
- Improved projection for cylindrical algebraic decomposition
- Truth table invariant cylindrical algebraic decomposition
