OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Compression of Propositional Resolution Proofs by Lowering Subproofs

Boudou, Joseph and Woltzenlogel Paleo, Bruno Compression of Propositional Resolution Proofs by Lowering Subproofs. (2013) In: 22nd International Conference TABLEAUX : Automated Reasoning with Analytic Tableaux and Related Methods - TABLEAUX 2013, 16 September 2013 - 19 September 2013 (Nancy, France).

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL: http://dx.doi.org/10.1007/978-3-642-40537-2_7


This paper describes a generalization of the LowerUnits algorithm for the compression of propositional resolution proofs. The generalized algorithm, here called LowerUnivalents, is able to lower not only units but also subproofs of non-unit clauses, provided that they satisfy some additional conditions. This new algorithm is particularly suited to be combined with the RecyclePivotsWithIntersection algorithm. A formal proof that LowerUnivalents always compresses more than LowerUnits is shown, and both algorithms are empirically compared on thousands of proofs produced by the SMT-Solver veriT.

Item Type:Conference or Workshop Item (Paper)
Additional Information:Thanks to Springer editor. The definitive version is available at http://www.springer.com The original PDF of the article can be found at Springer website : http://link.springer.com/chapter/10.1007/978-3-642-40537-2_7
HAL Id:hal-01166922
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE)
Other partners > Technische Universität Wien - TU Wien (AUSTRIA)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Laboratory name:
Deposited On:21 Apr 2015 09:55

Repository Staff Only: item control page