Efficient, verified checking of propositional proofs
From MaRDI portal
Publication:1687744
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
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 (8)
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 ⋮ Generating extended resolution proofs with a BDD-based SAT solver ⋮ Efficient verified (UN)SAT certificate checking ⋮ Clause redundancy and preprocessing in maximum satisfiability
Uses Software
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
