Compressing propositional refutations
From MaRDI portal
Recommendations
- Data compression for proof replay
- A Compressing Translation from Propositional Resolution to Natural Deduction
- Compression of propositional resolution proofs by lowering subproofs
- Compression of propositional resolution proofs via partial regularization
- An efficient and flexible approach to resolution proof reduction
Cites work
- A machine program for theorem-proving
- A Proof Procedure Using Connection Graphs
- Extended Resolution Proofs for Symbolic SAT Solving with Quantification
- scientific article; zbMATH DE number 234014 (Why is no real title available?)
- Logic Programming
- On Matrices with Connections
- Refutations by Matings
- Theory and Applications of Satisfiability Testing
- Tools and Algorithms for the Construction and Analysis of Systems
Cited in
(11)- Efficiently checking propositional refutations in HOL theorem provers
- Data compression for proof replay
- Extracting unsatisfiable cores for LTL via temporal resolution
- Compression of propositional resolution proofs by lowering subproofs
- Propositional proof compressions and DNF logic
- Fast DQBF Refutation
- Towards the compression of first-order resolution proofs by lowering unit clauses
- Resolution proof transformation for compression and interpolation
- Shortening of proof length is elusive for theorem provers
- Compression of propositional resolution proofs via partial regularization
- An efficient and flexible approach to resolution proof reduction
This page was built for publication: Compressing propositional refutations
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5178991)
