Normal Forms for Knowledge Compilation

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.

• Type: Conference
• Year: 2005
• Where: ISMIS
• Authors: Reiner Hähnle, Neil V. Murray, Erik Rosenthal
• Keywords: ISMIS 2005, Negated Form, Negation Normal Form, Reduced Factored Negation