Was ist Konjunktiv Normalform?
Konjunktive Normalform (CNF) ist eine Annäherung an die Boolesche Logik, die Formeln als Konjunktionen von Klauseln mit AND oder OR ausdrückt. Jede Klausel, die durch eine Konjunktion oder AND verbunden ist, muss entweder ein Literal sein oder eine Disjunktion oder einen ODER-Operator enthalten. CNF ist nützlich für automatisierte Theorembeweise.
In der konjunktiven Normalform sind Aussagen in der Booleschen Logik Konjunktionen von Klauseln mit Teilsätzen von Disjunktionen. Mit anderen Worten, eine Anweisung ist eine Folge von ODERs, die durch UND verknüpft sind.
Beispielsweise:
(A ODER B) UND (C ODER D)
(A ODER B) UND (NICHT C ODER B)
Die Klauseln können auch Literale sein:
A ODER B
A UND B
Literale werden in CNF als Konjunktionen von Literalklauseln und Konjunktionen gesehen, die zufällig eine einzige Klausel haben. Es ist möglich, Anweisungen in CNF zu konvertieren, die in einer anderen Form geschrieben sind, z. B. in der disjunktiven Normalform.
