Efficient, verified checking of propositional proofs

DOI10.1007/978-3-319-66107-0_18zbMath1483.68483OpenAlexW2746765002MaRDI QIDQ1687744

Warren jun. Hunt, Marijn J. H. Heule, Matt Kaufmann, Nathan D. Wetzler

Publication date: 4 January 2018

Full work available at URL: https://doi.org/10.1007/978-3-319-66107-0_18

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 (12)

Unnamed Item ⋮ Simulating strong practical proof systems with extended resolution ⋮ \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML ⋮ Certifying emptiness of timed Büchi automata ⋮ Milestones from the Pure Lisp Theorem Prover to ACL2 ⋮ Propositional proof skeletons ⋮ Unsatisfiability proofs for distributed clause-sharing SAT solvers ⋮ Generating extended resolution proofs with a BDD-based SAT solver ⋮ A resolution-based interactive proof system for UNSAT ⋮ Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker ⋮ Efficient verified (UN)SAT certificate checking ⋮ Clause redundancy and preprocessing in maximum satisfiability

Uses Software

• Unnamed Item
• Unnamed Item
• versat
• DRAT-trim

Cites Work

• Unnamed Item
• Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
• Formalization and implementation of modern SAT solvers
• Efficient certified RAT verification
• A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
• Rough Diamond: An Extension of Equivalence-Based Rewriting
• versat: A Verified Modern SAT Solver
• Inprocessing Rules
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• Recursive functions of symbolic expressions and their computation by machine, Part I
• Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
• Verifying Refutations with Extended Resolution
• The Mechanical Verification of a DPLL-Based Satisfiability Solver
• Theory and Applications of Satisfiability Testing
• Mechanical Verification of SAT Refutations with Extended Resolution
• Efficient execution in an automated reasoning environment
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• Efficient verified (UN)SAT certificate checking

This page was built for publication: Efficient, verified checking of propositional proofs