Seite parallel anzeigen





Du befindest dich hier: Aussagenlogik / Semantische Tableaux

Ein Tableaukalkül für Formeln in Negationsnormalform

(Aussagenlogik Kapitel 8.1)

Diese Seite nimmt Bezug auf

(Seite parallel anzeigen)
Liste überspringen
Zum Seitenanfang

Es gibt Tableaukalküle für aussagenlogische Formeln jeglicher Form - wir wollen hier eine vereinfachte Version für Formeln in Negationsnormalform vorstellen.

Betrachten wir eine Formel γ in Negationsnormalform. Für Modelle von γ gelten ganz einfache semantische Regeln:
  • Ist γ ein Atom, so ist jede Interpretation I für die I(γ) = 1 gilt ein Modell.
  • Ist γ eine Formel der Form !γ1, also eine Negation, so ist jede Interpretation I für die I(γ1) = 0 gilt ein Modell.
  • Ist γ eine Formel der Form γ1&γ2, also eine Konjunktion, so ist jede Interpretation I für die I(γ1) = I(γ2) = 1 gilt ein Modell.
  • Ist γ eine Formel der Form γ1|γ2, also eine Disjunktion, so ist jede Interpretation I für die I(γ1) = 1 oder I(γ2) = 1 gilt ein Modell.

Der Tableaukalkül bildet diese Regeln auf syntaktische Formationsregeln ab. Eine Formel γ wird derart in einen Baum umgewandelt, dass die Literale entlang der einzelnen Pfade die möglichen Modelle repräsentieren.

Wir wollen nun zunächst betrachten, wie wir ein Tableau erstellen, und uns dann die Bedeutung genauer ansehen.

Ein Tableau ist die Repräsentation einer Zerlegung einer Formel γ in Negationsnormalform als Baum:
  • Die Wurzel ist mit γ markiert.
  • Ist ein Knoten auf einem Pfad mit einer Aussage der Form γ1|γ2 markiert, so wird ein Kind des Endknotens des Pfades mit γ1, und das andere mit γ2 markiert. Wir bezeichnen diese Regel als "binäre Regel".
  • Ist ein Knoten auf einem Pfad mit einer Aussage der Form γ1&γ2 markiert, so wird der Nachfolgeknoten des Endknotens des Pfades mit γ1, und dessen Nachfolgeknoten mit γ2 markiert. Wir bezeichnen diese Regel als "unäre Regel".

Die Prozedur zur Erstellung eines Tableau terminiert immer, da es ausreicht, jede nichtatomare Formel auf jedem Pfad nur 1 Mal zu zerlegen. Diese Einschränkung wird durch die folgenden Anwendungsbedingungen realisiert:
  • Die binäre Regel wird nur angewandt, wenn es keinen Knoten auf dem Pfad gibt, der mit γ1 markiert ist und wenn es keinen Knoten auf dem Pfad gibt, der mit γ2 markiert ist.
  • Die unäre Regel wird nur angewandt, wenn es keinen Knoten auf dem Pfad gibt, der mit γ1 markiert ist oder wenn es keinen Knoten auf dem Pfad gibt, der mit γ2 markiert ist.
Um das aus der Prozedur entstehende Tableau weiter zu vereinfachen, wird die binäre Regel erst angewandt, wenn es nicht mehr möglich ist, die unäre Regel anzuwenden.

Beispiel - Erstellung eines Tableau

Wir wollen ein Tableau für die Formel
  • γ = p&q&!r|(!q|r)
erstellen.

Also markieren wir die Wurzel mit γ.
p&q&!r|(!q|r)
Der Hauptjunktor von γ ist die Disjunktion. Wir müssen also die binäre Regel anwenden, wobei
  • γ1 = p&q&!r
  • γ2 = !q|r
Wir markieren also das 1. Kind des Endknotens (hier die Wurzel) mit γ1 und das 2. Kind mit γ2 und erhalten das rechts abgebildete Resultat.
p&q&!r|(!q|r)
p&q&!r !q|r
Betrachten wir den linken Pfad und die Formel
  • γ' = p&q&!r
Der Hauptjunktor ist die Konjunktion. Wir müssen also die unäre Regel anwenden, wobei
  • γ1 = p&q
  • γ2 = !r
Wir markieren also den Nachfolgeknoten des Endknotens mit γ1 und dessen Nachfolgeknoten mit γ2 und erhalten das rechts abgebildete Resultat.
p&q&!r|(!q|r)
p&q&!r

p&q

!r 		!q|r
Betrachten wir weiterhin den linken Pfad: Wir haben breits γ und γ' zerlegt. Die nächste unzerlegte Formel ist also
  • γ'' = p&q
Der Hauptjunktor ist die Konjunktion. Wir müssen also die unäre Regel anwenden, wobei
  • γ1 = p
  • γ2 = q
Wir markieren also den Nachfolgeknoten des Endknotens mit γ1 und dessen Nachfolgeknoten mit γ2 und erhalten das rechts abgebildete Resultat.
p&q&!r|(!q|r)
p&q&!r

p&q

!r

p

q 		!q|r
Am linken Pfad gibt es nun keinen Knoten mehr, der zerlegbar wäre. Betrachten wir also den rechten Pfad: Der Hauptjunktor ist die Disjunktion. Wir müssen also die binäre Regel anwenden, wobei
  • γ1 = !q
  • γ2 = r
Wir markieren also das 1. Kind des Endknotens mit γ1 und das 2. Kind mit γ2 und erhalten das rechts abgebildete Resultat.
p&q&!r|(!q|r)
p&q&!r

p&q

!r

p

q
!q|r
!q  r
Da es keine weitere zerlegbare Formel gibt, sind wir fertig.
Befinden sich auf einem Pfad ein Atom und seine Negation, wird dieser geschlossen genannt, sonst ist der Pfad offen.
Sind alle Pfade eines Tableau geschlossen, wird dieses als geschlossen bezeichnet, andernfalls ist das Tableau offen.

Die offenen Pfade eines Tableau der Formel γ repräsentieren genau die Modelle von γ: man erhält die einzelnen Modelle, indem man pro offenem Pfad alle Literale als wahr annimmt.
Ist also ein Tableau der Formel γ
  • offen, so ist γ erfüllbar,
  • geschlossen, so ist γ unerfüllbar.

Beispiel - Ablesen der Modelle aus einem Tableau

Betrachten wir das Tableau aus dem vorherigen Beispiel:
p&q&!r|(!q|r)
p&q&!r

p&q

!r

p

q
!q|r
!q  r

Da offene Pfade existieren, ist γ erfüllbar.
Wir markieren alle Literale der offenen Pfade als wahr und erhalten die folgenden Modelle:
  • aus dem linken Ast ergibt sich das Modell I = {p→1, q→1, r→0}
  • aus dem mittleren Ast ergibt sich das Modell I = {q→0}
  • aus dem rechten Ast ergibt sich das Modell I = {r→1}
Die Gültigkeit einer Formel γ wird mittels des Tableaukalküls indirekt gezeigt: führt !γ zu einem Widerspruch, also zu einem geschlossenen Tableau, ist !γ unerfüllbar und somit γ gültig. Existiert mindestens ein offener Pfad, beschreibt dieser ein Gegenbeispiel für γ.

Beispiel - Prüfung der Gültigkeit einer Formel mit einem Tableau

Wir wollen die Gültigkeit der Formel
  • γ = ((p|q)&!p)->q
zeigen.

Um die Gültigkeit von γ mit einem Tableau zu zeigen, führen wir !γ zu einem Widerspruch.
Wir konstruieren also die Negationsnormalform von !γ und erhalten
  • γ' = NNF(!γ) = (p|q)&!p&!q
Nun konstruieren wir das Tableau von γ':

Zunächst markieren wir die Wurzel mit γ'.
(p|q)&!p&!q
Der Hauptjunktor von γ' ist die Konjunktion. Wir müssen also die unäre Regel anwenden, wobei
  • γ1 = (p|q)&!p
  • γ2 = !q
Wir markieren also den Nachfolgeknoten des Endknotens (hier die Wurzel) mit γ1 und dessen Nachfolgeknoten mit γ2 und erhalten das rechts abgebildete Resultat.
(p|q)&!p&!q

(p|q)&!p

!q
Betrachten wir den Pfad, so sehen wir, dass wir die Formel
  • γ'' = (p|q)&!p
zerlegen können.
Der Hauptjunktor ist die Konjunktion. Wir müssen also die unäre Regel anwenden, wobei
  • γ1 = p|q
  • γ2 = !p
Wir markieren also den Nachfolgeknoten des Endknotens mit γ1 und dessen Nachfolgeknoten mit γ2 und erhalten das rechts abgebildete Resultat.
(p|q)&!p&!q

(p|q)&!p

!q

p|q

!p
Betrachten wir den Pfad, so sehen wir, dass wir die Formel
  • γ''' = p|q
zerlegen können.
Der Hauptjunktor ist die Disjunktion. Wir müssen also die binäre Regel anwenden, wobei
  • γ1 = p
  • γ2 = q
Wir markieren also das 1. Kind des Endknotens mit γ1 und das 2. Kind mit γ2 und erhalten das rechts abgebildete Resultat.
(p|q)&!p&!q

(p|q)&!p

!q

p|q

!p
p q
Da es keine weitere zerlegbare Formel gibt, haben wir das Tableau erstellt.

Das Tableau hat 2 Pfade, die beide geschlossen sind:
  • der linke Pfad enthält die Literale p und !p
    (p|q)&!p&!q

    (p|q)&!p

    !q

    p|q

    !p
    p q
  • der rechte Pfad enthält die Literale q und !q
    (p|q)&!p&!q

    (p|q)&!p

    !q

    p|q

    !p
    p q
D.h. !γ ist unerfüllbar und somit ist γ gültig.
Abschließend ist zu bemerken, dass bei der Zerlegung einer Formel selbstverständlich nur offene Äste betrachtet werden müssen: ein geschlossener Ast repräsentiert ja bereits einen Widerspruch und eine weitere Zerlegung würde kein neues Ergebnis bringen.