Extensions of the cylindrical algebraic covering method for quantifiers
From MaRDI portal
Cites work
- \texttt{SMT-RAT}: an open source \texttt{C++} toolbox for strategic and parallel SMT solving
- A model-constructing satisfiability calculus
- An effective implementation of a symbolic-numeric cylindrical algebraic decomposition for quantifier elimination
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Computer Aided Verification
- Constructing a single cell in cylindrical algebraic decomposition
- Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)
- Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
- Efficient E-Matching for SMT Solvers
- Efficient projection orders for CAD
- Explainable AI insights for symbolic computation: a case study on selecting the variable ordering for cylindrical algebraic decomposition
- From simplification to a partial theory solver for non-linear real polynomial constraints
- scientific article; zbMATH DE number 3497890 (Why is no real title available?)
- scientific article; zbMATH DE number 517393 (Why is no real title available?)
- scientific article; zbMATH DE number 589124 (Why is no real title available?)
- scientific article; zbMATH DE number 1157658 (Why is no real title available?)
- scientific article; zbMATH DE number 2151206 (Why is no real title available?)
- scientific article; zbMATH DE number 3068536 (Why is no real title available?)
- Improved projection for cylindrical algebraic decomposition
- Levelwise construction of a single cylindrical algebraic cell
- Open non-uniform cylindrical algebraic decompositions
- Optimization modulo non-linear arithmetic via incremental linearization
- Polynomial constraints and unsat cores in \textsc{Tarski}
- QEPCAD B
- QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment
- Solving non-linear arithmetic
- Solving systems of strict polynomial inequalities
- Speeding up cylindrical algebraic decomposition by Gröbner bases
- Syntax-guided quantifier instantiation
- The complexity of cylindrical algebraic decomposition with respect to polynomial degree
- The complexity of quantifier elimination and cylindrical algebraic decomposition
- Validity proof of Lazard's method for CAD construction
This page was built for publication: Extensions of the cylindrical algebraic covering method for quantifiers
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7303131)
