EVA STAR Trefferanzeige

Volltext Volltext.pdf1.pdf (216 KB)
URN (für Zitat) http://nbn-resolving.org/urn:nbn:de:swb:90-AAA349953
Titel Fast subsumption checks using anti-links.
Autor Ramesh, Anavai
Murray, Neil V.
Beckert, Bernhard
Haehnle, Reiner
Institution Fakultät für Informatik (INFORMATIK)
Institut für Logik, Komplexität und Deduktionssysteme (ILKD)
Dokumenttyp Buch
Jahr 1995
Erscheinungsvermerk Karlsruhe 1995. (Interner Bericht. Fakultät für Informatik, Universität Karlsruhe. 1995,24.)
Abstract
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.