KIT | KIT-Bibliothek | Impressum | Datenschutz

Fast subsumption checks using anti-links

Ramesh, Anavai; Murray, Neil V.; Beckert, Bernhard; Haehnle, Reiner


The concept of "anti-link" is defined, and useful
equivalence-preserving operations based on anti-links are
introduced.These operations eliminate a potentially large number
of subsumed paths in a negation normal form formula.Those
anti-links that directly indicate the presence of subsumed paths
are characterized. The operations have linear time complexity in
the size of that part of the formula containing the anti-link.

The problem of removing all subsumed paths in an NNF formula is
shown to be NP-hard, even though such formulas may be small
relative to the size of their path sets. The general problem of
determining whether there exists a pair of subsumed paths
associated with an arbitrary anti-link is shown to be NP-complete.
Additional techniques based on "strictly pure full blocks" are
introduced and are also shown to eliminate redundant subsumption
checks. The effectiveness of these techniques is examined with
respect to some benchmark examples from the literature.

Open Access Logo

Volltext §
DOI: 10.5445/IR/34995
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Logik, Komplexität und Deduktionssysteme (ILKD)
Publikationstyp Buch
Publikationsjahr 1995
Sprache Englisch
Identifikator urn:nbn:de:swb:90-AAA349953
KITopen-ID: 34995
Erscheinungsvermerk Karlsruhe 1995. (Interner Bericht. Fakultät für Informatik, Universität Karlsruhe. 1995,24.)
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page