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
- scientific article; zbMATH DE number 234014 (Why is no real title available?)
- A Proof Procedure Using Connection Graphs
- A machine program for theorem-proving
- Extended Resolution Proofs for Symbolic SAT Solving with Quantification
- 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)- Extracting unsatisfiable cores for LTL via temporal resolution
- Resolution proof transformation for compression and interpolation
- Shortening of proof length is elusive for theorem provers
- Efficiently checking propositional refutations in HOL theorem provers
- Propositional proof compressions and DNF logic
- Compression of propositional resolution proofs via partial regularization
- An efficient and flexible approach to resolution proof reduction
- Fast DQBF Refutation
- Data compression for proof replay
- Towards the compression of first-order resolution proofs by lowering unit clauses
- Compression of propositional resolution proofs by lowering subproofs
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)
