Extended resolution simulates \({\mathsf{DRAT}}\)

DOI10.1007/978-3-319-94205-6_34zbMath1441.68278OpenAlexW2811000330MaRDI QIDQ1799112

Benjamin Kiesl, Marijn J. H. Heule, Adrián Rebola-Pardo

Publication date: 18 October 2018

Full work available at URL: https://doi.org/10.1007/978-3-319-94205-6_34

Mathematics Subject Classification ID

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

Related Items (6)

Unnamed Item ⋮ Inconsistency Proofs for ASP: The ASP - DRUPE Format ⋮ Simulating strong practical proof systems with extended resolution ⋮ \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML ⋮ Strong extension-free proof systems ⋮ Flexible proof production in an industrial-strength SMT solver

Uses Software

• DRAT-trim

This page was built for publication: Extended resolution simulates \({\mathsf{DRAT}}\)