Tableaukalkuel fuer Aussagenlogik fileDeduktion, SS 08, Folien Ded−Aussagen, Seite 14 23....
Transcript of Tableaukalkuel fuer Aussagenlogik fileDeduktion, SS 08, Folien Ded−Aussagen, Seite 14 23....
Tableaukalkuel fuer Aussagenlogik
Tableau:
• Test einer Formel auf Widerspruchlichkeit• Fallunterscheidung baumformig organisiert• Keine Normalisierung, d.h. alle Formeln sind erlaubt• Struktur der Formel wird beachtet• Verallgemeinerbar fur Modallogik, Pradikatenlogik
Deduktion, SS 08, Folien Ded−Aussagen, Seite 1 23. April2008
Tableaukalkul: Grundbegriffe
• α-Formeln (konjunktive Formeln)• β-Formeln (disjunktive Formeln)
Zerlegungen:
α α1 α2X ∧ Y X Y¬(X ∨ Y ) ¬X ¬Y¬(X ⇒ Y ) X ¬Y(X ⇔ Y ) X ⇒ Y Y ⇒ X
β β1 β2X ∨ Y X Y¬(X ∧ Y ) ¬X ¬YX ⇒ Y ¬X Y¬(X ⇔ Y ) ¬(X ⇒ Y ) ¬(Y ⇒ X)
Deduktion, SS 08, Folien Ded−Aussagen, Seite 2 23. April2008
Tableau: Definition
Idee beim Tableau-Kalkul:Zeige, dass die eingegebene Aussage inkonsistent ist.
Definition
Ein aussagenlogisches Tableau ist ein markierter Baumdie Knoten sind mit Formeln markiert.Die Eingabeformel ist an der Wurzel
Ein Pfad ist geschlossen, wenn 0 oder ¬1 vorkommt,oder gleichzeitig F und ¬F auf dem Pfad
Ein Pfad ist (atomar) geschlossen, wenn 0 oder ¬1 vorkommt,oder Atom A und ¬A auf diesem Pfad ist
Ein Tableau ist (atomar) geschlossen, wenn alle Pfade (atomar) ge-schlossen
Deduktion, SS 08, Folien Ded−Aussagen, Seite 3 23. April2008
Tableau-Aufbau-Regeln
• Eingabe ist eine Formel F• Initial: nur Knoten F• Danach Expansionsregeln:
¬¬X
X
α
α1α2
β
β1 | β2
¬0
1
¬1
0
Beachte: Die expandierte Formel muss kein Blatt sein.Einschrankung: Formel pro Pfad nur einmal expandieren
Ein Formel F ist bewiesen, wenn aus dem Tableau mit einem Knoten
und der Formel ¬F ein geschlossenes Tableau erzeugt worden ist.
Deduktion, SS 08, Folien Ded−Aussagen, Seite 4 23. April2008
Strategien
Aufbau-Regeln sind nicht-deterministisch
D.h. Reihenfolge ist nicht vorgeschrieben.
Effiziente Strategie: moglichst wenig verzweigend.h. bevorzuge α-Regeln
Deduktion, SS 08, Folien Ded−Aussagen, Seite 5 23. April2008
Beispiel
Tableau fur X ∧ ¬X:
X ∧ ¬X|X|
¬X
geschlossen
Deduktion, SS 08, Folien Ded−Aussagen, Seite 6 23. April2008
Beispiel
Tableau fur ¬(X ∧ Y ⇒ X):
¬(X ∧ Y ⇒ X)|
X ∧ Y|
¬X|X|Y
geschlossen
Deduktion, SS 08, Folien Ded−Aussagen, Seite 7 23. April2008
Optimierung fur Aquivalenzen
Neue Tableau-Expansionsregeln
A ⇔ B
A ¬AB ¬B
¬(A ⇔ B)
A ¬A¬B B
Nur eine Fallunterscheidung statt zwei !!
Deduktion, SS 08, Folien Ded−Aussagen, Seite 8 23. April2008
Beispiel: Aquivalenzen
¬((P ⇔ Q) ⇔ (Q ⇔ P ))
ggggggggggggggggggggg
WWWWWWWWWWWWWWWWWWWW
(P ⇔ Q) ¬(P ⇔ Q)
¬(Q ⇔ P )
ooooooooooooooQ ⇔ P
gggggggggggggggggggggggggggggg
P ¬P ¬Q Q
Q
xxxxxxxxx¬Q P ¬P
¬Q Q . . . . . . . . .
P ¬P
Deduktion, SS 08, Folien Ded−Aussagen, Seite 9 23. April2008
Beispiel
Zeige, dass P ⇒ (Q ⇒ P ) eine Tautologie ist:
¬(P ⇒ (Q ⇒ P ))
P
¬(Q ⇒ P )
Q
¬P
geschlossen, da P und ¬P auf dem Pfad liegen.
Deduktion, SS 08, Folien Ded−Aussagen, Seite 10 23. April2008
Beispiel
Zeige ((P ⇒ Q) ∧ (Q ⇒ R)) ⇒ (P ⇒ R):
Dazu starte mit ¬(((P ⇒ Q) ∧ (Q ⇒ R)) ⇒ (P ⇒ R)):
Deduktion, SS 08, Folien Ded−Aussagen, Seite 11 23. April2008
(P ⇒ Q)
(Q ⇒ R)
¬(P ⇒ R)
P
¬R
iiiiiiiiiiiiiiiiiiiiiiii
PPPPPPPPPPPPPPP
¬P Q
oooooooooooooooo
OOOOOOOOOOOOOOOOO
geschlossen ¬Q R
geschlossen geschlossen
Algorithmische Korrektheit des Tableaukalkuls
Nachweis von:
1. Korrektheit (Soundness): Der Kalkul erzeugt geschlossene Table-
aus nur fur unerfullbare Formeln.
2. Vollstandigkeit (Completeness): Fur jede unerfullbare Formel kann
der Tableaukalkul ein geschlossenes Tableau erzeugen.
Zusatzliche gute Eigenschaften:
• Tableaukalkul fur Aussagenlogik terminiert immer• Liefert Information, auch wenn er fehlschlagt.
Deduktion, SS 08, Folien Ded−Aussagen, Seite 13 23. April2008
Korrektheit des Tableaukalkuls (2)
Definition
• Ein Pfad eines Tableaus ist erfullbar, wenn die Kon-
junktion aller Formeln auf dem Pfad erfullbar ist.• Ein Tableau ist erfullbar, wenn es einen Pfad gibt,
der erfullbar ist.
Beachte: Wenn eine Menge von Formeln 0 oder ¬1 enthalt, dann ist
sie nicht erfullbar.
Es gilt: Ein geschlossenes Tableau ist nicht erfullbar.
Deduktion, SS 08, Folien Ded−Aussagen, Seite 14 23. April2008
Korrektheit des Tableaukalkuls (3)
Satz Wenn T → T ′ mit einer Transformationsregel, dann gilt:
T ist erfullbar gdw. T ′ ist erfullbar
Mittels Fallunterscheidung uber mogliche Expansionen:
Deduktion, SS 08, Folien Ded−Aussagen, Seite 15 23. April2008
Fundierte Ordnungen
Ziel: Terminierung
fundierte (well-founded) Ordnung:
ist eine partielle Ordnung ≥ auf einer Menge M ,
ohne unendlich absteigende Ketten a1 > a2 > . . .
zB. Naturliche Zahlen: 5 > 4 > 2 > 1.
Es gilt: Die lexikographische Kombination von fundierten Ordnungen
ist wieder eine fundierte Ordnung.
Deduktion, SS 08, Folien Ded−Aussagen, Seite 16 23. April2008
Fundierte Ordnungen: Multimengenordnung
(M, >) Menge mit fundierter Ordnung
Mult(M) endliche Multimengen uber M
Z.B. Multimengen uber IN:
{3,3,2,1}, ∅, {1,1,1,1,1,100}
Deduktion, SS 08, Folien Ded−Aussagen, Seite 17 23. April2008
Fundierte Ordnungen: Multimengenordnung
Seien A und B Multimengen uber M
A >> B, gdw ∃X, Y mit X 6= ∅, B = (A \X) ∪ Y undzu jedem Element von Y existiertein echt großeres Element in X
Z. B in Mult(IN):
{3,3,2,1} >> {3,2,2,2},denn {3,2,2,2} = {3,3,2,1} \ {3,1} ∪ {2,2,2}.
Es gilt: Die Multimengenordnung >> ist eine partielle Ordnung.>> ist fundiert, gdw. > fundiert ist.
Deduktion, SS 08, Folien Ded−Aussagen, Seite 18 23. April2008
Terminierung des Tableaukalkuls
Lemma Der Tableaukalkul fur Aussagenlogik terminiert, wenn man jede
Formel auf jedem Pfad hochstens einmal expandiert.
Beweis:
Benutze Multimengenordnung . . .
Deduktion, SS 08, Folien Ded−Aussagen, Seite 19 23. April2008
Korrektheit des Tableaukalkuls
Zusammen ergibt sich bis jetzt:
• Wenn F erfullbar:Der Tableaukalkul terminiert,Das Endtableau ist nicht geschlossen
• Wenn F unerfullbar:Der Tableaukalkul terminiert,Das Endtableau ist nicht erfullbarFrage? ist es auch geschlossen?
Deduktion, SS 08, Folien Ded−Aussagen, Seite 20 23. April2008
Korrektheit des Tableaukalkuls
Betrachte: Endtableau, das nicht geschlossen istDarin einen nicht geschlossenen Pfad.
Es gilt: Die Formelmenge H auf dem Pfad ist abgeschlossen und hat
folgende Eigenschaften:
• A ∈ H und ¬A ∈ H geht nicht.• 0 6∈ H,¬1 6∈ H• ¬¬X ∈ H ⇒ X ∈ H• α ∈ H ⇒ α1 ∈ H und α2 ∈ H• β ∈ H impliziert β1 ∈ H oder β2 ∈ H
D.h.: H ist eine (aussagenlogische) Hintikka-Menge
Es gilt: Hintikka-Mengen sind erfullbar
Deduktion, SS 08, Folien Ded−Aussagen, Seite 21 23. April2008
Korrektheit des Tableaukalkuls
Zusammenfassend ergibt sich jetzt:
• Wenn F erfullbar:Der Tableaukalkul terminiert,Das Endtableau ist nicht geschlossen
• Wenn F unerfullbar:Der Tableaukalkul terminiert,Das Endtableau ist geschlossen
D.h. der Tableaukalkul fur Aussagenlogik terminiert und ist korrekt.
Deduktion, SS 08, Folien Ded−Aussagen, Seite 22 23. April2008
Quantifizierte Boolesche Formeln
Quantifizierte Boolesche Formeln (QBF) sind
Boolesche Formeln mit Quantoren.
Syntax:
Q := 0 | 1| P ( Boolesche Variable)| (Q1 ∧Q2) | (Q1 ∨Q2) | (Q1 op Q2)| (¬ Q)| ∀X.Q | ∃X.Q wobei X Variable
Die Quantifizierung ist nur uber die zwei Wahrheitswerte 0,1
Die Gultigkeit ist nur fur geschlossene QBFs definiert.
Deduktion, SS 08, Folien Ded−Aussagen, Seite 23 23. April2008
QBF: Komplexitat
Gultigkeit von QBF ist PSPACE-vollstandig.
D.h. alle bekannten Algorithmen sind EXPTIME.
Ziel: Untersuchung und Optimierung der Entscheidungsalgorithmen
Hoffnung: großer Anteil praktisch relevanten Probleme effizient ent-
scheidbar
Deduktion, SS 08, Folien Ded−Aussagen, Seite 24 23. April2008
Aussagenlogik in QBFs:
• Erfullbarkeit einer aussagenlogischen Formel F= Gultigkeit der QBF ∃p1, . . . , pn.F ,wobei pi die Variablen in F sind.
• aussagenlogischen Formel F ist Tautologie= Gultigkeit der QBF ∀p1, . . . , pn.F ,wobei pi die Variablen in F sind.
Deduktion, SS 08, Folien Ded−Aussagen, Seite 25 23. April2008
Normalformen fur QBFs:
• Pranex-FormAlle Quantoren im Prafix der Formelder Rumpf ist eine aussagenlogischen Formel.
Deduktion, SS 08, Folien Ded−Aussagen, Seite 26 23. April2008
Pranexform einer QBF erzeugen
• Alle gebundenen Variablen mussen verschieden sein.Wenn nicht: neue Namen verwenden
1. Implikation und Aquivalenz ersetzen.2. Negationen nach innen schieben, u.a. mit
¬(∀X.P ) → (∃X.¬P ) und ¬(∃X.P ) → (∀X.¬P )3. Quantoren nach außen schieben, wobei
F ∨ ∀X.P → ∀X.F ∨ Pusw. auch fur die anderen Kombinationen
Deduktion, SS 08, Folien Ded−Aussagen, Seite 27 23. April2008
Normalformen fur QBFs:
• Pranexe Klauselform
Quantorenprafix und KlauselmengeTransformation ist effizient durchfuhrbar:P.F [G] → P.∃X.((X ⇔ G) ∧ F [X])
Alternativ:P.F [G] → P.∀X.((X ⇔ G) ⇒ F [X])
Deduktion, SS 08, Folien Ded−Aussagen, Seite 28 23. April2008
Nochmal: CNF-Herstellung in der Aussagenlogik
Zur Frage: Warum wird Aquivalenz von schneller CNF-Herstellung
nicht erhalten:
• Erhaltung der Erfullbarkeit: ok, da man in der ersten Variante nur
eine existenzquantifizierte Variable hinzufugt.
• Erhaltung der Tautologie-Eigenschaft:
wenn man die zweite Transformation verwendet.
• Aquivalenz der aussagenlogischen Formeln vorher und nacher gilt
i.a. nicht
Deduktion, SS 08, Folien Ded−Aussagen, Seite 29 23. April2008
Gultigkeit von QBF-Formeln
Naiver Algorithmus und gleichzeitig Def der Gultigkeit von F
Transformiere F durch Quantorenelimination:
1. ∀P.F → F [1/P ] ∧ F [0/P ]
2. ∃P.F → F [1/P ] ∨ F [0/P ]
Resultat nach Simplifikation: 0 oder 1
Nachteil: Zwischenergebnisse konnen exponentiell groß sein
Deduktion, SS 08, Folien Ded−Aussagen, Seite 30 23. April2008
Beispiel
F = ∀x∃y.x ⇔ y.
Quantorenelimination ergibt:
1. (∃y.1 ⇔ y) ∧ (∃y.0 ⇔ y).
2. ((1 ⇔ 1) ∨ (1 ⇔ 0)) ∧ ((0 ⇔ 1) ∨ (0 ⇔ 0))
3. Resultat: 1
Deduktion, SS 08, Folien Ded−Aussagen, Seite 31 23. April2008
Andere Ubersetzungsvariante
• ∀X.Q → ((X ⇔ 1) ⇒ Y ) ∧ ((X ⇔ 0) ⇒ Y ) ∧ (Y ⇔ (Q ∧ Q))
• ∃X.Q → (((X ⇔ 1) ∧ Y ) ∨ ((X ⇔ 0) ∧ Y )) ∧ (Y ⇔ Q)
Q ist die Formel Q[¬X/X].
Eigenschaften:
Die Ubersetzung ist erfullbarkeitserhaltend.
D.h. man muss auf Widerspruch testen!Komplexitat: linear in # ∃-quantoren,
exponentiell in # ∀-Quantoren
Deduktion, SS 08, Folien Ded−Aussagen, Seite 32 23. April2008
Klassifizierung von Klauseln
Gegeben: QBF in pranexer Klauselform.
Klassifikation von Klauseln:
1. Eine Klausel ist wahr, wenn sie ein Literal 1 enthalt, oder eine
Variable sowohl positiv als auch negativ (Tautologie).
2. Eine Klausel ist falsch, wenn 1. nicht gilt und wenn die Klausel
keine existenziell quantifizierte Variable enthalt.
Z.B. eine Klausel mit nur allquantifizierten Variablen ist falsch,
wenn sie keine Tautologie ist.
3. Andere Klauseln nennt man offen.
Deduktion, SS 08, Folien Ded−Aussagen, Seite 33 23. April2008
Ein Beispiel
∃x1∀x2∃x3∃x4.((¬x1 ∨ x2 ∨ ¬x3)︸ ︷︷ ︸c1
∧ (x3 ∨ ¬x4)︸ ︷︷ ︸c2
∧ (x3 ∨ x4)︸ ︷︷ ︸c3
∧ (x1 ∨ ¬x2 ∨ ¬x3)︸ ︷︷ ︸c4
)
Diese Formel ist nicht gultig:
·x1
zzzz
zzzz
zzzz
zzz
¬x1
AAAA
AAAA
AAAA
A
·¬x2
}}}}
}}}}
}}}}
}
}}}}
}}}}
}}}}
}
x2
·x2
¬x2
AAAA
AAAA
AAAA
A
AAAA
AAAA
AAAA
A
·x3
~~~~
~~~~
~~~~
~
¬x3
· ·x3
~~~~
~~~~
~~~~
~
¬x3
·
c1 ·
x4��
����
����
���
¬x4
????
????
????
? c4 ·
x4��
����
����
���
¬x4
????
????
????
?
c2 c3 c2 c3
Beachte: Doppelkanten = UND-Verzweigung; Einfachkante = Oder
Deduktion, SS 08, Folien Ded−Aussagen, Seite 34 23. April2008
Entscheidungsprozedur semantischer Baum
Eingabe: Pranexe KlauselformDatenstruktur: UND-ODER-Baum,
ALL ↔ UNDEX ↔ ODERKnoten sind Formeln
Deduktion, SS 08, Folien Ded−Aussagen, Seite 35 23. April2008
Semantischer Baum: Erzeugung
• Wurzel = Input-Formel in pranexer Klauselform• Am Knoten K erste Variable des Quantorenprafix von FK analysieren:
1. ∀x, dann UND-Knoten.Die beiden Tochterknoten sind:FK[1/x] und FK[0/x]
2. ∃x, dann ODER-Knoten.Die beiden Tochterknoten sind:FK[1/x] und FK[0/x]
• Knoten ist Blatt, wenn FK aussagenlogisch zu 1 oder 0 auswertbarunter Benutzung der Def. wahre / falsche Klauseln
• Auswertung des Ausgabe-Baums:Auswertung entsprechend der UND, bzw ODER-Strukturund Werten an den Blattern.
• Ergebnis: 0 oder 1.
Optimierungsmoglichkeit: Vertauschen von gleichartig quantifizierten
benachbarten Variablen
Deduktion, SS 08, Folien Ded−Aussagen, Seite 36 23. April2008
Quellen des Nichtdeterminismus
• Welche Variable wird zur Fallunterscheidung verwendet?
• Welcher Fall wird zuerst untersucht pro Variable?
Deduktion, SS 08, Folien Ded−Aussagen, Seite 37 23. April2008
Beispiel
∀x, ∃y.x ⇔ y:
∀x∃y.x ⇔ y
ffffffffffffffffffffffff
ffffffffffffffffffffffff
SSSSSSSSSSSSSS
SSSSSSSSSSSSSS
∃y.1 ⇔ y
mmmmmmmmmmmm
QQQQQQQQQQQQ∃y.0 ⇔ y
jjjjjjjjjjjjjjj
QQQQQQQQQQQQ
1 ⇔ 0 1 ⇔ 1 0 ⇔ 1 0 ⇔ 0
Der Wert an der Wurzel ist 1.
> dpll "ALL x EX y: (x <=> y)"
"Formel ist Tautologie"
Deduktion, SS 08, Folien Ded−Aussagen, Seite 38 23. April2008
Optimierungen:
Vermeiden von Fallunterscheidungen:
• Wenn aktuelle Variable nicht in der Klauselmenge enthalten ist,
dann streiche diese aus dem Prafix.
Deduktion, SS 08, Folien Ded−Aussagen, Seite 39 23. April2008
Optimierungen: Unit-Propagation
Situation: Formel am Knoten
Eine Klausel c ist eine Unit, gdw.
c hat genau ein existenzielles Literal (x oder ¬x) und
fur alle anderen (universellen) Literale y oder ¬y,
y ist rechts von x im Quantorenprafix
Aktion :
Nur ein Tochterknoten:
F [1/x], wenn x das Literal ist und
F [0/x], wenn ¬x das Literal ist.
Beachte: x muss nicht die Top-Variable sein
Deduktion, SS 08, Folien Ded−Aussagen, Seite 40 23. April2008
Optimierungen: Isoliertes Literal
Definition Ein Literal in einer Klauselmenge ist isoliert (pur),
wenn das Komplement nicht in der Klauselmenge vorkommt.
Aktion:
Sei x die Variable im isolierten Literal.
1. Wenn x Ex-quantifiziert ist,
Tochterknoten: F [1/x], wenn x das Literal ist und
Tochterknoten: F [0/x], wenn ¬x das Literal ist.
2. Wenn x All-quantifiziert ist,
Tochterknoten mit F [0/x], wenn x das Literal ist und
F [1/x], wenn ¬x das Literal ist.
Deduktion, SS 08, Folien Ded−Aussagen, Seite 41 23. April2008