Anzeige
Erschienen in:
2011 | OriginalPaper | Buchkapitel
Compression of Propositional Resolution Proofs via Partial Regularization
verfasst von : Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo
Erschienen in: Automated Deduction – CADE-23
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 two algorithms for the compression of propositional resolution proofs. The first algorithm,
RecyclePivots-WithIntersection
, performs partial regularization, removing an inference
η
when it is redundant in the sense that its pivot literal already occurs as the pivot of another inference located below in the path from
η
to the root of the proof. The second algorithm,
LowerUnits
, delays the resolution of (both input and derived) unit clauses, thus removing (some) inferences having the same pivot but possibly occurring also in different branches of the proof.