Verifying an incremental theory solver for linear arithmetic in Isabelle/HOL

DOI10.1007/978-3-030-29007-8_13zbMath1435.68362OpenAlexW2969660840MaRDI QIDQ2180230

Max W. Haslbeck, René Thiemann, Ralph Bottesch

Publication date: 13 May 2020

Full work available at URL: https://doi.org/10.1007/978-3-030-29007-8_13

zbMATH Keywords

simplex algorithmFarkas' lemmaSMT solvingDPLL(T)

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Computational aspects of satisfiability (68R07)

Related Items (4)

Formalizing the Face Lattice of Polyhedra ⋮ Verified Approximation Algorithms ⋮ Unnamed Item ⋮ Unnamed Item

Uses Software

• Isabelle
• Isabelle/HOL
• HOL

This page was built for publication: Verifying an incremental theory solver for linear arithmetic in Isabelle/HOL