Normalformen (DNF, CNF)

Definitionen:

• Variable: v₁,… mathend000#
• Literal: v mathend000# oder ¬v mathend000#
• DNF-Klausel: Konjunktion von Literalen
• DNF-Formel: Disjunktion von DNF-Klauseln
• CNF-Klausel: Disjunktion von Literalen
• CNF-Formel: Konjunktion von CNF-Klauseln

Disjunktion als Implikation: diese Formeln sind äquivalent:

• (x₁∧…∧x_m)→(y₁∨…∨y_n) mathend000#
• (¬x₁∨…∨¬x_m∨y₁∨…∨y_n) mathend000#