Efficient, verified checking of propositional proofs (Q1687744): Difference between revisions

@@ Property / author @@
-Nathan D. Wetzler
@@ Property / author: Nathan D. Wetzler / rank @@
-Normal rank
@@ Property / author @@
+Nathan D. Wetzler
@@ Property / author: Nathan D. Wetzler / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+Publication
@@ Property / MaRDI profile type: Publication / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/978-3-319-66107-0_18
+Normal rank
@@ Property / OpenAlex ID @@
+W2746765002
@@ Property / OpenAlex ID: W2746765002 / rank @@
+Normal rank
@@ Property / cites work @@
+A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
+Normal rank
@@ Property / cites work @@
+Efficient certified RAT verification
@@ Property / cites work: Efficient certified RAT verification / rank @@
+Normal rank
@@ Property / cites work @@
+A machine program for theorem-proving
@@ Property / cites work: A machine program for theorem-proving / rank @@
+Normal rank
@@ Property / cites work @@
+A Computing Procedure for Quantification Theory
@@ Property / cites work: A Computing Procedure for Quantification Theory / rank @@
+Normal rank
@@ Property / cites work @@
+Theory and Applications of Satisfiability Testing
@@ Property / cites work: Theory and Applications of Satisfiability Testing / rank @@
+Normal rank
@@ Property / cites work @@
+Efficient execution in an automated reasoning environment
+Normal rank
@@ Property / cites work @@
+Verifying Refutations with Extended Resolution
@@ Property / cites work: Verifying Refutations with Extended Resolution / rank @@
+Normal rank
@@ Property / cites work @@
+Inprocessing Rules
@@ Property / cites work: Inprocessing Rules / rank @@
+Normal rank
@@ Property / cites work @@
+Rough Diamond: An Extension of Equivalence-Based Rewriting
+Normal rank
@@ Property / cites work @@
+Efficient verified (UN)SAT certificate checking
@@ Property / cites work: Efficient verified (UN)SAT certificate checking / rank @@
+Normal rank
@@ Property / cites work @@
+Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
+Normal rank
@@ Property / cites work @@
+Formalization and implementation of modern SAT solvers
+Normal rank
@@ Property / cites work @@
+Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Recursive functions of symbolic expressions and their computation by machine, Part I
+Normal rank
@@ Property / cites work @@
+versat: A Verified Modern SAT Solver
@@ Property / cites work: versat: A Verified Modern SAT Solver / rank @@
+Normal rank
@@ Property / cites work @@
+The Mechanical Verification of a DPLL-Based Satisfiability Solver
+Normal rank
@@ Property / cites work @@
+Q3997095
@@ Property / cites work: Q3997095 / rank @@
+Normal rank
@@ Property / cites work @@
+Mechanical Verification of SAT Refutations with Extended Resolution
+Normal rank
@@ Property / cites work @@
+DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
+Normal rank