Designing theory solvers with extensions

DOI10.1007/978-3-319-66167-4_2zbMath1495.68239OpenAlexW2745929493MaRDI QIDQ1687536

Clark Barrett, Cesare Tinelli, Andrew Reynolds, Dejan Jovanović

Publication date: 4 January 2018

Full work available at URL: https://doi.org/10.1007/978-3-319-66167-4_2

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (5)

Optimization modulo non-linear arithmetic via incremental linearization ⋮ The CADE-27 Automated theorem proving System Competition – CASC-27 ⋮ Towards satisfiability modulo parametric bit-vectors ⋮ Towards bit-width-independent proofs in SMT solvers ⋮ Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)

This page was built for publication: Designing theory solvers with extensions