Decomposable negation normal form (DNNF) was developed primarily for knowledge compilation. Formulas in DNNF are linkless, in negation normal form (NNF), and have the property that atoms are not shared across conjunctions. Full dissolvents are linkless NNF formulas that do not in general have the latter property. However, many of the applications of DNNF can be obtained with full dissolvents. Two additional methods — regular tableaux and semantic factoring — are shown to produce equivalent DNNF. A class of formulae is presented on which earlier DNNF conversion techniques are necessarily exponential; path dissolution and semantic factoring handle these formulae in linear time.
CITATION STYLE
Murray, N. V., & Rosenthal, E. (2003). Tableaux, path dissolution, and decomposable negation normal form for knowledge compilation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2796, pp. 165–180). Springer Verlag. https://doi.org/10.1007/978-3-540-45206-5_14
Mendeley helps you to discover research relevant for your work.