Efficient, verified checking of propositional proofs
type: Item
instance of: scholarly article
title: Efficient, verified checking of propositional proofs
zbMATH Open document ID: 1483.68483
DOI: 10.1007/978-3-319-66107-0_18
author: Marijn J. H. Heule
author: Warren jun. Hunt
author: Matt Kaufmann
author: Nathan D. Wetzler
publication date: 2018-01-04T00:00:00Z
Mathematics Subject Classification ID: 68V15
Mathematics Subject Classification ID: 68T20
zbMATH DE Number: 6821857
describes a project that uses: Isabelle/HOL
describes a project that uses: versat
describes a project that uses: ACL2
describes a project that uses: DRAT-trim
MaRDI profile type: Publication
full work available at URL: 978-3-319-66107-0 18
OpenAlex ID: W2746765002
cites work: A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
cites work: Efficient certified RAT verification
cites work: A machine program for theorem-proving
cites work: A Computing Procedure for Quantification Theory
cites work: Theory and Applications of Satisfiability Testing
cites work: Efficient execution in an automated reasoning environment
cites work: Verifying Refutations with Extended Resolution
cites work: Inprocessing Rules
cites work: Rough Diamond: An Extension of Equivalence-Based Rewriting
cites work: Efficient verified (UN)SAT certificate checking
cites work: Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
cites work: Formalization and implementation of modern SAT solvers
cites work: Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
cites work: Recursive functions of symbolic expressions and their computation by machine, Part I
cites work: versat: A Verified Modern SAT Solver
cites work: The Mechanical Verification of a DPLL-Based Satisfiability Solver
cites work: Q3997095
cites work: Mechanical Verification of SAT Refutations with Extended Resolution
cites work: DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
description: scientific article; zbMATH DE number 6821857