Propositional proof skeletons
From MaRDI portal
Publication:6535365
DOI10.1007/978-3-031-30823-9_17zbMATH Open1543.68258MaRDI QIDQ6535365
Benjamin Kiesl-Reiter, Marijn J. H. Heule, Joseph E. Reeves
Publication date: 13 December 2023
Classical propositional logic (03B05) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Computational aspects of satisfiability (68R07)
Cites Work
- Unnamed Item
- Resolution proof transformation for compression and interpolation
- Efficient, verified checking of propositional proofs
- Incremental inprocessing in SAT solving
- \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
- Extending Sledgehammer with SMT solvers
- Efficient certified RAT verification
- Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
- Automated Proof Compression by Invention of New Definitions
- DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
- GRASP: a search algorithm for propositional satisfiability
- Theory and Applications of Satisfiability Testing
- Efficient verified (UN)SAT certificate checking
Related Items (1)
Recommendations
- Counting proofs in propositional logic π π
- Propositional consistency proofs π π
- Substructural Logic of Proofs π π
- Compositional Propositional Proofs π π
- Proof Systems for Effectively Propositional Logic π π
- Explicit Proofs in Formal Provability Logic π π
- Unnamed Item π π
- Unnamed Item π π
- Unnamed Item π π
- Unnamed Item π π
This page was built for publication: Propositional proof skeletons