Efficient certified RAT verification
From MaRDI portal
Publication:2405252
DOI10.1007/978-3-319-63046-5_14zbMath1494.68284arXiv1612.02353OpenAlexW2564212270MaRDI QIDQ2405252
Luís Cruz-Filipe, Peter Schneider-Kamp, Marijn J. H. Heule, Warren A. jun. Hunt, Matt Kaufmann
Publication date: 22 September 2017
Full work available at URL: https://arxiv.org/abs/1612.02353
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
Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs, A verified SAT solver framework with learn, forget, restart, and incrementality, Efficient, verified checking of propositional proofs, Generating Extended Resolution Proofs with a BDD-Based SAT Solver, Inconsistency Proofs for ASP: The ASP - DRUPE Format, Never trust your solver: certification for SAT and QBF, Towards Uniform Certification in QBF, Unnamed Item, QMaxSATpb: a certified MaxSAT solver, Simulating strong practical proof systems with extended resolution, Truth Assignments as Conditional Autarkies, \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML, Milestones from the Pure Lisp Theorem Prover to ACL2, The resolution of Keller's conjecture, A flexible proof format for SAT solver-elaborator communication, Generating extended resolution proofs with a BDD-based SAT solver, Efficient verified (UN)SAT certificate checking, Formally verifying the solution to the Boolean Pythagorean triples problem, The resolution of Keller's conjecture, Flexible proof production in an industrial-strength SMT solver, Clause redundancy and preprocessing in maximum satisfiability
Uses Software
