Abstract
A class of formulas called factored negation normal form is introduced. They are closely related to BDDs, but there is a DPLL-like tableau procedure for computing them that operates in PSPACE. Ordered factored negation normal form provides a canonical representation for any boolean function. Reduction strategies are developed that provide a unique reduced factored negation normal form. These compilation techniques work well with negated form as input, and it is shown that any logical formula can be translated into negated form in linear time. © Springer-Verlag Berlin Heidelberg 2005.
Cite
CITATION STYLE
Hähnle, R., Murray, N. V., & Rosenthal, E. (2005). Normal forms for knowledge compilation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3488 LNAI, pp. 304–313). Springer Verlag. https://doi.org/10.1007/11425274_32
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
