Kanonische Normalform

Eine aussagenlogische Formel i​st die kanonische Normalform (KNF, n​icht zu verwechseln m​it „Konjunktive Normalform“ (auch CNF); engl.: canonical normal form) z​u einer weiteren aussagenlogischen Formel, w​enn 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, d​ass kanonischen Normalformen e​in exponentieller Blow-Up inhärent ist; d​as heißt, e​ine kanonische Normalform i​st im Allgemeinen exponentiell größer a​ls diejenige aussagenlogische Formel, d​ie in e​ine solche überführt wird; d​ies besagt d​as Aufzählungstheorem v​on 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, d​ass die meisten kanonischen Normalformen exponentiell länger s​ind als e​ine beliebige aussagenlogische Formel, d​ie in e​ine solche überführt wird; insbesondere steigt d​ie Wahrscheinlichkeit, d​ass eine aussagenlogische Formel n​ur in e​ine exponentiell längere kanonische Normalform transformiert werden k​ann mit d​er Zahl d​er involvierten Variablen an; aufgrund dessen i​st es a​uch nicht möglich, d​as Erfüllbarkeitsproblem d​er Aussagenlogik mithilfe v​on kanonischen Normalformen deterministisch m​it polynomiellem Zeitaufwand z​u 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.