Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings (Q1996869): Difference between revisions

Revision as of 16:13, 24 July 2024

scientific article

Language	Label	Description	Also known as
English	Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings	scientific article

Statements

instance of

scholarly article

0 references

title

Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings (English)

0 references

0 references

0 references

0 references

0 references

Journal of Logical and Algebraic Methods in Programming

0 references

publication date

26 February 2021

0 references

full work available at URL

https://arxiv.org/abs/2003.05633

0 references

zbMATH Keywords

satisfiability modulo theories

0 references

nonlinear real arithmetic

0 references

cylindrical algebraic decomposition

0 references

real polynomial systems

0 references

describes a project that uses

0 references

0 references

0 references

0 references

0 references

0 references

0 references

0 references

CylindricalAlgebraicDecompose

0 references

MaRDI profile type

MaRDI publication profile

0 references

cites work

New Domains for Applied Quantifier Elimination

0 references

A Case Study on the Parametric Occurrence of Multiple Steady States

0 references

TheoryGuru: a Mathematica package to apply quantifier elimination technology to economics

0 references

Mathematics by machine

0 references

Q4391214

0 references

Q4391215

0 references

Improving the Use of Equational Constraints in Cylindrical Algebraic Decomposition

0 references

The Complexity of Cylindrical Algebraic Decomposition with Respect to Polynomial Degree

0 references

Cylindrical algebraic decomposition with equational constraints

0 references

Q5301651

0 references

Algorithms in real algebraic geometry

0 references

Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions

0 references

Polyhedral Approximation of Multivariate Polynomials Using Handelman’s Theorem

0 references

Q5457277

0 references

raSAT: an SMT solver for polynomial constraints

0 references

Quantifier elimination for real algebra -- the quadratic case and beyond

0 references

Virtual Substitution for SMT-Solving

0 references

Subtropical satisfiability

0 references

CoCoALib: A C++ Library for Computations in Commutative Algebra... and Beyond

0 references

Cylindrical algebraic sub-decompositions

0 references

Partial cylindrical algebraic decomposition for quantifier elimination

0 references

Q4391213

0 references

Truth table invariant cylindrical algebraic decomposition

0 references

Solving Nonlinear Integer Arithmetic with MCSAT

0 references

Open Non-uniform Cylindrical Algebraic Decompositions

0 references

A new decision method for elementary algebra

0 references

Q5503674

0 references

Building Bridges between Symbolic Computation and Satisfiability Checking

0 references

$$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation

0 references

SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving

0 references

Fully incremental cylindrical algebraic decomposition

0 references

Solving Non-linear Arithmetic

0 references

Adapting Real Quantifier Elimination Methods for Conflict Set Computation

0 references

Q4391223

0 references

Validity proof of Lazard's method for CAD construction

0 references

Q4295433

0 references

Projection and Quantifier Elimination Using Non-uniform Cylindrical Algebraic Decomposition

0 references

Cylindrical Algebraic Decomposition in the RegularChains Library

0 references

Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition

0 references

Q3624141

0 references

A Model-Constructing Satisfiability Calculus

0 references

Using machine learning to improve cylindrical algebraic decomposition

0 references

Improved Cross-Validation for Classifiers that Make Algorithmic Choices to Minimise Runtime Without Compromising Output Correctness

0 references

Enhancements to Lazard's method for cylindrical algebraic decomposition

0 references

Editorial: Symbolic computation and satisfiability checking

0 references

Identifiers

DOI

10.1016/j.jlamp.2020.100633

0 references

Mathematics Subject Classification ID

0 references

0 references

0 references

0 references

Sitelinks

Mathematics(1 entry)

mardi Publication:1996869

@@ Property / describes a project that uses @@
+SMT-RAT
@@ Property / describes a project that uses: SMT-RAT / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+QEPCAD
@@ Property / describes a project that uses: QEPCAD / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+RegularChains
@@ Property / describes a project that uses: RegularChains / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+SMT-LIB
@@ Property / describes a project that uses: SMT-LIB / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+raSAT
@@ Property / describes a project that uses: raSAT / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Theoryguru
@@ Property / describes a project that uses: Theoryguru / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CylindricalAlgebraicDecompose
@@ Property / describes a project that uses: CylindricalAlgebraicDecompose / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W3010680447
@@ Property / OpenAlex ID: W3010680447 / rank @@
+Normal rank
@@ Property / cites work @@
+New Domains for Applied Quantifier Elimination
@@ Property / cites work: New Domains for Applied Quantifier Elimination / rank @@
+Normal rank
@@ Property / cites work @@
+A Case Study on the Parametric Occurrence of Multiple Steady States
+Normal rank
@@ Property / cites work @@
+TheoryGuru: a Mathematica package to apply quantifier elimination technology to economics
+Normal rank
@@ Property / cites work @@
+Mathematics by machine
@@ Property / cites work: Mathematics by machine / rank @@
+Normal rank
@@ Property / cites work @@
+Q4391214
@@ Property / cites work: Q4391214 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4391215
@@ Property / cites work: Q4391215 / rank @@
+Normal rank
@@ Property / cites work @@
+Improving the Use of Equational Constraints in Cylindrical Algebraic Decomposition
+Normal rank
@@ Property / cites work @@
+The Complexity of Cylindrical Algebraic Decomposition with Respect to Polynomial Degree
+Normal rank
@@ Property / cites work @@
+Cylindrical algebraic decomposition with equational constraints
+Normal rank
@@ Property / cites work @@
+Q5301651
@@ Property / cites work: Q5301651 / rank @@
+Normal rank
@@ Property / cites work @@
+Algorithms in real algebraic geometry
@@ Property / cites work: Algorithms in real algebraic geometry / rank @@
+Normal rank
@@ Property / cites work @@
+Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions
+Normal rank
@@ Property / cites work @@
+Polyhedral Approximation of Multivariate Polynomials Using Handelman’s Theorem
+Normal rank
@@ Property / cites work @@
+Q5457277
@@ Property / cites work: Q5457277 / rank @@
+Normal rank
@@ Property / cites work @@
+raSAT: an SMT solver for polynomial constraints
@@ Property / cites work: raSAT: an SMT solver for polynomial constraints / rank @@
+Normal rank
@@ Property / cites work @@
+Quantifier elimination for real algebra -- the quadratic case and beyond
+Normal rank
@@ Property / cites work @@
+Virtual Substitution for SMT-Solving
@@ Property / cites work: Virtual Substitution for SMT-Solving / rank @@
+Normal rank
@@ Property / cites work @@
+Subtropical satisfiability
@@ Property / cites work: Subtropical satisfiability / rank @@
+Normal rank
@@ Property / cites work @@
+CoCoALib: A C++ Library for Computations in Commutative Algebra... and Beyond
+Normal rank
@@ Property / cites work @@
+Cylindrical algebraic sub-decompositions
@@ Property / cites work: Cylindrical algebraic sub-decompositions / rank @@
+Normal rank
@@ Property / cites work @@
+Partial cylindrical algebraic decomposition for quantifier elimination
+Normal rank
@@ Property / cites work @@
+Q4391213
@@ Property / cites work: Q4391213 / rank @@
+Normal rank
@@ Property / cites work @@
+Truth table invariant cylindrical algebraic decomposition
+Normal rank
@@ Property / cites work @@
+Solving Nonlinear Integer Arithmetic with MCSAT
@@ Property / cites work: Solving Nonlinear Integer Arithmetic with MCSAT / rank @@
+Normal rank
@@ Property / cites work @@
+Open Non-uniform Cylindrical Algebraic Decompositions
+Normal rank
@@ Property / cites work @@
+A new decision method for elementary algebra
@@ Property / cites work: A new decision method for elementary algebra / rank @@
+Normal rank
@@ Property / cites work @@
+Q5503674
@@ Property / cites work: Q5503674 / rank @@
+Normal rank
@@ Property / cites work @@
+Building Bridges between Symbolic Computation and Satisfiability Checking
+Normal rank
@@ Property / cites work @@
+$$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation
+Normal rank
@@ Property / cites work @@
+SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
+Normal rank
@@ Property / cites work @@
+Fully incremental cylindrical algebraic decomposition
+Normal rank
@@ Property / cites work @@
+Solving Non-linear Arithmetic
@@ Property / cites work: Solving Non-linear Arithmetic / rank @@
+Normal rank
@@ Property / cites work @@
+Adapting Real Quantifier Elimination Methods for Conflict Set Computation
+Normal rank
@@ Property / cites work @@
+Q4391223
@@ Property / cites work: Q4391223 / rank @@
+Normal rank
@@ Property / cites work @@
+Validity proof of Lazard's method for CAD construction
+Normal rank
@@ Property / cites work @@
+Q4295433
@@ Property / cites work: Q4295433 / rank @@
+Normal rank
@@ Property / cites work @@
+Projection and Quantifier Elimination Using Non-uniform Cylindrical Algebraic Decomposition
+Normal rank
@@ Property / cites work @@
+Cylindrical Algebraic Decomposition in the RegularChains Library
+Normal rank
@@ Property / cites work @@
+Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition
+Normal rank
@@ Property / cites work @@
+Q3624141
@@ Property / cites work: Q3624141 / rank @@
+Normal rank
@@ Property / cites work @@
+A Model-Constructing Satisfiability Calculus
@@ Property / cites work: A Model-Constructing Satisfiability Calculus / rank @@
+Normal rank
@@ Property / cites work @@
+Using machine learning to improve cylindrical algebraic decomposition
+Normal rank
@@ Property / cites work @@
+Improved Cross-Validation for Classifiers that Make Algorithmic Choices to Minimise Runtime Without Compromising Output Correctness
+Normal rank
@@ Property / cites work @@
+Enhancements to Lazard's method for cylindrical algebraic decomposition
+Normal rank
@@ Property / cites work @@
+Editorial: Symbolic computation and satisfiability checking
+Normal rank