Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)
type: Item
instance of: scholarly article
title: Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)
DOI: 10.1007/978-3-031-10769-6_7
author: Gereon Kremer
author: Andrew Reynolds
author: Clark Barrett
author: Cesare Tinelli
publication date: 2022-12-07T00:00:00Z
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7628183
zbMATH Keywords: satisfiability modulo theories
zbMATH Keywords: nonlinear real arithmetic
zbMATH Keywords: abstraction refinement
zbMATH Keywords: cylindrical algebraic coverings
describes a project that uses: CoCoA
describes a project that uses: CoCoALib
describes a project that uses: veriT
describes a project that uses: MathSAT5
describes a project that uses: z3
describes a project that uses: raSAT
describes a project that uses: dReal
describes a project that uses: Zephyrus2
describes a project that uses: REDLOG
describes a project that uses: SMT-RAT
describes a project that uses: libpoly
describes a project that uses: Yices
MaRDI profile type: Publication
full work available at URL: 978-3-031-10769-6 7
OpenAlex ID: W4289104052
cites work: Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
cites work: On the combinatorial and algebraic complexity of quantifier elimination
cites work: Planning for Hybrid Systems via Satisfiability Modulo Theories
cites work: Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions
cites work: The MathSAT5 SMT Solver
cites work: Q4079605
cites work: Virtual Substitution for SMT-Solving
cites work: SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
cites work: Real quantifier elimination is doubly exponential
cites work: SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers
cites work: Subtropical satisfiability
cites work: dReal: An SMT Solver for Nonlinear Theories over the Reals
cites work: Solving systems of polynomial inequalities in subexponential time
cites work: Solving Non-linear Arithmetic
cites work: Fully incremental cylindrical algebraic decomposition
cites work: Q4295433
cites work: A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition
cites work: Validity proof of Lazard's method for CAD construction
cites work: A Model-Constructing Satisfiability Calculus
cites work: Solving SAT and SAT Modulo Theories
cites work: Designing theory solvers with extensions
cites work: raSAT: An SMT Solver for Polynomial Constraints
cites work: Quantifier elimination for real algebra -- the quadratic case and beyond
description: scientific article; zbMATH DE number 7628183