Compression of Propositional Resolution Proofs via Partial Regularization
From MaRDI portal
Publication:5200028
DOI10.1007/978-3-642-22438-6_19zbMath1341.68188OpenAlexW92083396MaRDI 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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (6)
Labelled interpolation systems for hyper-resolution, clausal, and local proofs ⋮ Towards the Compression of First-Order Resolution Proofs by Lowering Unit Clauses ⋮ Implementation and Evaluation of Contextual Natural Deduction for Minimal Logic ⋮ Optimization techniques for Craig interpolant compaction in unbounded model checking ⋮ Resolution proof transformation for compression and interpolation ⋮ Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL
Uses Software
Cites Work
This page was built for publication: Compression of Propositional Resolution Proofs via Partial Regularization