Wikipedia · einfach zusammengefasst · Stand
Klausel-Normalform
Klauselnormalformen sind über eine Transformation erstellbar und dienen zur maschinellen Beweisführung über logischen Formeln. Inhaltsverzeichnis. 1 Beispiel 1 …
Inhalt4 Abschnitte
Begriff und Bedeutung
Die Klauselform oder Klauselnormalform ist eine Darstellungsweise für logische Formeln. Bei einer Formel in konjunktiver Normalform (KNF) werden die durch Konjunktionen, also UND-Verknüpfungen, verbundenen Bestandteile in Mengenschreibweise zusammengefasst. Eine Klausel ist dabei eine Menge von Literalen. Ein Literal ist entweder eine atomare Aussage wie a oder ihre Negation wie ¬a.
Allgemeiner beschreibt der Artikel eine Formel in Klauselform als logische Verknüpfung von Literalen, die als disjunktive oder konjunktive Normalform notiert wird. Für leere Verknüpfungen gilt: Die leere verallgemeinerte Disjunktion, also eine ODER-Verknüpfung ohne Bestandteile, hat den Wahrheitswert falsch. Die leere verallgemeinerte Konjunktion, also eine UND-Verknüpfung ohne Bestandteile, hat den Wahrheitswert wahr.
Klauselnormalformen können durch Transformation aus anderen logischen Formeln erzeugt werden. Sie sind besonders für die maschinelle Beweisführung über logische Formeln wichtig. Der Artikel weist allerdings darauf hin, dass für seine Angaben Belege aus der Fachliteratur zur mathematischen Logik fehlen.
Darstellung einer KNF als Klauselmenge
Die Formel
((a ∨ b) ∧ (b ∨ c) ∧ (a ∨ ¬d ∨ ¬e) ∧ d)
steht in konjunktiver Normalform. Die gesamte Formel ist eine UND-Verknüpfung mehrerer Klauseln; innerhalb jeder Klausel sind die Literale durch ODER verbunden.
In Klauselform wird sie als Menge von Mengen geschrieben:
{{a,b},{b,c},{a,¬d,¬e},{d}}
Dabei entspricht jede innere Menge genau einer durch ODER verknüpften Klausel. Beispielsweise steht {a,b} für a ∨ b. Die einelementige Klausel {d} steht unmittelbar für das Literal d. Die äußere Menge fasst die Klauseln zusammen, die in der ursprünglichen KNF durch UND miteinander verbunden sind.
Transformation in konjunktive Klauselform
Die aussagenlogische Formel
¬(P ∨ (¬(P ∧ Q) ∧ ¬R))
wird schrittweise in konjunktive Klauselform umgeformt. Zunächst wird sie als verallgemeinerte Konjunktion aufgefasst:
{¬(P ∨ (¬(P ∧ Q) ∧ ¬R))}
Danach werden die Negationen mithilfe der logischen Umformungsregeln nach innen verschoben. Die im Artikel angegebenen Schritte lauten:
{{¬P},{¬(¬(P ∧ Q) ∧ ¬R)}}
{{¬P},{¬¬(P ∧ Q),¬¬R}}
{{¬P},{(P ∧ Q),R}}
Im letzten Schritt wird die noch enthaltene Konjunktion P ∧ Q so verteilt, dass ausschließlich Klauseln mit disjunktiv verbundenen Literalen übrig bleiben. Das Ergebnis ist:
{{¬P},{P,R},{Q,R}}
Die ursprüngliche Formel ist damit als Konjunktion der drei Klauseln ¬P, P ∨ R und Q ∨ R dargestellt.
Hornklauseln
Hornklauseln sind eine besondere Form von Klauseln in Klauselnormalform. Jede Hornklausel enthält höchstens ein positives Literal, also höchstens ein Literal ohne Negationszeichen.
Man unterscheidet:
- Eine negative Hornklausel enthält kein positives Literal.
- Eine positive Hornklausel enthält genau ein positives Literal.
Hornklauseln sind beliebt, weil sie sich schnell in eine Menge von Implikationen umformen lassen. Eine Implikation hat die Form Voraussetzung ⇒ Folgerung.
Als Beispiel nennt der Artikel die Klauselmenge
{{a,¬b},{¬c,¬d},{b}}.
Ein dazu äquivalenter Ausdruck ist:
(¬a ⇒ ¬b) ∧ (c ⇒ ¬d) ∧ (true ⇒ b).
Eine weitere mögliche Schreibweise lautet:
(b ⇒ a) ∧ (c ∧ d ⇒ false) ∧ (true ⇒ b).
Dabei zeigt die zweite Schreibweise typische Deutungen von Hornklauseln: Die Klausel {a,¬b} wird als b ⇒ a gelesen. Die rein negative Klausel {¬c,¬d} entspricht c ∧ d ⇒ false. Die Klausel {b}, die nur aus einem positiven Literal besteht, entspricht true ⇒ b.