Anzeige
Erschienen in:
2013 | OriginalPaper | Buchkapitel
Compression of Propositional Resolution Proofs by Lowering Subproofs
verfasst von : Joseph Boudou, Bruno Woltzenlogel Paleo
Erschienen in: Automated Reasoning with Analytic Tableaux and Related Methods
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
This paper describes a generalization of the
LowerUnits
algorithm [8] for the compression of propositional resolution proofs. The generalized algorithm, 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 [8]. 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
.