Transcript
Aussagenlogik � Syntax und Semantik � Erfu ¨llbarkeit � SAT-Solver � Kompaktheit � Beweiskalku ¨le
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.1 Aussagenlogik – Syntax und Semantik
Einfu ¨hrendes Beispiel
Norbert sagt “Marcel sagt die Wahrheit”. Marcel sagt “Bahareh lu ¨gt”. Bahareh sagt “Norbert und Marcel sagen entweder beide die Wahrheit oder lu ¨gen beide”. Wer lu ¨gt, und wer sagt die Wahrheit?
23
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.1 Aussagenlogik – Syntax und Semantik
Syntax der Aussagenlogik Wir setzen eine Menge V = {A, B, C , . . .} von Aussagenvariablen voraus. Formeln der Aussagenlogik (u ¨ber V) sind induktiv definiert durch: • Jeder Aussagenvariable A ist eine Formel. • Die Konstanten tt und ff sind Formeln. • Sind ϕ und ψ Formeln, so sind auch • (ϕ ∧ ψ) • (ϕ ∨ ψ) • ¬ϕ • (ϕ → ψ) • (ϕ ↔ ψ)
Formeln.
(“und”) (“oder”) (“nicht”) (“wenn-dann”) (“genau-dann-wenn”)
24
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.1 Aussagenlogik – Syntax und Semantik
Pr¨ azedenzregeln zur besseren Lesbarkeit lassen wir auch Klammern weg (z.B. ganz außen) Bindungskraft der Operatoren (auch Junktoren genannt) in absteigender Reihenfolge: ¬, ∧, ∨, →, ↔ soll heissen: ((A ∨ ¬(B ∧ ¬C )) ↔ (C → A)) schreiben wir auch als A ∨ ¬(B ∧ ¬C ) ↔ C → A
25
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.1 Aussagenlogik – Syntax und Semantik
Interpretationen Def.: Sei B = {0, 1} Menge der Booleschen Werte falsch und wahr. Def.: Eine Interpretation (Variablenbelegung) ist eine Abbildung I : V → B. Interpretationen k¨onnen Modelle einer Formel sein; diese Beziehung ist induktiv definiert: I |= tt, I �|= ff und I |= A
gdw.
I |= ϕ ∨ ψ
gdw.
I |= ϕ → ψ
gdw.
I |= ϕ ∧ ψ
gdw.
I |= ¬ϕ
gdw.
I |= ϕ ↔ ψ
gdw.
I(A) = 1
I |= ϕ und I |= ψ
I |= ϕ oder I |= ψ I �|= ϕ
wenn I |= ϕ dann I |= ψ
I |= ϕ genau dann, wenn I |= ψ
Beachte Unterscheidung zwischen Formeln ff, tt (Syntax) und zugeordneten Werten 0, 1 (Semantik)
26
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.1 Aussagenlogik – Syntax und Semantik
Beispiele Bsp.: I = {A �→ 1, B �→ 0, C �→ 1, D �→ 0} Ist I jeweils Modell der folgenden Formeln? • (A ∨ B) ∧ (C ∨ D) • (¬A ∨ B) ∨ (¬C ∧ D) • A → ¬B • ¬A → B • A→B • ¬A → ¬B • (A ↔ B) ↔ ¬(C ↔ ¬D) • ¬(¬D → ff)
27
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.1 Aussagenlogik – Syntax und Semantik
Beispiel Logik u ¨ber anonymen Aussagenvariablen fu ¨r Theorie der Wahrheit beliebiger Aussagen Formeln lassen sich natu ¨rlich mit konkreten Aussagen instanziieren Bsp. (weitergef.): • Norbert sagt “Marcel sagt die Wahrheit”. • Marcel sagt “Bahareh lu ¨gt”. • Bahareh sagt “Norbert und Marcel sagen entweder beide die Wahrheit oder lu ¨gen beide”. Lo¨sung erfordert Formalisierung; drei Variablen B, M, N mit intendierter Bedeutung: Bahareh sagt die Wahrheit (B), . . . obiger Sachverhalt wird beschrieben durch welche Formel(n)? (N ↔ M) ∧ (M ↔ ¬B) ∧ (B ↔ (M ↔ N)) jedes Modell dieser Formel beschreibt L¨osung des R¨atsels
28
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.1 Aussagenlogik – Syntax und Semantik
Formeln und Boolesche Funktionen
eine Formel ϕ mit n vorkommenden Aussagenvariablen A1 , . . . , An stellt eine Funktion vom Typ Bn → B dar es gibt nur 2n viele Interpretationen, die sich in A1 , . . . , An unterscheiden; also gibt es nur 2n viele verschiedene “Eingaben” an ϕ Funktionswert 1 besagt, dass die durch Argumente gegebene Interpretation ein Modell ist Funktionen mit endlichem Domain k¨onnen durch Tabellierung aller Argumente repr¨asentiert werden
29
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.1 Aussagenlogik – Syntax und Semantik
30
Wahrheitstafeln . . . fu ¨r die Junktoren und Konstanten der Aussagenlogik ϕ 0 0 1 1 ϕ 0 0 1 1
ψ 0 1 0 1
ψ 0 1 0 1
ϕ∧ψ 0 0 0 1 ϕ→ψ 1 1 0 1
ϕ 0 0 1 1 ϕ 0 0 1 1
ψ 0 1 0 1 ψ 0 1 0 1
ϕ∨ψ 0 1 1 1 ϕ↔ψ 1 0 0 1
ϕ 0 1
tt 1
¬ϕ 1 0
ff 0
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.1 Aussagenlogik – Syntax und Semantik
Wahrheitstafeln
. . . fu ¨r komplexere Formeln
A 0 0 0 0 1 1 1 1
B 0 0 1 1 0 0 1 1
C 0 1 0 1 0 1 0 1
A∧B 0 0 0 0 0 0 1 1
A ∧ B → ff 1 1 1 1 1 1 0 0
¬B 1 1 0 0 1 1 0 0
¬B → C 0 1 1 1 0 1 1 1
(A ∧ B → ff) ∧ (¬B → C ) 0 1 1 1 0 1 0 0
31
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.1 Aussagenlogik – Syntax und Semantik
Beispiel (weiterg.) • Norbert sagt “Marcel sagt die Wahrheit”. • Marcel sagt “Bahareh lu¨gt”. • Bahareh sagt “Norbert und Marcel sagen entweder beide die Wahrheit oder lu ¨gen beide”.
formalisiert als (N ↔ M) ∧ (M ↔ ¬B) ∧ (B ↔ (M ↔ N)) M 0 0 0 0 1 1 1 1
N 0 0 1 1 0 0 1 1
B 0 1 0 1 0 1 0 1
ϕ 0 1 0 0 0 0 0 0
einzige mo¨gliche Lo¨sung: Norbert und Marcel lu ¨gen, Bahareh sagt die Wahrheit
32
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.1 Aussagenlogik – Syntax und Semantik
¨ Aquivalenzen Def.: ϕ und ψ heissen ¨aquivalent, geschrieben ϕ ≡ ψ, gdw. fu ¨r alle Interpretationen I gilt: I |= ϕ gdw. I |= ψ ¨ Aquivalenzen k¨onnen z.B. ausgenutzt werden, um kleinere Formeln, die dasselbe ausdru ¨cken, zu erhalten Bsp.: B ↔ (A → ¬B) ≡ A ↔ ¬B Beweis z.B. durch Wahrheitstafeln A 0 0 1 1
B 0 1 0 1
B ↔ (A → ¬B) 0 1 1 0
A ↔ ¬B 0 1 1 0
33
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.1 Aussagenlogik – Syntax und Semantik
34
“Wenige” Formeln Warum ist die folgende Aussagen falsch? “Es gibt 17 paarweise nicht-¨aquivalente Formel ϕ1 , . . . , ϕ17 , die nur die Variablen A und B verwenden.” n
Thm.: Fu ¨r jedes n ∈ N gibt es genau 22 viele verschiedene, paarweise nicht-¨aquivalente Formeln der Aussagenlogik. Beweis: ϕ ≡ ψ genau dann, wenn ihre Wahrheitstafeln 2n viele verschiedene u bereinstimmen. Es gibt aber genau nur 2 ¨ Wahrheitstafeln mit n Argumenten.
�
¨ Ubung: Finde alle 16 paarweise nicht-¨aquivalenten Formeln u ¨ber 2 Variablen.
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.2 Aussagenlogik – Erfu ¨llbarkeit
Erfu ¨llbarkeit und Allgemeingu ¨ltigkeit Def.: eine Formel ϕ heißt erfu ¨llbar, wenn es ein I gibt, so dass I |= ϕ Def.: eine Formel ϕ heißt allgemeingu ¨ltig (oder Tautologie), wenn fu ¨r alle I gilt: I |= ϕ ¨ Ubung: erkl¨are Erfu ¨llbarkeit und Allgemeingu ¨ltigkeit anhand von Wahrheitstafeln Lemma: ϕ ist erfu ¨llbar gdw. ¬ϕ nicht allgemeingu ¨ltig ist Beweis: “⇒” Sei ϕ erfu ¨llbar. Dann ex. I mit I |= ϕ und daher I �|= ¬ϕ. Somit ist ¬ϕ nicht allgemeingu ¨ltig. “⇐” Genauso. beachte: ϕ unerfu ¨llbar gdw. ¬ϕ allgemeingu ¨ltig
35
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.2 Aussagenlogik – Erfu ¨llbarkeit
Beispiele die folgenden Formeln sind erfu ¨llbar A , ¬A , A ∧ ¬B , (A ∨ B) ∧ (¬A ∨ B) ∧ (A ∨ ¬B) die folgenden Formeln sind unerfu ¨llbar A ∧ ¬A , (A ∨ B) ∧ (¬A ∨ B) ∧ (A ∨ ¬B) ∧ (¬A ∨ ¬B) die folgenden Formeln sind Tautologien A ∨ ¬A , (A → B) → (B → C ) → (A → C ) , ¬¬A ↔ A beachte: → ist nicht assoziativ; Konvention: rechts geklammert
36
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.2 Aussagenlogik – Erfu ¨llbarkeit
Zusammenh¨ ange
Theorem 1 a) ϕ ∧ ψ ist allgemeingu ¨ltig gdw. ϕ und ψ allgemeingu ¨ltig sind
b) ϕ ∨ ψ ist erfu ¨llbar gdw. ϕ oder ψ erfu ¨llbar ist c) ϕ ≡ ψ gdw. ϕ ↔ ψ allgemeingu ¨ltig
d) ϕ allgemeingu ¨ltig gdw. ϕ ≡ tt e) ϕ unerfu ¨llbar gdw. ϕ ≡ ff
¨ Beweis: (Ubung)
37
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.2 Aussagenlogik – Erfu ¨llbarkeit
Fallstricke
Vorsicht! Folgendes gilt nicht: • ϕ ∨ ψ allgemeingu ¨ltig gdw. ϕ oder ψ allgemeingu ¨ltig • ϕ ∧ ψ erfu ¨llbar gdw. ϕ und ψ erfu ¨llbar
Gegenbeispiele? aber es gelten jeweils eine der beiden Richtungen, welche?
38
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.2 Aussagenlogik – Erfu ¨llbarkeit
Erfu ¨llbarkeit, Allgemeingu ¨ltigkeit und Negation
¨ Ubung: Was ist jeweils m¨oglich bzw. unm¨ oglich? a) ϕ und ¬ϕ beide erfu ¨llbar b) ϕ und ¬ϕ beide allgemeingu ¨ltig c) ϕ und ¬ϕ beide unerfu ¨llbar d) ϕ erfu ¨llbar und ¬ϕ unerfu ¨llbar e) das Gegenteil von (d)
39
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.2 Aussagenlogik – Erfu ¨llbarkeit
Anwendungen von Erfu ¨llbarkeit
Def.: Das Erfu ¨llbarkeitsproblem der Aussagenlogik (SAT) ist das folgende: Geg. ϕ, entscheide, ob ϕ erfu ¨llbar ist oder nicht. • L¨ osung des R¨atsels u ¨ber das Lu ¨gen ist Erfu ¨llbarkeitstest • Zusammenhang zu Allgemeingu ¨ltigkeit bedeutet: u ¨ber
Erfu ¨llbarkeit l¨asst sich herausfinden, welche aussagenlogischen Zusammenh¨ange gelten
• allgemein: Erfu osungen ¨llbarkeitstest ist Auffinden von L¨ • ...
40
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.2 Aussagenlogik – Erfu ¨llbarkeit
Bsp.: Sudoko via Aussagenlogik
k mit 1 ≤ i, j ≤ 9 und 0 ≤ k ≤ 3 fur binare verwende Variablen Xi,j ¨ ¨ Kodierung der L¨osung
intuitive Bedeutung “das k-te Bit der Zahl im Feld (i, j) ist gesetzt” betrachte Konjunktion u ¨ber die folgenden Aussagen • “an jeder Stelle steht eine Zahl zwischen 1 und 9”
• “in jeder Zeile / Spalte / Block kommt keine Zahl doppelt
vor”
• Vorbelegungen, z.B. “in Feld (2, 7) steht die 5”
41
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.2 Aussagenlogik – Erfu ¨llbarkeit
Ein naiver Erfu ¨llbarkeitstest
Theorem 2 SAT ist in Zeit O(|ϕ| · 2|Vars(ϕ)| ) entscheidbar. (|ϕ| = L¨ange von ϕ, Vars(ϕ) = Menge der Variablen in ϕ) Beweis: Beachte: • in Zeit O(|ϕ|) l¨ asst sich fu ¨r gegebenes I entscheiden, ob
¨ I |= ϕ gilt oder nicht (Ubung).
• es reicht aus, nur Interpretationen vom Typ
I : Vars(ϕ) → {0, 1} zu betrachten; davon gibt es nur 2|Vars(ϕ)| viele
Aufz¨ahlung aller relevanten Interpretationen und sukzessives Testen
42
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.2 Aussagenlogik – Erfu ¨llbarkeit
43
Normalformen Def.: • Ein Literal ist eine Variable A oder ihre Negation ¬A. • Eine Klausel ist eine Disjunktion von Literalen,
�n
• Ein Minterm ist eine Konjunktion von Literalen,
i=1 �i .
�n
i=1 �i .
• Eine Formel ist in konjunktiver Normalform (KNF), falls sie
eine Konjunktion von Klauseln ist,
�n
i=1
�m i
j=1 �i,j .
• Eine Formel ist in disjunktiver Normalform (DNF), falls sie
eine Disjunktion von Mintermen ist,
�n
i=1
Bsp. (A ∨ ¬B) ∧ (B ∨ ¬C ∨ ¬A) ist in KNF
�m i
j=1 �i,j .
wir schreiben Formeln in KNF (oder DNF) wegen Assoziativit¨at, Kommutativit¨at und Idempotenz auch als Mengen von Mengen von Literalen
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.2 Aussagenlogik – Erfu ¨llbarkeit
Substitutionen Def.: ϕ[ψ/A] bezeichne die simultane Ersetzung von jedem Vorkommen der Variablen A in ϕ durch ψ
Theorem 3 ¨ Aussagenlogische Aquivalenz ist eine Kongruenzrelation: Wenn ψ ≡ θ dann ϕ[ψ/A] ≡ ϕ[θ/A]. Beweis (durch Induktion u ¨ber den Aufbau von ϕ) Frage: macht es einen Unterschied, wenn man nicht simultan ersetzt?
44
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.2 Aussagenlogik – Erfu ¨llbarkeit
Existenz von Normalformen Theorem 4 Fu ¨r jedes ϕ existiert ein ψ in KNF / DNF, so dass ϕ ≡ ψ. Beweis: Durch schrittweises Umbauen von ϕ: 1
Elimination von →, ↔ mittels ϕ1 ↔ ϕ2 ≡ (ϕ1 → ϕ2 )∧(ϕ2 → ϕ1 )
2
3
,
ϕ1 → ϕ2 ≡ ¬ϕ1 ∨ϕ2
Anwenden der de Morgan-Gesetze und ¬¬θ ≡ θ liefert Formel, die nur aus Literalen mit ∧, ∨ gebaut ist.
Anwenden der Distributivgesetze liefert KNF oder DNF.
Alle Schritte sind ¨aquivalenzerhaltend laut Thm. 3.
45
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.2 Aussagenlogik – Erfu ¨llbarkeit
Das Erfu ¨llbarkeitsproblem fu ¨r DNF Theorem 5 DNF-SAT (SAT fu ¨r Formeln in DNF) l¨asst sich in Zeit O(|ϕ| log |ϕ|) entscheiden. Beweis: • Ein Minterm
�n
i=1 li
ist erfu ¨llbar gdw. es keine A, i, j gibt, so dass li = A und lj = ¬A fu ¨r 1 ≤ i, j ≤ n. � • Eine Disjunktion ni=1 ϕi ist erfu ¨llbar gdw. es ein i gibt, so dass ϕi erfu ¨llbar ist.
Somit kann Erfu ¨llbarkeit einer DNF in einem Durchlauf (nach Sortierung) durch die Formel entschieden werden.
Warum dann nicht Erfu ¨llbarkeitstest fu ¨r allgemeine Formel ϕ so: Wandle ϕ in ¨aquivalente DNF ψ um. Teste Erfu ¨llbarkeit von ψ.
46
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.2 Aussagenlogik – Erfu ¨llbarkeit
Erfu aquivalenz ¨llbarkeits¨ ¨ neben dem starken Aquivalenzbegriff ≡ fu ¨hren wir noch einen schw¨acheren ein Def.: ϕ und ψ sind erfu ¨llbarkeits¨aquivalent, ϕ ≡sat ψ, falls gilt: ϕ erfu ¨llbar gdw. ψ erfu ¨llbar ¨ beachte: ≡sat ist Aquivalenzrelation mit nur zwei ¨ Aquivalenzklassen; kanonische Vertreter sind tt, ff Wofu ¨r kann das dann u ¨berhaupt gut sein? Ist man (nur) an Erfu ¨llbarkeit von ϕ interessiert, so reicht es aus, Erfu ¨llbarkeit von ψ zu testen, falls ϕ ≡sat ψ (aber evtl. nicht ϕ ≡ ψ).
47
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.2 Aussagenlogik – Erfu ¨llbarkeit
Erfu aquivalente KNF ¨llbarkeits¨ Theorem 6 Fu ¨r jedes ϕ gibt es ein ψ in KNF, so dass ϕ ≡sat ψ und |ψ| = O(|ϕ|). Beweis: Fu ¨r jede nicht-atomare Subformel θ von ϕ fu ¨hren wir eine Variable Xθ ein. Dann wird ϕ sukzessive nach folgender Vorschrift “von unten nach oben” umgebaut. Solange es noch eine nicht-atomare Subformel θ gibt, ersetze diese durch Xθ und definiere eine KNF ψθ je nach Junktor in θ, z.B. Falls θ = Y ∧ Z , dann ψθ := (¬Xθ ∨ Y ) ∧ (¬Xθ ∨ Z ) ∧ (Xθ ∨ ¬Y ∨ ¬Z ) �
Definiere schlussendlich ψ := Xϕ ∧ {ψθ | θ Subformel von ϕ}
48
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.2 Aussagenlogik – Erfu ¨llbarkeit
Erfu aquivalente KNF ¨llbarkeits¨
Beachte: Es gilt in obiger Konstruktion nicht nur ϕ ≡sat ψ, sondern noch etwas st¨arkeres: • Vars(ϕ) ⊆ Vars(ψ)
• Ist I |= ψ, so auch I |= ϕ (aber nicht unbedingt umgekehrt).
Soll heißen: ψ ist nicht nur erfu ¨llbarkeits¨aquivalent zu ϕ, sondern jeder erfu ¨llende Variablenbelegung fu ¨r ψ ist auch eine fu ¨r ϕ. Beachte: Erfu ¨llbarkeitstest in O(n log n) war fu ¨r DNF, nicht KNF! Umwandlung in erfu ¨llbarkeits¨aquivalente DNF ist wohl nicht mit nur polynomiellem Aufwand m¨oglich.
49
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.2 Aussagenlogik – Erfu ¨llbarkeit
Beispiel Gesucht ist Formel ExactlyOne(V ) fu ¨r endliche Variablenmenge V , so dass I |= ExactlyOne(V )
gdw.
I(A) = 1 fu ¨r genau ein A ∈ V
Einfache L¨osung: ExactlyOne(V ) :=
�
A∈V
(A ∧
beachte: dies hat Gr¨oße O(n2 ) Geht es auch mit Formel der Gr¨oße O(n)?
�
B∈V B�=A
¬B)
50
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.2 Aussagenlogik – Erfu ¨llbarkeit
“Genau eins” mit linearem Aufwand
angenommen V = {A1 , . . . , An }. spendiere zus¨atzliche Variablen Bi , i = 1, . . . , n, die jeweils ausdru ¨cken sollen “eine der A1 , . . . , Ai ist wahr” ExactlyOne(V ) := ϕ1 ∧ ϕ2 , wobei ϕ1 :=
n �
Ai
i=1
ϕ2 := (A1 ↔ B1 ) ∧
n �
i=2
((¬Bi−1 ↔ Ai ) → Bi ) ∧ ¬(Bi−1 ∧ Ai )
51
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.2 Aussagenlogik – Erfu ¨llbarkeit
Horn-Formeln Def.: Eine Horn-Formel ist ein ϕ in KNF, so dass in jeder Klausel h¨ochstens ein positives Literal vorkommt. Beachte: ¬A1 ∨ . . . ∨ ¬An ∨ B ≡ A1 ∧ . . . ∧ An → B
¬A1 ∨ . . . ∨ ¬An ≡ A1 ∧ . . . ∧ An → ff
Theorem 7 HORN-SAT (Erfu ¨llbarkeitsproblem fu ¨r Horn-Formeln) ist in Zeit O(|ϕ|2 ) l¨osbar. ¨ Beweis: (Ubung) Beachte: mit etwas Cleverness l¨asst es sich sogar in O(|ϕ|) l¨ osen
52
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.3 Aussagenlogik – SAT-Solver
SAT-Solver Ein SAT-Solver ist eine Implementierung eines Algorithmus fu ¨r das SAT-Problem. Obwohl dies i.A. exponentielle (in |Vars(ϕ)|) Laufzeit braucht, gibt es mittlerweile einige SAT-Solver, die in der Praxis erstaunlich gut funktionieren. • Minisat
http://minisat.se/
• Picosat
http://fmv.jku.at/picosat/
• Berkmin
http://eigold.tripod.com/BerkMin.html
• RSat
• zChaff
http://reasoning.cs.ucla.edu/rsat/ http://www.princeton.edu/~chaff/zchaff.html
• ...
siehe auch SATLive-Webseite
http://www.satlive.org/
53
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.3 Aussagenlogik – SAT-Solver
Das DIMACS-Format SAT-Solver verlangen typischerweise eine Eingabe in KNF. Standardisiertes Format: DIMACS • Variablen sind natu ¨rliche Zahlen ≥ 1 • Literale werden durch Integer bezeichnet, z.B. A7 = 7, ¬A4 =
-4
• Klausel ist Liste von Integern, 0 markiert Klauselende • KNF ist Liste von Klauseln • Kommentare im Header (c ...) • spezielle Headerzeile (p cnf ...) gibt Anzahl verwendeter
Klauseln und Variablen an
54
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.3 Aussagenlogik – SAT-Solver
Beispiel Die KNF (¬A ∨ B ∨ C ) ∧ (B ∨ ¬C ) ∧ ¬D ∧ (A ∨ D) ∧ (¬B ∨ ¬C ∨ ¬D) kann im DIMACS-Format so repr¨asentiert werden: c Beispielformel aus der Vorlesung c Autor: Martin Lange p cnf 4 5 -1 2 3 0 2 -3 0 -4 0 1 4 0 -2 -3 -4 0
55
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.3 Aussagenlogik – SAT-Solver
SAT-Solver im Einsatz Clevere Heuristiken und jahrelanges Tuning haben dazu gefu ¨hrt, dass moderne SAT-Solver typischerweise Instanzen der Gr¨oßenordnung • ∼ 105 Variablen • ∼ 106 Klauseln
l¨osen k¨onnen.
Vorsicht! Es gibt natu ¨rlich auch (im Vergleich dazu) sehr kleine Instanzen, an denen sie sich die Z¨ahne ausbeissen. typischer Einsatz von SAT-Solvern (nicht ann¨ahernd vollst¨andig): • Hardware-Verifikation • Planungsprobleme in der KI • Constraint-Solving • ...
56
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.3 Aussagenlogik – SAT-Solver
Ersetzung von Literalen Def.: Sei C Klauselmenge (= Menge von Mengen von Literalen). Mit C[A �→ 1] bezeichnen wir die Menge von Klauseln, die dadurch entsteht, dass man 1 2
jede Klausel, die das Literal A enth¨alt, aus C entfernt, und das Literal ¬A aus jeder Klausel in C entfernt.
Fu ¨r C[A �→ 0] gilt das entsprechend duale. Bsp.:
C = {{A, ¬B}, {¬A, ¬B}, {¬A, B}}
C[A �→ 1] = {{¬B}, {B}}
C[B �→ 0] = {{¬A}}
Lemma: Sei C Klauselmenge (als KNF aufgefasst), A Variable. C erfu ¨llbar gdw. C[A �→ 1] oder C[A �→ 0] erfu ¨llbar. ¨ Beweis: (Ubung)
57
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.3 Aussagenlogik – SAT-Solver
Unit-Propagation Lemma: Sei C Klauselmenge, A Variable, so dass {A} ∈ C. Dann ist C erfu ¨llbar gdw. C[A �→ 1] erfu ¨llbar ist. Beweis: “⇐” folgt sofort aus Lemma davor. “⇒” Sei C erfu ¨llbar. Wegen Lemma davor mu ¨ssen wir lediglich zeigen, dass C[A �→ 0] unerfu ¨llbar ist. Dies ist der Fall, denn da {A} ∈ C gilt ∅ ∈ C[A �→ 0], und wegen KNF steht ∅ fu ¨r ff, und ff ∧ ϕ ≡ ff, was unerfu � ¨llbar ist. entsprechendes Lemma fu ¨r Fall {¬A} ∈ C � Algorithmus Unit-Propagation(C) fu ¨hrt sukzessive diese Ersetzungsschritte durch, solange noch Singleton-Klauseln in C vorhanden sind.
58
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.3 Aussagenlogik – SAT-Solver
Der DPLL-Algorithmus Alle modernen SAT-Solver basieren auf dem DPLL-Algorithmus (nach Davis, Putnam, Logemann, Loveland). DPLL(C) = Unit-Propagation(C) if C = ∅ then return erfu ¨llbar if ∅ ∈ C then return unerfu ¨llbar w¨ahle Variable A, die noch in C vorkommt if DPLL(C[A �→ 1]) = erfu ¨llbar then return erfu ¨llbar return DPLL(C[A �→ 0]) Bem.: Algorithmus DPLL terminiert immer, ist korrekt (wenn er “erfu ¨llbar” sagt, dann war die Eingabe auch erfu ¨llbar) und vollst¨andig (wenn die Eingabe erfu ¨llbar ist, dann sagt er auch “erfu ¨llbar”), aber wieso?
59
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.4 Aussagenlogik – Kompaktheit
60
Erfu ¨llbarkeit und endliche Konsistenz Def.: Eine Menge Φ von Formeln heißt erfu ¨llbar, wenn es eine Interpretation I gibt, so dass I |= ϕ fu ¨r alle ϕ ∈ Φ gilt. Notation: I |= Φ. �
Fu ¨r |Φ| < ∞ ist also Menge Φ erfu ¨llbar gdw. Formel Φ erfu ¨llbar ist. Def. beinhaltet aber auch Fall unendlicher Mengen! Bsp.: {Ai ↔ ¬Ai+1 | i ∈ N} ist erfu ¨llbar Im folgenden nehmen wir an, dass V nur abz¨ahlbar unendlich viele Variablen enth¨alt, also o.B.d.A. V = {A0 , A1 , . . .}. Def.: Eine Menge Φ von Formeln heißt endlich konsistent, wenn fu ¨r alle Ψ ⊆ Φ mit |Ψ| < ∞ gilt: Ψ ist erfu ¨llbar.
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.4 Aussagenlogik – Kompaktheit
Der Kompaktheitssatz Theorem 8 Fu ¨r alle Mengen Φ von Formeln gilt: Φ erfu ¨llbar gdw. Φ endlich konsistent. Anders gesagt: Ist jede endliche Teilmenge einer Menge Φ erfu ¨llbar, so ist auch Φ erfu ¨llbar. Eigentlich nur fu ¨r |Φ| = ∞ interessant. Wieso? Notation: Ψ ⊆fin Φ gdw. Ψ ⊆ Φ und |Ψ| < ∞ Beweis von “⇒”: Sei I |= Φ, also gilt I |= ϕ fu ¨r alle ϕ ∈ Φ. Damit ist dann auch I |= Ψ fu ¨r alle Ψ ⊆ Φ, insbesondere falls Ψ ⊆fin Φ. �
61
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.4 Aussagenlogik – Kompaktheit
“⇐” ist schwieriger Beachte: Bei endlich konsistentem Φ kann jedes Ψ ⊆fin Φ verschiedenes Modell haben! Bsp. Φ = {ϕn,m | 0 ≤ n ≤ m} mit ϕn,m =
m �
Ai
i=n
Sei Ψ ⊆fin Φ und IΨ definiert durch � 1 , falls min{n | ϕn,m ∈ Ψ} ≤ k ≤ max{m | ϕn,m ∈ Φ} IΨ (Ak ) = 0 , sonst Beachte: • Fu ¨r alle Ψ ⊆fin Φ gilt IΨ |= Ψ, aber IΨ �|= Φ. • Es gibt unendliche viele Ψ mit paarweise verschiedenen IΨ .
62
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.4 Aussagenlogik – Kompaktheit
63
Lemma 1 fu ¨r die Kompaktheit Lemma 1: Sei ϕ Formel, I, I � Interpretationen, so dass I(A) = I � (A) fu ¨r alle A ∈ Var (ϕ). Dann gilt I |= ϕ gdw. I � |= ϕ. Beweis Per Induktion u ¨ber Aufbau von ϕ. Induktionsanfang: • Fu ¨r ϕ = tt, ff gilt die Aussage sicherlich.
• Sei ϕ = A. Offensichtlich gilt dann A ∈ Vars(ϕ) und damit
dann auch die Aussage.
Induktionsschritt: • Sei ϕ = ¬ψ und die Aussage fu ¨r ψ bereits beweisen. Dann gilt
I |= ϕ
gdw.
I �|= ψ
gdw.
I � �|= ψ
• F¨ alle ϕ = ψ1 ∧ ψ2 , ψ1 ∨ ψ2 genauso.
gdw.
I � |= ϕ �
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.4 Aussagenlogik – Kompaktheit
Lemma 2 fu ¨r die Kompaktheit Lemma 2: Ist Φ endlich konsistent, so ist Φ ∪ {A} oder Φ ∪ {¬A} endlich konsistent. Beweis: Durch Widerspruch. Angenommen, • Φ ist endlich konsistent, aber
• sowohl Φ ∪ {A} als auch Φ ∪ {¬A} sind nicht endlich
konsistent.
Dann ex. unerfu ¨llbare Ψ ⊆fin Φ ∪ {A} und Ψ� ⊆fin Φ ∪ {¬A}.
Somit ist auch Θ := Ψ ∪ Ψ� unerfu ¨llbar, und damit auch Θ ∪ {A} und Θ ∪ {¬A}. Dann muss aber bereits Θ \ {{A}, {¬A}} unerfu ¨llbar sein. Da Θ \ {{A}, {¬A}} ⊆fin Φ, ist Φ also dann nicht endlich konsistent.
64
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.4 Aussagenlogik – Kompaktheit
Beweis des Kompaktheitssatzes Beweis von “⇐” (“Φ endlich konsistent ⇒ Φ erfu ¨llbar”). Seien A0 , A1 , A2 , . . . Variablen in Φ. Def. simultan Φ0 := Φ, Φi+1 := Φi ∪ {�i } und � Ai , falls Φi ∪ {Ai } endlich konsistent �i := ¬Ai , sonst Mit Lemma 2 und Induktion sind alle Φi endlich konsistent. Definiere I u ¨ber � 1 , falls �i = Ai I(Ai ) := 0 , falls �i = ¬Ai Behauptung: I |= ϕ fu ¨r alle ϕ ∈ Φ
65
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.4 Aussagenlogik – Kompaktheit
Beweis des Kompaktheitssatzes
Sei ϕ ∈ Φ. W¨ahle k := max{i | Ai ∈ Var (ϕ)}. Da Φ = Φ0 ⊆ Φ1 ⊆ . . . gilt also ϕ ∈ Φk+1 und somit Ψ := {ϕ, �0 , . . . , �k } ⊆fin Φk+1 Wegen endlicher Konsistenz von Φk+1 ist Ψ erfu ¨llbar. Also ex. I � , so dass I � |= Ψ.
Beachte: I(A) = I � (A) fu ¨r alle A ∈ Var (ϕ) und außerdem I � |= ϕ. Wegen Lemma 1 gilt dann I |= ϕ.
66
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.4 Aussagenlogik – Kompaktheit
Erste Anwendung des Kompaktheitssatzes Theorem 9 (K¨onigs Lemma) Jeder endlich-verzweigende Baum, in dem Pfade beliebiger L¨ange existieren, hat einen unendlichen Ast. Beweis: Sei t Baum mit abz¨ahlbarer Knotenmenge N und Wurzel 0, so dass es Pfade beliebiger L¨ange gibt. Wir schreiben succ(i) fu ¨r die unmittelbaren Nachfolger von i. Betrachte � � � � � ϕi := Xi → ExactlyOne(succ(i)) ∧ ¬Xi → ¬Xj j∈succ(i)
und Φ := {X0 } ∪ {ϕi | i ∈ N}.
• alle Ψ ⊆fin Φ sind erfu ¨llbar wegen Pfaden beliebiger L¨ange • nach Kompaktheit ist dann auch Φ erfu ¨llbar • Modell von Φ liefert unendlichen Pfad in t
67
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.4 Aussagenlogik – Kompaktheit
Zweite Anwendung des Kompaktheitssatzes Kacheln sind Einheitsquadrate mit gef¨arbten Kanten: Sei K eine endliche Menge von Kacheln. Dies induziert zwei Relationen H und V , die besagen, ob zwei Kacheln horizontal bzw. vertikal aneinanderpassen. Eine K -Kachelung der n × n-Ebene ist eine Funktion κ : {0, . . . , n − 1}2 → K , so dass fu ¨r alle i = 0, . . . , n − 2, j = 0, . . . , n − 1 gilt: • (κ(i, j), κ(i + 1, j)) ∈ H
“horizontal passt alles”
• (κ(j, i), κ(j, i + 1)) ∈ V
“vertikal passt alles”
analog K -Kachelung der unendlichen N × N-Ebene definiert
68
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.4 Aussagenlogik – Kompaktheit
Beispiel
Bsp.: K = K -Kachelung der 3 × 3-Ebene:
69
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.4 Aussagenlogik – Kompaktheit
70
Anwendung des Kompaktheitssatzes Theorem 10 Sei K endliche Menge von Kacheln. Wenn jede n × n-Ebene K -kachelbar ist, so ist auch die N × N-Ebene K -kachelbar. Beweis: Benutze Aussagenvariablen Ati,j , i, j ∈ N, t ∈ K mit Bedeutung “das Feld (i, j) ist mit Kachel t belegt” dru ¨cke K -Kachelbarkeit der n × n-Ebene aus: ϕn :=
n−1 � n−1 � i=0 j=0
∧
n−2 � n−1 �
ExactlyOne({Ati,j | t ∈ T }) � �
¬(Ati,j i=0 j=0 (t,t � )�∈H
∧
t� Ai+1,j )
�
∧
� �
¬(Atj,i (t,t � )�∈V
∧
t� Aj,i+1 )
�
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.4 Aussagenlogik – Kompaktheit
Anwendung des Kompaktheitssatzes Beachte: • Erfu ¨llende Belegung fu ¨r ϕn liefert Kachelung der n × n-Ebene. • Wenn m ≤ n, dann ist ϕn → ϕm allgemeingu ¨ltig. Intuitiv:
n × n-Kachelung liefert auch immer eine m × m-Kachelung.
Sei Φ := {ϕn | n ∈ N}. “Jede n × n-Ebene ist K -kachelbar” bedeutet: Fu ¨r alle n ∈ N ist ϕn erfu ¨llbar. Sei Ψ ⊆fin Φ. Dann ist Ψ = {ϕi1 , . . . , ϕik } fu ¨r ein k ∈ N und i1 < i2 < . . . < ik . Da ϕik erfu ¨llbar ist, ist mit obiger Bemerkung auch Ψ erfu ¨llbar. Aus dem Kompaktheitssatz folgt, dass auch Φ erfu ¨llbar ist; erfu ¨llende Belegung induziert Kachelung der N × N-Ebene mit K .
71
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.5 Aussagenlogik – Resolution
Beweiskalku ¨le DPLL-Algorithmus in gewisser Weise semantisches Verfahren zum Erkennen von Erfu ¨llbarkeit. (Konstruiert Modell fu ¨r Formel) Im folgenden zwei syntaktische Verfahren zum Erkennen von (Un-)Erfu ¨llbarkeit / Allgemeingu ¨ltigkeit. 1
Resolution (fu ¨r Unerfu ¨llbarkeit)
2
Sequenzenkalku ¨l (fu ¨r Folgerungsbeziehung und damit insbesondere Allgemeingu ¨ltigkeit)
Beachte Zusammenhang zwischen Erfu ¨llbarkeit und Allgemeingu ¨ltigkeit (und auch Folgerungsbeziehung, wie wir noch sehen werden): diese Verfahren sind somit auch in der Lage, die jeweils anderen Fragestellungen zu l¨osen.
72
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.5 Aussagenlogik – Resolution
Resolventen ¨ Wir erweitern den Begriff der Aquivalenz auf Klauselmengen. Sei C Klausel, K, K� Klauselmengen: � I |= C gdw. I |= � �∈C
I |= K
K ≡ K�
gdw. gdw.
Def.: Sei � Literal. �¯ :=
fu ¨r alle C ∈ K : I |= C
fu ¨r alle I : I |= K gdw. I |= K� �
¬A A
, falls � = A, , falls � = ¬A
Def.: Seien C1 , C2 Klauseln, � Literal, so dass � ∈ C1 , �¯ ∈ C2 . Dann heisst ¯ C := (C1 \ {�}) ∪ (C2 \ {�}) Resolvente von C1 und C2 .
73
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.5 Aussagenlogik – Resolution
Das Resolutionslemma Lemma: Sei K Klauselmenge, C1 , C2 ∈ K, C Resolvente von C1 und C2 . Dann gilt: K ≡ K ∪ {C }. Beweis: “⇐=” Sei I |= K ∪ {C }. Da K ⊆ K ∪ {C }, gilt dann auch I |= K. “=⇒” Sei I |= K. Es reicht aus zu zeigen, dass I |= C gilt. Da C1 , C2 ∈ K gilt also insbesondere I |= C1 und I |= C2 . D.h. es gibt Literale �1 ∈ C1 , �2 ∈ C2 , so dass I |= �1 und I |= �2 . Somit ¯ fu gilt �1 �= �¯2 . Da C = (C1 \ {�}) ∪ (C2 \ {�}) ¨r ein � ∈ C1 muss �1 ∈ C oder �2 ∈ C sein. Dann gilt aber I |= C . Def. Sei K Klauselmenge, Res(K) ist Menge aller Resolventen von Klauseln in K.
74
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.5 Aussagenlogik – Resolution
Resolution Def.: Ein Resolutionsbeweis fu ¨r (Unerfu ¨llbarkeit von) K ist ein endlicher, bin¨ar verzweigender Baum, dessen Knoten mit Klauseln beschriftet sind und fu ¨r den gilt: • Die Wurzel ist mit ∅ beschriftet. • An den Bl¨ attern stehen nur Klauseln aus K. • Die Beschriftung eines inneren Knoten ist Resolvente der Beschriftungen seiner beiden S¨ohne. Bsp.: Gibt es Resolutionsbeweise jeweils fu ¨r • K = {{A, B}, {A, ¬B}, {¬A, B}, {¬A, ¬B}}, A, B
¬A, B
A, ¬B
¬A, ¬B
¬B
B ∅ • K = {{A, B}, {A, ¬B}, {¬A, B}}?
75
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.5 Aussagenlogik – Resolution
Korrektheit der Resolution Theorem 11 Sei K Klauselmenge. K ist unerfu ¨llbar gdw. es einen Resolutionsbeweis fu ¨r K gibt. Beweis: “⇐=” Angenommen, es existiert Resolutionsbeweis T der H¨ohe h fu ¨r K. Definiere Klauselmengen wie folgt. K0 := {C | C Blatt in T }
Ki+1 := Ki ∪ Res(Ki ) Beachte:
• ∅ ∈ Kh+1 , also Kh+1 unerfu ¨llbar. • K0 ≡ . . . ≡ Kh+1 nach Resolutionslemma, also K0 unerfu ¨llbar. • K0 ⊆ K, also K unerfu ¨llbar.
76
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.5 Aussagenlogik – Resolution
Vollst¨ andigkeit der Resolution andere Richtung schwieriger: konstruiere Resolutionsbeweis fu ¨r unerfu ¨llbare Klauselmenge “=⇒” Angenommen K ist unerfu ¨llbar. Nach dem Kompaktheitssatz existiert K0 ⊆fin K, welches bereits unerfu ¨llbar ist. Offensichtlich gilt: Ein Resolutionsbeweis fu ¨r K0 ist auch einer fu ¨r K. Sei Var (K0 ) = {A1 , . . . , An }. Wir zeigen die Existenz eines Resolutionsbeweises fu ¨r K0 durch Induktion u ¨ber n. Induktionsanfang, n = 0. Dann ist Var (K0 ) = ∅. Es gibt nur zwei Klauselmengen u ¨ber der leeren Variablenmenge: ∅ und {∅}. Da ∅ aber trivialerweise erfu ¨llbar ist, muss K0 = {∅} gelten. Offensichtlich l¨asst sich dafu ¨r ein Resolutionsbeweis bauen.
77
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.5 Aussagenlogik – Resolution
Vollst¨ andigkeit der Resolution Induktionsschritt, n > 0. Die Induktionshypothese besagt, dass es fu ¨r unerfu ¨llbare Klauselmengen u ¨ber den Variablen A1 , . . . , An−1 Resolutionsbeweise gibt. Konstruiere nun K0+ := {C \ {¬An } | C ∈ K0 und An �∈ C } K0− := {C \ {An } | C ∈ K0 und ¬An �∈ C } ¨ Beachte: sowohl K0+ als auch K0− sind unerfu und ¨llbar (Ubung) enthalten h¨ochstens die Variablen A1 , . . . , An−1 . Die Induktionshypothese liefert nun also zwei Resolutionsbeweise T + und T − . Durch Einfu ¨gen von ¬An in jede Klausel in T + und An in jede Klausel in T − entstehen B¨aume mit Wurzeln in K0 , deren innere Knoten jeweils Resolventen ihrer S¨ ohne sind. Durch Resolution nach den Literalen ¬A und A entsteht aus diesen ein Resolutionsbeweis fu ¨ r K0 .
78
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.5 Aussagenlogik – Resolution
Resolution verwenden Unerfu ¨llbarkeit ist eine universelle Eigenschaft: alle Interpretationen sind kein Modell. Resolution charakterisiert dies existentiell: statt alle Interpretationen fu ¨r eine Formel zu testen, reicht es aus, einen Resolutionsbeweis anzugeben. Aber: Resolutionsbeweise k¨onnen exponentielle Gr¨ oße haben ¨ (Ubung). Im Vergleich: Zeugen fu ¨r Erfu ¨llbarkeit (Modelle) haben h¨ochstens lineare Gr¨oße. Beweissuche im Resolutionskalku ¨ l fu ¨r Klauselmenge K: K0 := K
Kn+1 := Kn ∪ Res(Kn ) Iteration bis ∅ als Resolvente auftritt oder Kn+1 = Kn fu ¨r ein n gilt.
79
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.6 Aussagenlogik – Der Sequenzen-Kalku ¨l
Sequenzen
Zum Abschluss des Kapitels u ¨ber Aussagenlogik behandeln wir noch Gentzens Sequenzenkalku ¨l. Def.: Eine Sequenz ist ein Paar Γ =⇒ ∆ von Formel(multi)mengen. Γ heißt Antezedens, ∆ Sukzedens. Vereinfachte Schreibweise ohne Mengenklammern, etc.: ϕ1 , . . . , ϕn =⇒ ψ1 , . . . , ψm Def.: Γ =⇒ ∆ ist gu ¨ltig, falls fu ¨r alle I gilt: wenn I |= ϕ fu ¨r alle ϕ ∈ Γ dann I |= ψ fu ¨r ein ψ ∈ ∆
80
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.6 Aussagenlogik – Der Sequenzen-Kalku ¨l
Beispiele
Bsp.: welche der folgenden Sequenzen sind gu ¨ltig? 1
A, A → B =⇒ B
2
¬A, ¬B =⇒ A, B
3
A, A → B =⇒ ∅
4
A, ¬A =⇒ B
5
A → B, B → C , A =⇒ C
6
A ∧ B → C , A =⇒ B → C
81
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.6 Aussagenlogik – Der Sequenzen-Kalku ¨l
Folgerung und Allgemeingu ¨ltigkeit etc. Gu ¨ltigkeit von Sequenzen kann bekannte Konzepte wie Allgemeingu ¨ltigkeit etc. ausdru ¨cken, z.B. Lemma: ϕ ist allgemeingu ¨ltig gdw. die Sequenz ∅ =⇒ ϕ gu ¨ltig ist. ¨ Beweis: Ubung. Was bedeutet die Gu ¨ltigkeit der Sequenz ϕ =⇒ ∅? Kann umgekehrt z.B. Gu ¨ltigkeit von Sequenzen auf Allgemeingu ¨ltigkeit von Formeln zuru ¨ckgefu ¨hrt werden? Bei endlichen Sequenzen ist dies der Fall: � � Γ =⇒ ∆ gu gdw. ( Γ) → ( ∆) allgemeingu ¨ltig ¨ltig
82
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.6 Aussagenlogik – Der Sequenzen-Kalku ¨l
Beweise im Sequenzenkalku ¨l Ziel: Formalismus (“Sequenzenkalku ¨l”), der genau die gu ¨ltigen Sequenzen charakterisiert Def.: Ein Beweis im Sequenzenkalku ¨ l fu ¨r eine Sequenz Γ =⇒ ∆ ist ein endlicher Baum, dessen • Wurzel mit Γ =⇒ ∆ beschriftet ist, • Bl¨ atter mit Axiomen beschriftet sind, • innere Knoten mit ihren S¨ ohnen Instanzen von Beweisregeln sind. Beweisregeln haben die Form Γ1 =⇒ ∆1
. . . Γn =⇒ ∆n Γ =⇒ ∆
(Name)
Γi =⇒ ∆i heißen Pr¨amissen, Γ =⇒ ∆ Konklusion Axiom = Beweisregel ohne Pr¨amissen
83
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.6 Aussagenlogik – Der Sequenzen-Kalku ¨l
84
Axiome und Regeln des Sequenzenkalku ¨ls Axiome: Γ, ff =⇒ ∆
(ffL )
Γ =⇒ ∆, tt
(ttR )
Γ, ϕ =⇒ ∆, ϕ
(Ax)
Beweisregeln: Γ, ϕ, ψ =⇒ ∆ Γ, ϕ ∧ ψ =⇒ ∆
(∧L )
Γ =⇒ ∆, ϕ Γ =⇒ ∆, ψ Γ =⇒ ∆, ϕ ∧ ψ
Γ, ϕ =⇒ ∆ Γ, ψ =⇒ ∆ Γ, ϕ ∨ ψ =⇒ ∆
(∨L )
Γ =⇒ ∆, ϕ, ψ Γ =⇒ ∆, ϕ ∨ ψ
(∧R )
(∨R )
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.6 Aussagenlogik – Der Sequenzen-Kalku ¨l
85
Beweisregeln des Sequenzenkalku ¨ls
Γ =⇒ ∆, ϕ Γ, ¬ϕ =⇒ ∆
(¬L )
Γ =⇒ ∆, ϕ Γ, ψ =⇒ ∆ Γ, ϕ → ψ =⇒ ∆ Γ =⇒ ∆ Γ, tt =⇒ ∆
Γ, ϕ =⇒ ∆ Γ =⇒ ∆, ¬ϕ
(ttL )
(¬R )
Γ, ϕ =⇒ ∆, ψ Γ =⇒ ∆, ϕ → ψ
(→L )
Γ =⇒ ∆ Γ =⇒ ∆, ff
¨ Es fehlen noch 2 Regeln fu ¨r ↔ (Ubung)
(ffR )
(→R )
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.6 Aussagenlogik – Der Sequenzen-Kalku ¨l
86
Beispiel
Formel ϕ := A ∨ (B ∧ C ) → (A ∨ B) ∧ (A ∨ C ) ist allgemeingu ¨ltig. Wie sieht Beweis fu ¨r ∅ =⇒ ϕ aus?
B, C =⇒ A, B B, C =⇒ A ∨ B
(Ax) (∨R )
B, C =⇒ A, C
(Ax)
B, C =⇒ A ∨ C
B, C =⇒ (A ∨ B) ∧ (A ∨ C ) B ∧ C =⇒ (A ∨ B) ∧ (A ∨ C )
(∧L )
(∨R ) (∧R )
A =⇒ A, B A =⇒ A ∨ B
(Ax) (∨R )
A =⇒ A, C A =⇒ A ∨ C
A =⇒ (A ∨ B) ∧ (A ∨ C )
A ∨ (B ∧ C ) =⇒ (A ∨ B) ∧ (A ∨ C ) ∅ =⇒ A ∨ (B ∧ C ) → (A ∨ B) ∧ (A ∨ C )
(→R )
(Ax) (∨R ) (∧R )
(∨L )
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.6 Aussagenlogik – Der Sequenzen-Kalku ¨l
Axiomen- und Ableitungslemma Ziel: zeige, dass im Sequenzenkalku ¨l genau die gu ¨ltigen Sequenzen beweisbar sind dazu brauchen wir zun¨achst zwei Lemmas Lemma: (Axiomenlemma I) Jede Sequenz Γ =⇒ ∆, die ein Axiom ist, ist gu ¨ltig. Beweis: Leicht zu sehen fu ¨r Axiome (ffL ) und (ttR ). Betrachte noch Axiom�(Ax) mit Γ, ϕ =⇒ ∆,�ϕ. Sei I Interpretation. Zu zg.: Wenn I |= Γ ∪ {ϕ} � dann I |= ∆ ∪ {ϕ}. Angenommen, I |= �Γ ∪ {ϕ}. Dann�gilt insbesondere I |= ϕ und somit auch I |= ϕ ∨ ∆ bzw. I |= ∆ ∪ {ϕ}. Lemma: (Ableitungslemma) Fu ¨r alle Regeln des Sequenzenkalku ¨ls gilt: Die Konklusion ist gu ¨ltig gdw. alle Pr¨amissen gu ¨ltig sind.
87
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.6 Aussagenlogik – Der Sequenzen-Kalku ¨l
Beweis des Ableitungslemmas Beweis Wir zeigen dies exemplarisch fu ¨r die Regeln (∧L ) und (∧R ). � � Fall (∧L ). Dies ist trivial, da Γ ∪ {ϕ ∧ ψ} ≡ Γ ∪ {ϕ, ψ}. Fall (∧R ). Zur Erinnerung: Konklusion K = Γ =⇒ ∆, ϕ ∧ ψ, Pr¨amissen sind P1 = Γ =⇒ ∆, ϕ und P2 = Γ =⇒ ∆, ψ.
“⇒” Angenommen, eine der beiden Pr¨amissen ist ungu ¨ltig. � Sei dies P1 . Der � Fall mit P2 ist analog. Dann ex. I, so dass I |= � Γ und I �|= ∆ ∪ {ϕ}. Daraus folgt insbesondere, dass I �|= ∆ und I �|= ϕ. � Somit gilt dann � aber auch I �|= ϕ ∧ ψ. Zusammengefasst: I |= Γ und I �|= ∆ ∪ {ϕ ∧ ψ}. Also ist K nicht gu ¨ltig. “⇐” Angenommen, die � Konklusion ist ungu ¨ltig. Also gibt es I, so � dass I |= Γ und I �|= ∆ ∪ {ϕ ∧ ψ}. Insbesondere gilt I �|= ϕ � ∧ ψ, also I �|= ϕ oder � I �|= ψ. Dann gilt auch I �|= ∆ ∪ {ϕ} oder I �|= ∆ ∪ {ψ}. Also ist entweder P1 ungu ¨ltig oder P2 ungu ¨ltig.
88
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.6 Aussagenlogik – Der Sequenzen-Kalku ¨l
Korrektheit des Sequenzenkalku ¨ls Theorem 12 Jede im Sequenzenkalku ¨l beweisbare Sequenz ist gu ¨ltig. Beweis: Angenommen es ex. Beweis fu ¨r Γ =⇒ ∆. Wir zeigen per Induktion u ¨ber die H¨ohe h des Beweisbaums, dass Γ =⇒ ∆ gu ¨ltig ist. Induktionsanfang h = 0. Dann ist Γ =⇒ ∆ ein Axiom und laut Axiomenlemma I gu ¨ltig. Induktionsschritt. Sei h > 0. Dann gibt es eine Beweisregel mit Pr¨amissen P1 , . . . , Pn , zu denen Γ =⇒ ∆ Konklusion ist. Beachte: Jedes Pi ist beweisbar im Sequenzenkalku ¨l mit einem Beweis der Ho¨he < h. Nach Induktionsvoraussetzung sind alle Pi somit gu ¨ltig. Mit dem Ableitungslemma folgt dann, dass auch Γ =⇒ ∆ gu ¨ltig sein muss. �
89
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.6 Aussagenlogik – Der Sequenzen-Kalku ¨l
Vorbereitung auf die Vollst¨ andigkeit Lemma: (Axiomenlemma II) Angenommen Γ, ∆ ⊆ V. Dann ist Γ =⇒ ∆ gu ¨ltig gdw. Γ ∩ ∆ �= ∅. Beweis: “⇒” Angenommen, Γ ∩ ∆ = ∅. Wir zeigen, dass Γ =⇒ ∆ ungu ¨ltig ist, indem wir eine falsifizierende Interpretation angeben. � 1 , falls A ∈ Γ I(A) := 0 , sonst Aufgrund der Voraussetzung gilt I(B) = 0 fu ¨r alle B ∈ ∆. Also gilt � � I |= Γ und I �|= ∆ und somit ist Γ =⇒ ∆ nicht gu ¨ltig.
90
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.6 Aussagenlogik – Der Sequenzen-Kalku ¨l
Maß einer Sequenz Ziel: Umkehrung von Thm. 12 (gu ¨ltige Sequenzen sind beweisbar) schwierig, denn “fu ¨r alle Interpretationen . . . ⇒ es gibt Beweis . . . ” Intuition: auf gu ¨ltige Sequenzen lassen sich Beweisregeln sinnvoll anwenden, so dass am Ende ein Beweis entstanden ist Was heißt “am Ende”? Wir mu ¨ssen irgendwie zeigen, dass dieser Prozess auch terminiert. Def.: (Maß) ||Γ −→ ∆|| :=
�
ϕ∈Γ
||ϕ|| +
�
ϕ∈∆
||ϕ||, wobei
||tt|| = ||ff|| := 1 ||A|| := 0
||¬ϕ|| := 1 + ||ϕ||
||ϕ ∧ ψ|| = ||ϕ ∨ ψ|| = ||ϕ → ψ|| = ||ϕ ↔ ψ|| := 1 + ||ϕ|| + ||ψ||
91
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.6 Aussagenlogik – Der Sequenzen-Kalku ¨l
Vollst¨ andigkeit des Sequenzenkalku ¨ls
Theorem 13 Jede gu ¨ltige Sequenz ist im Sequenzenkalku ¨l beweisbar. Beweis: Sei Γ =⇒ ∆ gu ¨ltig. Wir zeigen, dass es auch beweisbar ist durch Induktion u ¨ber j = ||Γ =⇒ ∆||. Induktionsanfang, j = 0. Dann besteht Γ ∪ ∆ nur aus Variablen. Nach dem Axiomenlemma II gilt Γ ∩ ∆ �= ∅. Dann ist Γ =⇒ ∆ Instanz von (Ax) und somit beweisbar. Induktionsschritt, j > 0. Also existiert noch mindestens ein Junktor oder eine Konstante in Γ ∪ ∆. Wir unterscheiden zwei F¨alle.
92
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.6 Aussagenlogik – Der Sequenzen-Kalku ¨l
Vollst¨ andigkeit des Sequenzenkalku ¨ls
1
ff ∈ Γ oder tt ∈ ∆. Dann ist Γ =⇒ ∆ Instanz von (ffL ) oder (ttR ) und somit beweisbar.
2
Sonst. Da j > 0 muss mindestens eine Beweisregel anwendbar sein. Nach dem Ableitungslemma sind alle entstehenden Pr¨amissen gu ¨ltig. Außerdem ist deren Maß jeweils echt kleiner als j. Nach Induktionshypothese sind diese beweisbar. Durch Verknu ¨pfung derer Beweisb¨aume erh¨alt man einen Beweis fu ¨r Γ =⇒ ∆.
93
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.6 Aussagenlogik – Der Sequenzen-Kalku ¨l
Beweissuche Der Sequenzenkalku ¨l erm¨oglicht es, automatisch festzustellen, ob eine gegebene Formel allgemeingu ¨ltig ist. Systematisch wendet man Regeln auf die Sequenz ∅ =⇒ ϕ an, um einen Beweisbaum zu konstruieren. Alle Pfade enden in Axiomen � Beweis gefunden. Ein Pfad endet in Sequenz, die kein Axiom ist und auf die keine Regel angewandt werden kann � kein Beweis m¨oglich. Beachte: Die Regel selbst verlangen zwar keine Auswahl seitens des Benutzers; auf eine Sequenz k¨onnen jedoch i.A. mehrere Regeln angewandt werden. Reihenfolge der Regelanwendungen unerheblich dafu ¨r, ob Beweis gefunden wird oder nicht. Sie kann aber die Gr¨oße des gefundenen Beweises beeinflussen.
94
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.6 Aussagenlogik – Der Sequenzen-Kalku ¨l
95
Beispiel B =⇒ A, B, C A =⇒ A, B, C
C =⇒ A, B, C
(B ∨ C ) =⇒ A, B, C
A ∨ (B ∨ C ) =⇒ A, B, C A ∨ (B ∨ C ) =⇒ A ∨ B, C
A =⇒ A, B, C A =⇒ A ∨ B, C
(∨R )
A =⇒ (A ∨ B) ∨ C
(∨R )
B =⇒ A ∨ B, C
(∨R )
(∨R )
B =⇒ (A ∨ B) ∨ C
(∨L )
(∨R )
A ∨ (B ∨ C ) =⇒ (A ∨ B) ∨ C B =⇒ A, B, C
(∨R )
C =⇒ A, B, C C =⇒ A ∨ B, C
(∨R )
C =⇒ (A ∨ B) ∨ C
B ∨ C =⇒ (A ∨ B) ∨ C
A ∨ (B ∨ C ) =⇒ (A ∨ B) ∨ C
(∨L )
(∨L )
(∨R ) (∨L )
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.6 Aussagenlogik – Der Sequenzen-Kalku ¨l
Andere Beweisregeln
Hier vorgestellter Sequenzenkalku ¨l ist ein System fu ¨r aussagenlogische Beweise. Gibt es auch andere, vielleicht bessere? Einfachere Frage: Gibt es noch andere Beweisprinzipien (≈ Beweisregeln), mit denen man einfach Beweise fu ¨hren kann? zwei M¨oglichkeiten, Sequenzenkalku ¨l zu erweitern: • herleitbare Regeln • zul¨ assige Regeln
96
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.6 Aussagenlogik – Der Sequenzen-Kalku ¨l
97
Herleitbarkeit Def.: Eine Regel mit Pr¨amissen P1 , . . . , Pn und Konklusion K heißt herleitbar, wenn es einen Beweis fu ¨r K gibt, der P1 , . . . , Pn als Axiome benutzt. Bsp.: Die folgenden Regeln sind z.B. im Sequenzenkalku ¨l herleitbar. Γ =⇒ ∆, ϕ1 . . . Γ =⇒ ∆, ϕn Γ =⇒ ∆, ϕ1 ∧ . . . ∧ ϕn
(∧∗R )
Γ, ϕ, ψ =⇒ ∆ Γ =⇒ ∆, ¬(ϕ ∧ ψ)
(NANDR )
Herleitbare Regeln k¨onnen die Beweissuche vereinfachen. Außerdem sollte folgendes offensichtlich sein. Thm.: Eine Sequenz ist in einem Sequenzenkalku ¨l mit zus¨atzlichen herleitbaren Regeln beweisbar, gdw. sie gu ¨ltig ist.
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.6 Aussagenlogik – Der Sequenzen-Kalku ¨l
Zul¨ assigkeit Def.: Eine Regel heißt zul¨assig, wenn sich im Sequenzenkalku ¨l mit dieser Regel dieselben Sequenzen beweisen lassen wie ohne diese Regel. Bsp.: Die folgenden Regeln sind z.B. zul¨assig aber nicht herleitbar! Γ =⇒ ∆ Γ, ϕ =⇒ ∆
(WeakL )
Γ =⇒ ∆ Γ =⇒ ∆, ϕ
(WeakR )
Bem.: Jede herleitbare Regel ist zul¨assig. Nicht jede zul¨assige Regel ist herleitbar. Thm.: Eine Sequenz ist in einem Sequenzenkalku ¨l mit zus¨atzlichen zul¨assigen Regeln beweisbar, gdw. sie gu ¨ltig ist.
98
Theoretische Informatik: Logik, M. Lange, FB16, Uni Kassel:
3.6 Aussagenlogik – Der Sequenzen-Kalku ¨l
Fallunterscheidung
Fallunterscheidung ist wichtiges Beweisprinzip, welches Beweise vereinfachen kann. im Sequenzenkalku ¨l: Γ, ¬ϕ =⇒ ∆ Γ, ϕ =⇒ ∆ Γ =⇒ ∆
(CD)
Bsp.: beweise ∅ =⇒ (A ∧ B) ∨ (¬A ∧ B) ∨ (A ∧ ¬B) ∨ (¬A ∧ ¬B) jeweils mit und ohne Regel (CD) Thm.: (CD) ist nicht herleitbar aber zul¨assig.
99
