Definition
Eine Formel, die äquivalent als Konjunktion von Disjunktionen von Literalen dargestellt wird, häufig verwendet in Erfüllbarkeitslösungen und logischer Normalisierung.
Prinzip
Prinzip
Die KNF ordnet eine Formel als endliche Konjunktion von Klauseln, wobei jede Klausel eine Disjunktion von Literalen ist; logische Äquivalenzen (De Morgan, Distributivität) und Quantorenmanipulationen werden genutzt, um Formeln in KNF zu überführen und dabei Erfüllbarkeit oder Äquivalenz je nach angewandter Transformation zu erhalten.
Demonstration
Demonstration
Die Formel (p ∨ q) ∧ (¬p ∨ r) ist in KNF; um (p ∧ q) ∨ r in KNF zu überführen, wendet man Distributivität an und erhält (p ∨ r) ∧ (q ∨ r). In der automatischen Beweisführung werden KNF-Klauseln oft als Mengen von Literalen gehandhabt.
Fehlanwendung
Fehlanwendung
Die Annahme, die KNF-Umwandlung erhalte stets die logische Äquivalenz der Ausgangsformel, ist falsch; einige Verfahren führen frische Symbole oder Skolem-Funktionen ein und erzeugen nur eine erfüllbarkeitsäquivalente KNF, nicht eine tatsächlich äquivalente Form, was zu falschen Aussagen über Modell-Erhaltung führt.
Konsequenz
Konsequenz
Die Darstellung in KNF ermöglicht die direkte Nutzung von SAT-Solvern und resolutionbasierten Theorembeweisern, unterstützt Klausel-Indexierung und Unit-Propagation und standardisiert die Eingabe für viele Entscheidungsverfahren.
Umkehrung
Umkehrung
Die duale Sicht ist die Disjunktive Normalform (DNF), in der die Formel eine Disjunktion von Konjunktionen von Literalen ist; der Wechsel von KNF zu DNF kann Prime Implikanten offenlegen, verursacht jedoch häufig einen exponentiellen Größenzuwachs.
Abgrenzung
Abgrenzung
KNF verlangt, dass Klauseln Disjunktionen von Literalen sind; sie schreibt nicht die Quantorenstellung vor und behandelt reichere Junktoren nicht ohne Transformation, und naive Umwandlung kann zu exponentiellem Größenwachstum führen.
Semantische Spannung
Semantische Spannung
KNF vs Klauselmenge vs normalisierte Theorie: KNF als syntaktische Form steht in engem Zusammenhang mit der abstrakten Klauselmenge, die Solver verwenden; die Eins-zu-eins-Abbildung kann jedoch verschleiert werden, wenn frische Symbole oder Skolemierung Äquivalenzen verändern.
Synthese
Synthese
Die Konjunktive Normalform ist die kanonische syntaktische Gestalt, die eine Formel als Konjunktion disjunktiver Klauseln von Literalen anordnet; sie ist zentral für Erfüllbarkeitsalgorithmen und Normalisierungsworkflows, verlangt jedoch Vorsicht hinsichtlich Äquivalenz vs Erfüllbarkeitsäquivalenz.