4.4 Normalformen

© 1999 Fran�ois Bry
Dieses Lehrmaterial wird ausschlie�lich zur privaten Verwendung angeboten. Eine nichtprivate Nutzung (z.B. im Unterricht oder eine Ver�ffentlichung von Kopien oder �bersetzungen) dieses Lehrmaterials bedarf der Erlaubnis des Autors.

4.4 Normalformen

Viele Beweismethoden sind der Einfachheit halber nur für Formeln von eingeschränkter syntaktischer Gestalt definiert. Formeln einer anderen Gestalt müssen zunächst ,,normalisiert`` werden, das heißt, in die entsprechende syntaktische Gestalt umgewandelt. Wir haben zum Beispiel in Kapitel 3 gesehen, dass jede Formel der Prädikatenlogik erster Stufe äquivalent zu einer Formel in Pränexform ist. Die Pränexform ist eine typische ,,Normalform``, die von einer Beweismethode vorausgesetzt werden kann.

Dieser Abschnitt behandelt einige dieser Normalformen, die für die zu besprechenden Beweismethoden von Bedeutung sind.

Definition 4.4.2 (Polyadische Junktoren). Für jedes n≥0 seien
F₁,...,F_n Formeln einer Sprache der Aussagenlogik oder der Prädikatenlogik erster Stufe.

∧*(F₁,...,F_n) bezeichnet die polyadische Konjunktion von F₁,...,F_n.
Die Modellbeziehung wird für jede Interpretation M darauf erweitert:
M∧*(F₁,...,F_n) gdw. für alle i mit 1≤i≤n gilt MF_i.
∨*(F₁,...,F_n) bezeichnet die polyadische Disjunktion von F₁,...,F_n.
Die Modellbeziehung wird für jede Interpretation M darauf erweitert:
M∨*(F₁,...,F_n) gdw. es gibt ein i mit 1≤i≤n und MF_i.

Bemerkungen:

∧* und ∨* haben beliebig viele Argumente und nicht etwa stets n Argumente für ein festes n (dafür wäre die Schreibweise ∧ⁿ und ∨ⁿ).
Bei null Argumenten besagt diese Definition, dass für jede Interpretation M gilt M∧*() und M gilt M∨*().
∧*()
∧*(F₁)F₁
∧*(F₁,F₂) (F₁∧F₂)
∧*(F₁,F₂,F₃) (F₁∧(F₂∧F₃))

∨*()
∨*(F₁)F₁
∨*(F₁,F₂) (F₁∨F₂)
∨*(F₁,F₂,F₃) (F₁∨(F₂∨F₃))
Man könnte also auch definieren
∧*(F₁,...,F_n):=(F₁∧...∧F_n) und ∨*(F₁,...,F_n):=(F₁∨...∨F_n)
mit zum Beispiel rechtsassoziativer Klammerung. Damit wären aber die Fälle mit null und mit einem Argument nicht erklärt.

Das König'sche Unendlichkeitslemma

Dieser Einschub behandelt ein bekanntes Ergebnis über Bäume, das auch außerhalb der Logik nützlich ist, insbesondere für Terminierungsnachweise.

Wenn es eine Obergrenze n gibt, so dass jeder Knoten im Baum höchstens n direkte Nachfolger hat, dann hat der Baum endlichen Verzweigungsgrad. Aber er kann auch endlichen Verzweigungsgrad haben, ohne dass so eine Obergrenze existiert. Zum Beispiel kann die Wurzel zwei direkte Nachfolger haben, der erste davon drei direkte Nachfolger, der erste davon vier usw.

Beweis: Sei K ein beliebiger Knoten in T. Wegen des endlichen Verzweigungsgrads hat er endlich viele direkte Nachfolger. Falls jeder davon Wurzel eines Teilbaums mit endlich vielen Knoten ist, dann ist auch K selbst Wurzel eines Teilbaums mit endlich vielen Knoten.

Durch Kontraposition, und weil K beliebig ist, erhalten wir: wenn ein Knoten in T Wurzel eines Teilbaums mit unendlich vielen Knoten ist, dann hat er mindestens einen direkten Nachfolger, der ebenfalls Wurzel eines Teilbaums mit unendlich vielen Knoten ist.

Sei K₀ die Wurzel von T, also die Wurzel eines Teilbaums mit unendlich vielen Knoten. K hat mindestens einen direkten Nachfolger, der die Wurzel eines Teilbaums mit unendlich vielen Knoten ist, also sei K₁ ein solcher Nachfolger. K₁ hat wieder mindestens einen solchen Nachfolger, also sei K₂ einer davon, und so weiter. Auf diese Weise kann ein unendlicher Ast K₀,K₁,K₂,... konstruiert werden.

Es gibt ein gedankliches Spiel, das eine hübsche Illustration für die Anwendung des König'schen Unendlichkeitslemmas liefert. Gegeben sei ein Vorrat von Münzen, die mit natürlichen Zahlen beschriftet sind. Für jede Zahl seien unbegrenzt viele Münzen mit dieser Zahl verfügbar. Gegeben sei außerdem ein Sparschwein, das am Anfang genau eine Münze enthält.

Ein Spielzug besteht darin, eine Münze aus dem Sparschwein herauszunehmen (und der eigenen Geldbörse einzuverleiben) und dafür beliebig viele, aber endlich viele, Münzen aus dem Vorrat in das Sparschwein hineinzulegen. Diese Münzen können mit gleichen oder verschiedenen Zahlen beschriftet sein, aber jede dieser Zahlen muss echt kleiner sein als die Zahl auf der herausgenommenen Münze.

Das Spiel kann immer mit dem ersten Spielzug beendet werden, indem man die ursprüngliche Münze herausnimmt und null Münzen dafür hineinlegt. Offensichtlich kann man auf diese Weise von jedem Zustand aus das Spiel mit endlich vielen Spielzügen beenden. Weniger offensichtlich ist die Frage, ob man die Spielzüge so wählen kann, dass das Spiel nicht endet, dass man sich also unendlich oft aus dem Sparschwein bedienen kann, ohne dass es je leer wird. Man könnte ja zum Beispiel die erste Münze herausnehmen und dafür 10 neue hineinlegen; dann nimmt man eine davon wieder heraus und legt dafür 100 neue hinein; bei jedem Schritt verzehnfacht man die Anzahl der Münzen, die man hineinlegt.

Jeder mögliche Spielverlauf kann durch einen Baum dargestellt werden: die Wurzel ist die Münze, die am Anfang im Sparschwein ist, die direkten Nachfolger einer Münze sind die Münzen, durch die sie bei einem Spielzug ersetzt wird. Die Knoten des Baums repräsentieren also sämtliche Münzen, die bei diesem Spielverlauf jemals in das Sparschwein kommen.

Jeder dieser Bäume hat endlichen Verzweigungsgrad, da bei jedem Spielzug nur endlich viele neue Münzen in das Sparschwein kommen. Außerdem ist jeder Knoten außer der Wurzel mit einer kleineren Zahl beschriftet als sein Vorgänger. Also kann kein Ast eines solchen Baums länger sein als die Zahl, mit der die Wurzel beschriftet ist, das heißt, jeder Ast in einem solchen Baum ist endlich.

Nach dem König'schen Unendlichkeitslemma hat jeder dieser Bäume nur endlich viele Knoten. Also terminiert jeder mögliche Spielverlauf.

Das Spiel entspricht einem nichtdeterministischen Algorithmus mit sehr vielen Wahlmöglichkeiten, nicht einmal eine Obergrenze für den Verzweigungsgrad ist vorgegeben. Das König'sche Unendlichkeitslemma ermöglicht in solchen Fällen Ergebnisse der Art: ,,wie auch immer diese Wahlmöglichkeiten ausgenutzt werden, der Algorithmus terminiert in jedem Fall.``

Aussagenlogische Normalformen

In diesem Abschnitt ist mit der Bezeichnung ,,Konjunktion`` immer eine Formel der Gestalt ∧*(...) gemeint, mit ,,Disjunktion`` eine Formel der Gestalt ∨*(...), einschließlich der Fälle mit null Argumenten.

Definition 4.4.4

Sei A eine atomare Formel der Aussagenlogik. Ein Literal hat eine der Gestalten A oder ¬A. Ein Literal der Gestalt A heißt positiv, ein Literal der Gestalt ¬A negativ. Das Komplement eines positiven Literals A ist ¬A, das Komplement eines negativen Literals ¬A ist A.
Eine Klausel ist eine Disjunktion von Literalen.
Eine aussagenlogische Formel heißt in konjunktiver Normalform, wenn sie eine Konjunktion von Klauseln ist.
Eine Klausel in Implikationsnormalform hat die Gestalt (R⇒K), wobei R (für Rumpf) eine Konjunktion und K (für Kopf) eine Disjunktion von positiven Literalen, also von atomaren Formeln, ist.
Eine aussagenlogische Formel heißt in Implikationsnormalform, wenn sie eine Konjunktion von Klauseln in Implikationsnormalform ist.

Ein Beispiel für eine Klausel ist ∨*(p,¬q,r,¬s). Die Implikationsnormalform dieser Klausel ist (∧*(q,s)⇒∨(p,r)). Eine andere Klausel ist ∨*(). Für diese ,,leere Klausel`` ist auch die Notation verbreitet. Sie ist, wie bereits erwähnt, logisch äquivalent mit .

Bemerkung: In Kapitel 2 wurden

und

als nullstellige Junktoren eingeführt und nicht als atomare Formeln. Die Formeln

, ¬

sind also keine Literale und können deshalb nicht in einer Klausel vorkommen.

Eine Klausel kann auch als Menge von Literalen definiert werden. Dann sind zum Beispiel die logisch äquivalenten Klauseln ∨*(p,¬q,p), ∨*(p,p,¬q) und ∨*(p,¬q) alle durch dieselbe Menge {p,¬q} repräsentiert. Für Implementierungen ist es aber oft günstiger, solche Klauseln zu unterscheiden.

Man kann natürlich ganz analog die disjunktive Normalform definieren als eine Disjunktion von Konjunktionen von Literalen. Diese Normalform spielt aber für die hier behandelten Beweismethoden keine Rolle.

Sowohl n=0 als auch m=0 sind dabei möglich. Dass diese Transformation die logische Äquivalenz erhält, folgt unmittelbar aus den Definitionen.

Definition 4.4.6 (Umschreibungsregeln für Disjunktionen).

∨*(... ¬¬G ...)
___________
∨*(... G ...)

∨*(... ¬(G₁∧G₂) ...)
_________________
∨*(... ¬G₁,¬G₂ ...)

∨*(... ¬(G₁∨G₂) ...)
_________________
∨*(... G₁,G₂ ...)

∨*(... ¬(G₁⇒G₂) ...)
_________________
∨*(... ¬G₁,G₂ ...)

∨*(... ¬(G₁⇔G₂) ...)
____________________________
∨*(... ¬G₁,G₂ ...),∨*(... G₁,¬G₂ ...)

∨*(...

...)
___________
∨*(... ...)

∨*(...

...)
___________

∨*(... (G₁∧G₂) ...)
____________________________
∨*(... G₁ ...),∨*(... G₂ ...)

∨*(... ¬(G₁∨G₂) ...)
____________________________
∨*(... ¬G₁ ...),∨*(... ¬G₂ ...)

∨*(... ¬(G₁⇒G₂) ...)
____________________________
∨*(... G₁ ...),∨*(... ¬G₂ ...)

∨*(... ¬(G₁⇔G₂) ...)
____________________________
∨*(... G₁,G₂ ...),∨*(... ¬G₁,¬G₂ ...)

∨*(... ¬

...)
___________

∨*(...

...)
___________
∨*(... ...)

Diese Umschreibungsregeln dienen als Hilfsmittel zur Berechnung einer konjunktiven Normalform einer aussagenlogischen Formel F. Sie sind dafür vorgesehen, auf eine Disjunktion angewandt zu werden, die in einer Sequenz von Argumenten von ∧* vorkommt. Bei der Anwendung einer Umschreibungsregel wird eine Disjunktion durch eine Teilsequenz ersetzt, die aus einer einzigen Disjunktion bestehen kann (z.B. im obersten linken Fall) oder aus zwei Disjunktionen (z.B. im obersten rechten Fall) oder aus null Disjunktionen (z.B. im untersten linken Fall).

Definition 4.4.7 (Transformation in konjunktive Normalform)

Nichtdeterministischer Algorithmus konjunktive_normalform(F):

Initialisierung: K:=∧*(∨*(F))
Solange es in K=∧*(D₁,...,D_m) eine Disjunktion gibt, die keine Klausel ist:
- (a) Wähle eine solche Disjunktion D_j=∨*(F₁,...,F_m) aus K aus.
- (b) Wähle eine Formel F_i aus D_j aus, die kein Literal ist.
- (c) Bestimme die Umschreibungsregel für D_j gemäß Definition 4.4.6, die auf die Gestalt von F_i passt.
- (d) Wende die Umschreibung auf D_j innerhalb von K an.
  (Dadurch ändert sich der Wert von K.)
Liefere K als Ergebnis.

Zum Beispiel ergeben sich für F=(p∨(q∧(r∨ ))) der Reihe nach folgende Werte für K:

∧*(∨*[(p∨(q∧(r∨ )))])

∧*(∨*[p, (q∧(r∨ ))])

∧*(∨*[p,q], ∨*[p,(r∨ )])

∧*(∨*[p,q], ∨*[p,r, ])

∧*(∨*[p,q], ∨*[p,r])

In diesem Beispiel ist keine andere Folge von Werten für K möglich. In der letzten Zeile sind beide Disjunktionen Klauseln. Jede andere Zeile enthält genau eine Disjunktion, die keine Klausel ist, und jede davon enthält genau eine Formel, die kein Literal ist. Im allgemeinen kann es aber in beiden Fällen mehrere Möglichkeiten geben. Die Schritte 2(a) und 2(b) sind nichtdeterministisch. Dagegen ist die Umschreibungsregel in Schritt 2(c) eindeutig bestimmt, sobald F_i gewählt ist. Dies ergibt sich unmittelbar aus dem Eindeutigkeitssatz 2.1.7 (erweitert auf ∧* und ∨*).

Beweis:

Wir definieren nach dem Prinzip der strukturellen Rekursion eine Funktion rg, genannt Rang, die jeder aussagenlogischen Formel eine natürliche Zahl zuordnet:

rg(A)	:= 0	A atomare Formel
rg():= rg()	:= 1
rg(¬G)	:= 1+rg(G)
rg((G₁θG₂))	:= 2+rg(G₁)+rg(G₂)	θ zweistelliger Junktor

Intuitiv ist der Rang die Anzahl der Junktoren in einer Formel, wobei zweistellige Junktoren doppelt zählen. Wir erweitern die Funktion auf Disjunktionen: rg(∨*(F₁,...,F_n)):= rg(F₁)+...+rg(F_n).

Man prüft leicht nach, dass für jede Umschreibungsregel in Definition 4.4.6 gilt, dass jede Disjunktion unterhalb des Strichs einen echt kleineren Rang hat als die Disjunktion oberhalb des Strichs.

Die Konjunktion K=∧*(...) enthält initial genau eine Disjunktion. Bei jedem Schleifendurchgang wird eine der Disjunktionen in K durch maximal zwei Disjunktionen mit echt kleinerem Rang ersetzt. Der so konstruierbare Baum aller Disjunktionen, die jemals in Schritt 2 umgeschrieben werden, hat endlichen Verzweigungsgrad und nur endliche Äste, also nach dem König'schen Unendlichkeitslemma endlich viele Knoten.

K ist initial eine Konjunktion von Disjunktionen und bleibt bei jedem Durchgang durch Schritt 2 eine Konjunktion von Disjunktionen.
Nach Beendigung der Schleife (Schritt 2) ist jede Disjunktion in K eine Klausel (sonst wäre die Schleife noch nicht beendet), das heißt, K ist in konjunktiver Normalform.
Initial gilt K=∧*(∨*(F))F. Man prüft leicht nach, dass die logische Äquivalenz bei jeder Anwendung einer Umschreibungsregel auf eine Disjunktion in K erhalten bleibt.

Das Terminierungsargument ist analog zu dem Spiel mit den Münzen: K=∧*(...) entspricht dem Sparschwein, die Disjunktionen den Münzen.

Der Nichtdeterminismus im Ablauf des Algorithmus hat auch einen Nichtdeterminismus bezüglich seines Ergebnisses zur Folge. Zum Beispiel kann konjunktive_normalform(((p∧q)∨(r∧s))) je nach der getroffenen Wahl in Schritt 2(a) entweder ∧*(∨*(p,r), ∨*(p,s), ∨*(q,r), ∨*(q,s)) ergeben oder ∧*(∨*(p,r), ∨*(q,r), ∨*(p,s), ∨*(q,s)). Dieser Unterschied in der Reihenfolge der Klauseln ist aber uninteressant.

Der obige Satz garantiert, dass jeder deterministische Algorithmus, der durch geeignete Festlegung der Auswahl in den Schritten 2(a) und 2(b) definiert werden kann, die relevanten Eigenschaften besitzt.

Man kann als Datenstruktur für das K im Algorithmus statt einer Konjunktion eine Menge wählen (also Mehrfachvorkommen von Disjunktionen vermeiden). Dann liefert der Algorithmus als Ergebnis eine endliche Menge von Klauseln.

Normalformen für die Prädikatenlogik erster Stufe

Die Begriffe Literal und Klausel werden völlig analog zur Aussagenlogik definiert, nur dass die Grundlage jetzt atomare Formeln im Sinne der Prädikatenlogik statt der Aussagenlogik sind. Die konjunktive Normalform wird als spezielle Pränexform definiert. Zusätzlich gibt es Normalformen, die gar keine expliziten Quantoren enthalten.

Definition 4.4.10

Sei A eine atomare Formel der Prädikatenlogik erster Stufe. Ein Literal hat eine der Gestalten A oder ¬A. Ein Literal der Gestalt A heißt positiv, ein Literal der Gestalt ¬A negativ. Das Komplement eines positiven Literals A ist ¬A, das Komplement eines negativen Literals ¬A ist A.
Eine Formel der Prädikatenlogik erster Stufe heißt rektifiziert, wenn die Variablen, die unmittelbar hinter einem Vorkommen eines Quantors in der Formel stehen, paarweise verschieden und verschieden von allen freien Variablen in der Formel sind. (Siehe Kapitel 3)
Eine Formel der Prädikatenlogik erster Stufe heißt in Pränexform, wenn sie die Gestalt Q₁x₁...Q_nx_n G hat, n≥0, wobei die Q_i Quantoren sind und in G kein Quantor vorkommt. (Siehe Kapitel 3)
Eine Klausel ist eine Disjunktion von Literalen.
Eine Formel der Prädikatenlogik erster Stufe heißt in konjunktiver Normalform, wenn sie in Pränexform ist und ihr quantorfreier Teil eine Konjunktion von Klauseln ist.
Eine Formel der Prädikatenlogik erster Stufe heißt in Klauselnormalform, wenn sie eine Konjunktion von Klauseln ist.
Eine Klausel in Implikationsnormalform hat die Gestalt (R⇒K), wobei R (für Rumpf) eine Konjunktion und K (für Kopf) eine Disjunktion von positiven Literalen, also von atomaren Formeln, ist.
Eine Formel der Prädikatenlogik erster Stufe heißt in Implikationsnormalform, wenn sie eine Konjunktion von Klauseln in Implikationsnormalform ist.

Die Formeln , , ¬, ¬ kommen auch in prädikatenlogischen Klauseln nicht vor.

Ein Beispiel für eine Klausel ist ∨*(¬p(x,y),¬q(x,y),r(x),s(x,z)), ihre Implikationsnormalform ist (∧*(p(x,y),q(x,y)) ⇒∨*(r(x),s(x,z))). Die Formel ∀x∃y∀z ∧*(∨*(p(a,x),p(x,a)),∨*(¬p(x,y),¬q(x,y),r(x),s(x,z))) ist in konjunktiver Normalform und obendrein geschlossen.

Eine Formel in Klauselnormalform oder in Implikationsnormalform ist nach Definition eine quantorfreie Darstellung einer Formel. Sie dient als abkürzende Schreibweise für die konjunktive Normalform einer universellen geschlossenen Formel.

Notation 4.4.11 (Allabschluss).

Sei F eine Formel. Der Allabschluss ∀(F) ist die geschlossene Formel

∀(F) := F falls F geschlossen ist

∀x₁...x_n F falls fvar(F)={x₁,...,x_n}
Sei S eine Menge von Formeln. Der Allabschluss ∀S ist die Menge ∀S:={∀(F) | F∈S}.

Für eine universelle geschlossene Formel in Pränexform enthält der Quantorpräfix nur Allquantoren, und zwar einen Allquantor für jede Variable in der Formel. Der Quantorpräfix kann aus dem quantorfreien Teil der Formel immer durch Bildung des Allabschlusses rekonstruiert werden. Die Klauselnormalform bzw. Implikationsnormalform nutzt das aus, indem sie die Quantoren implizit lässt.

Die Skolemisierung ermöglicht eine Umwandlung von nichtuniversellen Formeln in universelle, für die die semantischen Begriffe auf Herbrand-Interpretationen zurückgeführt werden können (Satz 3.8.23). Damit ergibt sich:

Folgesatz 4.4.14 (Normalformensatz für die Prädikatenlogik erster Stufe). Es bezeichne F eine geschlossene Formel und S eine endliche Menge von geschlossenen Formeln. Es gibt Algorithmen zur effektiven Berechnung:

Einer Formel F' in Klauselnormalform oder in Implikationsnormalform, so dass F erfüllbar ist genau dann wenn ∀(F') ein Herbrand-Modell hat.
Einer endlichen Menge S' von Klauseln oder von Klauseln in Implikationsnormalform, so dass S erfüllbar ist genau dann wenn ∀(S') ein Herbrand-Modell hat.

Die Herbrand-Modelle beziehen sich dabei auf das Herbrand-Universum einer Erweiterung der ursprünglichen Sprache um endlich viele Funktionssymbole.

∀(F) :=	F	falls F geschlossen ist
	∀x₁...x_n F	falls fvar(F)={x₁,...,x_n}