Kanonische Normalform

Eine aussagenlogische Formel ist die kanonische Normalform (KNF, nicht zu verwechseln mit „Konjunktive Normalform“ (auch CNF); engl.: canonical normal form) zu einer weiteren aussagenlogischen Formel, wenn sie

• eine Normalform dieser aussagenlogischen Formel ist, d. h. eine zu dieser Formel äquivalente aussagenlogische Formel, die bestimmten syntaktischen Restriktionen unterliegt und
• für äquivalente aussagenlogische Formeln identisch und eindeutig ist.

Beispiele

• Disjunktive Normalformen sind im Allgemeinen nicht kanonisch, aber die maximale, bzw. erweiterte disjunktive Normalform (eine Disjunktive Normalform, die nur Minterme enthält, in denen alle Variablen vorhanden sind, jede Variable genau einmal vorkommt und deren Minterme alle voneinander verschieden sind) ist kanonisch
• Konjunktive Normalformen sind im Allgemeinen nicht kanonisch, aber die maximale, bzw. erweiterte konjunktive Normalform (eine Konjunktive Normalform, die nur Maxterme enthält, in denen alle Variablen vorhanden sind, jede Variable genau einmal vorkommt und deren Maxterme alle voneinander verschieden sind) ist kanonisch
• Die Ringsummennormalform (auch Reed-Muller-Normalform genannt) ist kanonisch
• Für eine feste Variablenordnung ist die reduzierte Shannon-Normalform kanonisch (Anwenden der Shannon-Zerlegung bei fester Variablenordnung und anschließendes Eliminieren redundanter Teilformeln). Diese Eigenschaft ist beispielsweise wichtig bei Binären Entscheidungsdiagrammen (BDDs), deren Grundlage die Shannon-Zerlegung bildet: Boolesche Operationen auf reduzierten geordneten BDDs (ROBDDs) bewahren hier stets die kanonische Normalform solcher Diagramme.

Anwendungsmöglichkeiten

Um die Äquivalenz zweier aussagenlogischer Formeln ${\displaystyle \alpha }$ und ${\displaystyle \beta }$ aufzuzeigen, können beide Formeln mit sämtlichen möglichen Interpretationen ausgewertet werden; liefern alle Interpretationen bei beiden Formeln jeweils denselben booleschen Wert, sind beide Formeln äquivalent.

Alternativ können beide Formeln auch in kanonische Normalformen KNF(${\displaystyle \alpha }$) und KNF(${\displaystyle \beta }$) transformiert werden; beide Formeln sind äquivalent genau dann, wenn KNF(${\displaystyle \alpha }$) = KNF(${\displaystyle \beta }$).

Außerdem können Fragen die Erfüllbarkeit und Allgemeingültigkeit einer Formel ${\displaystyle \gamma }$ betreffend mithilfe von kanonischen Normalformen beantwortet werden: so ist eine aussagenlogische Formel ${\displaystyle \gamma }$ erfüllbar genau dann, wenn KNF(${\displaystyle \gamma }$) ${\displaystyle \neq }$ KNF(0) und ${\displaystyle \gamma }$ ist allgemeingültig genau dann, wenn KNF(${\displaystyle \gamma }$) = KNF(1).

Größe kanonischer Normalformen

Es gilt, dass kanonischen Normalformen ein exponentieller Blow-Up inhärent ist; das heißt, eine kanonische Normalform ist im Allgemeinen exponentiell größer als diejenige aussagenlogische Formel, die in eine solche überführt wird; dies besagt das Aufzählungstheorem von Claude Elwood Shannon:

Sei a(n) die Zahl derjenigen aussagenlogischen Formeln mit n Variablen, deren kanonische Normalform nur polynomiell größer ist, dann steht dieser Zahl die Zahl sämtlicher möglicher Boolescher Funktionen B(n) mit n Variablen gegenüber, die ${\displaystyle 2^{2^{n}}}$ ist. Dann gilt: ${\displaystyle \lim _{n\to \inf }{\frac {a(n)}{B(n)}}=0}$.

Daraus folgt, dass die meisten kanonischen Normalformen exponentiell länger sind als eine beliebige aussagenlogische Formel, die in eine solche überführt wird; insbesondere steigt die Wahrscheinlichkeit, dass eine aussagenlogische Formel nur in eine exponentiell längere kanonische Normalform transformiert werden kann mit der Zahl der involvierten Variablen an; aufgrund dessen ist es auch nicht möglich, das Erfüllbarkeitsproblem der Aussagenlogik mithilfe von kanonischen Normalformen deterministisch mit polynomiellem Zeitaufwand zu lösen.

Unterschiedliche kanonische Normalformen können für eine bestimmte aussagenlogische Formel ein unterschiedliches Verhalten ihre Größe betreffend aufweisen: So ist zum Beispiel die kanonische disjunktive Normalform für die sog. Paritätsfunktion ${\displaystyle F_{n}=x_{1}\otimes ...\otimes x_{n}}$ exponentiell länger als ${\displaystyle F_{n}}$, die Länge der Reed-Muller-Normalform wächst dagegen nur polynomiell für ${\displaystyle F_{n}}$ mit größer werdendem n.