Efficient, verified checking of propositional proofs
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 46981 (Why is no real title available?)
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
- A verified SAT solver framework with learn, forget, restart, and incrementality
- DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
- Efficient certified RAT verification
- Efficient execution in an automated reasoning environment
- Efficient verified (UN)SAT certificate checking
- Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
- Formalization and implementation of modern SAT solvers
- Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
- Inprocessing rules
- Mechanical verification of SAT refutations with extended resolution
- Recursive functions of symbolic expressions and their computation by machine, Part I
- Rough diamond: an extension of equivalence-based rewriting
- The mechanical verification of a DPLL-based satisfiability solver
- Theory and Applications of Satisfiability Testing
- Verifying Refutations with Extended Resolution
- versat: A Verified Modern SAT Solver
Cited in
(34)- On the concrete efficiency of probabilistically-checkable proofs
- Formally verifying the solution to the Boolean Pythagorean triples problem
- Compositional propositional proofs
- Generating extended resolution proofs with a BDD-based SAT solver
- Milestones from the Pure Lisp Theorem Prover to ACL2
- Efficiently checking propositional refutations in HOL theorem provers
- Efficient verified (UN)SAT certificate checking
- Verification in ACL2 of a generic framework to synthesize SAT-provers
- Batch ZK Proof and Verification of OR Logic
- Propositional proof skeletons
- Mechanical verification of SAT refutations with extended resolution
- A certified constraint solver over finite domains
- Certifying emptiness of timed Büchi automata
- Simulating strong practical proof systems with extended resolution
- Efficient certified RAT verification
- Unsatisfiability proofs for distributed clause-sharing SAT solvers
- Rocket-Fast Proof Checking for SMT Solvers
- Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof
- Using an induction prover for verifying arithmetic circuits
- SAT-enhanced Mizar proof checking
- \textsc{Carcara}: an efficient proof checker and elaborator for SMT proofs in the Alethe format
- Efficient verified (UN)SAT certificate checking
- The propositional formula checker HeerHugo
- SMT proof checking using a logical framework
- Tools and Algorithms for the Construction and Analysis of Systems
- The mechanical verification of a DPLL-based satisfiability solver
- Clause redundancy and preprocessing in maximum satisfiability
- A resolution-based interactive proof system for UNSAT
- Efficient Probabilistically Checkable Debates
- Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker
- DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
- scientific article; zbMATH DE number 7649971 (Why is no real title available?)
- Verified AIG algorithms in ACL2
- \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
This page was built for publication: Efficient, verified checking of propositional proofs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1687744)
