DRAT-based bit-vector proofs in CVC4

DOI10.1007/978-3-030-24258-9_21zbMath1441.68235arXiv1907.00087OpenAlexW2963523951MaRDI QIDQ2181940

Aina Niemetz, Alex Ozdemir, Yoni Zohar, Mathias Preiner, Clark Barrett

Publication date: 20 May 2020

Full work available at URL: https://arxiv.org/abs/1907.00087

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (3)

CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver ⋮ Flexible proof production in an industrial-strength SMT solver ⋮ Symbolic computation in Maude: some tapas

Uses Software

• Coq
• MiniSat
• SMT-LIB
• CVC4
• CryptoMiniSat
• DRAT-trim
• SMTCoq

This page was built for publication: DRAT-based bit-vector proofs in CVC4