Compression of Propositional Resolution Proofs via Partial Regularization
From MaRDI portal
Publication:5200028
DOI10.1007/978-3-642-22438-6_19zbMath1341.68188MaRDI QIDQ5200028
Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo
Publication date: 29 July 2011
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-22438-6_19
Related Items
Labelled interpolation systems for hyper-resolution, clausal, and local proofs, Resolution proof transformation for compression and interpolation, Optimization techniques for Craig interpolant compaction in unbounded model checking, Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL, Implementation and Evaluation of Contextual Natural Deduction for Minimal Logic, Towards the Compression of First-Order Resolution Proofs by Lowering Unit Clauses
Uses Software
Cites Work