Efficient, verified checking of propositional proofs
From MaRDI portal
Recommendations
Cites work
- 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
- scientific article; zbMATH DE number 46981 (Why is no real title available?)
- 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
(40)- Efficiently checking propositional refutations in HOL theorem provers
- Using an induction prover for verifying arithmetic circuits
- The propositional formula checker HeerHugo
- Certifying emptiness of timed Büchi automata
- Generating extended resolution proofs with a BDD-based SAT solver
- Clause redundancy and preprocessing in maximum satisfiability
- Simulating strong practical proof systems with extended resolution
- \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
- Milestones from the Pure Lisp Theorem Prover to ACL2
- Formally verifying the solution to the Boolean Pythagorean triples problem
- Efficient certified RAT verification
- SMT proof checking using a logical framework
- Verification in ACL2 of a generic framework to synthesize SAT-provers
- Efficient Probabilistically Checkable Debates
- DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
- Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof
- Compositional propositional proofs
- Batch ZK Proof and Verification of OR Logic
- A certified constraint solver over finite domains
- The mechanical verification of a DPLL-based satisfiability solver
- Mechanical verification of SAT refutations with extended resolution
- Rocket-Fast Proof Checking for SMT Solvers
- On the concrete efficiency of probabilistically-checkable proofs
- SAT-enhanced Mizar proof checking
- scientific article; zbMATH DE number 7649971 (Why is no real title available?)
- Tools and Algorithms for the Construction and Analysis of Systems
- Efficient verified (UN)SAT certificate checking
- Efficient verified (UN)SAT certificate checking
- Propositional proof skeletons
- Unsatisfiability proofs for distributed clause-sharing SAT solvers
- \textsc{Carcara}: an efficient proof checker and elaborator for SMT proofs in the Alethe format
- Verified AIG algorithms in ACL2
- A resolution-based interactive proof system for UNSAT
- Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker
- Trusted scalable SAT solving with on-the-fly LRAT checking
- Producing proofs of unsatisfiability with distributed clause-sharing SAT solvers
- Fast and verified UNSAT certificate checking
- Certifying phase abstraction
- A resolution-based interactive proof system for UNSAT
- Verifying Datalog reasoning with Lean
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)
