Vorlesung Logiksysteme
Sommer 2015 – v4
Martin Mundhenk
Univ. Jena, Institut f¨
ur Informatik
22. April 2015
0.0.1
Ein paar einfu
¨hrende Worte
I
Logik heißt korrekte Schl¨usse ziehen . . .
(Aristoteles, 300 v.Chr.)
I
Aussagenlogik ist auch nur Rechnen . . .
(Boole, Mitte 19.Jhdt)
I
Alles Formale ist Logik . . .
(Frege, Peano, Russell um 1900)
0.0.2
Logik in der Informatik
Turing zeigt 1936 die Unentscheidbarkeit des
G¨ultigkeitsproblems der Pr¨adikatenlogik.
Shannon zeigt 1937, dass Aussagenlogik zur Beschreibung und
Optimierung elektromagnetischer Schaltungen benutzt werden kann.
Newell, Simon, Robinson entwickeln in den 1950ern erste Algorithmen
zur logischen Deduktion und wenden sie auf KI-Probleme an.
Cook zeigt 1972 die NP-Vollst¨andigkeit des
Erf¨ullbarkeitsproblems der Aussagenlogik.
0.0.3
Logikanwendungen in der Informatik
I
Entwurf und Verifikation digitaler Schaltkreise
I
Beschreibung komplexer Systeme
I
Verifikation der Korrektheit von Programmen
I
Datenbanken
I
K¨unstliche Intelligenz
I
Logisches Programmieren
Inhalt dieser Vorlesung
I
Was wird betrachtet?
1. Aussagenlogik
2. Nicht-klassische Aussagenlogiken
I
I
I
Modallogik
Temporale Logik
Wie wird es betrachtet?
Schwerpunkt auf Beweissystemen und deren Vollst¨andigkeit
I
I
I
Wie lassen sich g¨
ultige Formeln formal beschreiben?
Wie lassen sich formale Beschreibungen zu Algorithmen umbauen?
Ziel: Verst¨andnis der Vollst¨andigkeitsbeweise
und Bef¨ahigung zum selbst¨andigen F¨uhren “kleiner” Beweise
Zitate
Edsger W. Dijkstra:
Informatik = VLSAL
(Very Large Scale Application of Logics)
Georg Gottlob:
Informatik ist die Fortsetzung der Logik mit anderen Mitteln.
0.0.6
¨
Formalien zur Vorlesung/Ubung
I
Termine:
montags 16:15–17:45 Uhr
mittwochs 16:15–17:45 Uhr
Logik-Sprechstunde freitags 10-12 Uhr (oder n.V.)
I
Zulassungsvoraussetzung zur Pr¨ufung:
¨
ausreichende Bearbeitung der schriftlichen Ubungsaufgaben
mit w¨ochentlicher Abgabe mittwochs und
¨
aktive Teilnahme an den Ubungen.
I
Modulpr¨ufung:
m¨undliche Pr¨ufung
(Termin wird noch bekanntgegeben)
0.0.7
Vorlesung Logiksysteme
Sommer 2015
1. Klassische Aussagenlogik
2. Modale Aussagenlogik
3. Temporale Logik
0.0.1
1 Klassische Aussagenlogik
1. Klassische Aussagenlogik
Grundbegriffe
Tableau-Kalk¨ul
Algorithmen
Frege-Kalk¨ul
Nat¨urliches Schließen
Vergleich von Beweis-Kalk¨ulen
1 Grundbegriffe Aussagenlogik
1. Klassische Aussagenlogik
Grundbegriffe
Sprache (Formeln)
Semantik (Belegungen und die Erf¨
ullungsrelation)
Erf¨
ullbarkeit und G¨
ultigkeit
¨
Aquivalenz
und ad¨aquate Formelmengen
Semantische Folgerung
Algorithmische Fragen
Tableau-Kalk¨ul
Algorithmen
Frege-Kalk¨ul
Nat¨urliches Schließen
Vergleich von Beweis-Kalk¨ulen
[Literatur:
Sch¨oning: Logik f¨
ur Informatiker
((fast) jedes Logikbuch)]
1.1 Grundbegriffe
Wir werden die Grundbegriffe der Aussagenlogik definieren:
I
aussagenlogische Formeln
I
Belegungen f¨ur Formeln
I
I
Erf¨ullung einer Formel durch eine Belegung
¨
Erf¨ullbarkeit, G¨ultigkeit und Aquivalenz
von Formeln
I
semantische Folgerung
Syntax: Formeln
Definition 1.1 (die Sprache der Aussagenlogik: Formeln)
Eine atomare Formel (kurz: Atom) hat die Form Ai f¨ur i = 0, 1, 2, . . .
(Aussagenlogische) Formeln sind induktiv definiert wie folgt.
1. Die Konstanten ⊥ (falsum) und > (verum) und alle Atome
sind Formeln.
2. F¨ur alle Formeln α ist ¬α (Negation von α) ebenfalls eine Formel.
F¨ur alle Formeln α und β sind
(α ∧ β) (Konjunktion von α und β, logisches Und ),
(α ∨ β) (Disjunktion von α und β, logisches Oder ) und
(α → β) (Implikation von α und β, logische Folgerung )
ebenfalls Formeln.
(3. Es gibt keine anderen Formeln.)
Semantik: Belegung und Erfu
¨llungsrelation
Definition 1.2 (Belegung)
Eine Belegung B ist eine Menge B ⊆ {A0 , A1 , A2 , . . .} von Atomen.
Definition 1.3 (Erf¨
ullungsrelation
)
Sei B eine Belegung, α und β seien Formeln.
Die Relation zwischen Belegungen und Formeln ist wie folgt definiert.
B
>
B
Ai gdw. Ai ∈ B, f¨ur atomare Formeln Ai
B
und
B 6
¬α gdw. B 6
⊥
α
B
(α ∧ β) gdw. B
α und B
β
B
(α ∨ β) gdw. B
α oder B
β
(α → β) gdw. B 6
α oder B
β
B
Erfu
¨llbarkeit, Gu
¨ltigkeit
F¨ur “B
α” sagt man “B erf¨ullt α”.
F¨ur Formelmengen Γ bedeutet B Γ (“B erf¨ullt Γ”),
dass B ϕ f¨ur alle ϕ ∈ Γ gilt.
Definition 1.4 (erf¨
ullbar, g¨
ultig)
1. Eine Formel heißt erf¨ullbar,
wenn es eine Belegung gibt, die sie erf¨ullt.
Anderenfalls heißt die Formel unerf¨ullbar (oder Kontradiktion).
2. Wenn α von jeder Belegung erf¨ullt wird,
dann heißt α g¨ultig (oder Tautologie, Schreibweise:
α).
1.1.5
Abku
¨rzende Schreibweisen
A, B, C , . . . oder . . . f¨ur A0 , A1 , A2 , . . .
(α ↔ β) f¨ur ((α → β) ∧ (β → α))
(
n
V
i=1
n
W
(
αi ) f¨ur (. . . ((α1 ∧ α2 ) ∧ α3 ) ∧ . . . ∧ αn )
αi ) f¨ur (. . . ((α1 ∨ α2 ) ∨ α3 ) ∨ . . . ∨ αn )
i=1
1.1.6
¨
Aquivalente
Formeln
Die Formeln (A ∧ B) und ¬(¬A ∨ ¬B) werden von den gleichen
Belegungen erf¨ullt.
I
Die Belegungen ∅, {A} und {B} erf¨ullen beide Formeln nicht.
I
Die Belegung {A, B} erf¨ullt beide Formeln.
I
Jede andere Belegung entspricht f¨ur die Atome A und B einer der
obigen Belegungen.
Definition 1.5 (semantisch ¨
aquivalent)
Formeln α und β heißen (semantisch) ¨aquivalent (α ≡ β),
falls f¨ur jede Belegung B gilt: B α genau dann, wenn B
β.
1.1.7
¨
Lemma 1.6 (n¨
utzliche Aquivalenzen)
Idempotenz:
(α ∧ α) ≡ α
(α ∨ α) ≡ α
Kommutativit¨at:
(α ∧ β) ≡ (β ∧ α)
(α ∨ β) ≡ (β ∨ α)
Absorption:
(α ∧ (α ∨ β)) ≡ α
(α ∨ (α ∧ β)) ≡ α
Doppelnegation:
¬¬α ≡ α
deMorgan’s Regeln:
¬(α ∧ β) ≡ (¬α ∨ ¬β)
¬(α ∨ β) ≡ (¬α ∧ ¬β)
Tautologieregeln:
(α ∧ >) ≡ α
(α ∨ >) ≡ >
Kontradiktionsregeln:
(α ∧ ⊥) ≡ ⊥
(α ∨ ⊥) ≡ α
1.1.8
(Fortsetzung von Lemma 1.6)
Negation von Konstanten:
¬⊥ ≡ >
Gesetz des ausgeschlossenen Dritten:
(α ∨ ¬α) ≡ >
¬> ≡ ⊥
(α ∧ ¬α) ≡ ⊥
Implikation:
(α → β) ≡ (¬α ∨ β)
Assoziativit¨at:
((α ∧ β) ∧ γ) ≡ (α ∧ (β ∧ γ))
((α ∨ β) ∨ γ) ≡ (α ∨ (β ∨ γ))
Distributivit¨at:
(α ∧ (β ∨ γ)) ≡ ((α ∧ β) ∨ (α ∧ γ))
(α ∨ (β ∧ γ)) ≡ ((α ∨ β) ∧ (α ∨ γ))
Vereinfachende Schreibweise:
“¨uberfl¨ussige” Klammern k¨onnen weggelassen werden.
¨
Aquivalentes
Umformen
¨
Satz 1.7 (Aquivalentes
Ersetzen ergibt ¨
aquivalente Formel)
Sei ϕ eine Formel mit der Teilformel α,
und β sei ¨aquivalent zu α.
Sei ϕ0 eine Formel, die aus ϕ entsteht,
wenn ein Vorkommen der Teilformel α durch β ersetzt wird.
Dann sind ϕ und ϕ0 ¨aquivalent.
Beispiel:
ϕ
α
β
ϕ0
=
=
=
=
(B → (A ∧ (A ∨ B)))
(A ∧ (A ∨ B))
A
(B → A)
¨
Die semantische Aquivalenz
von Formeln l¨asst sich jetzt
syntaktisch durch ¨aquivalentes Umformen verifizieren
¨
(da ≡ eine Aquivalenzrelation
ist).
Beispiel 1: (A → B) ≡ (¬B → ¬A)
(A → B) ≡
≡
≡
≡
(¬A ∨ B)
(¬A ∨ ¬¬B)
(¬¬B ∨ ¬A)
(¬B → ¬A)
(Implikation)
(Doppelnegation)
(Kommutativit¨at)
(Implikation)
1.1.11
Beispiel 2: ((A ∧ B) → C ) ≡ (A → (B → C ))
((A ∧ B) → C )
≡ (¬(A ∧ B) ∨ C )
≡ ((¬A ∨ ¬B) ∨ C )
≡ (¬A ∨ (¬B ∨ C ))
≡ (¬A ∨ (B → C ))
≡ (A → (B → C ))
(Implikation)
(deMorgan)
(Assoziativit¨at)
(Implikation)
(Implikation)
Allgemeiner gilt:
n
^
i=1
Ai → B ≡ (A1 → (A2 → (· · · → (An → B) · · · )))
Beispiel 3: (⊥ → ⊥) ≡ >
(⊥ → ⊥)
≡ (¬⊥ ∨ ⊥) (Implikation)
≡ (> ∨ ⊥)
(Negation von Konstanten)
≡ >
(Kontradiktionsregel)
Beispiel 4: ¬α ≡ (α → ⊥) f¨ur jede Formel α
¬α
≡ (¬α ∨ ⊥) (Kontradiktionsregel)
≡ (α → ⊥) (Implikation)
Lemma 1.8 (⊥ und → sind ad¨
aquat)
F¨ur jede aussagenlogische Formel ϕ gibt es eine ¨aquivalente Formel ϕ0 ,
die nur Atome, ⊥ und → enth¨alt.
Beweis: mittels Induktion u¨ber den Formelaufbau der Formel ϕ.
Was ist zu zeigen?
Induktionsanfang (IA) – zu zeigen ist:
F¨ur jede aussagenlogische Formel ϕ,
die ⊥, > oder ein Atom ist,
gibt es eine ¨aquivalente Formel ϕ0 , die nur Atome, ⊥ und → enth¨alt.
Fall 1: ϕ = ⊥. Sei ϕ0 = ϕ. Dann gilt ϕ0 ≡ ϕ,
und ϕ0 besteht nur aus Atomen, ⊥ und →.
Fall 2: ϕ = >. Sei ϕ0 = (⊥ → ⊥). Dann gilt ϕ0 ≡ ϕ (Beispiel 3),
und ϕ0 besteht nur aus Atomen, ⊥ und →.
Fall 3: ϕ = Ai . Sei ϕ0 = ϕ. Dann gilt ϕ0 ≡ ϕ, und . . .
1.1.14
Was noch zu zeigen bleibt:
F¨ur alle aussagenlogischen Formeln α und β gilt:
wenn α und β ¨aquivalente Formeln besitzen,
die nur aus Atomen, ⊥ und → bestehen,
dann gibt es auch f¨ur ¬α, (α ∧ β), (α ∨ β) und (α → β)
¨aquivalente Formeln,
die nur aus Atomen, ⊥ und → bestehen.
Daraus wird:
Induktionsvoraussetzung:
α und β besitzen ¨aquivalente Formeln α0 bzw. β 0 ,
die nur aus Atomen, ⊥ und → bestehen.
und
Induktionsschluss – zu zeigen ist:
¬α, (α ∧ β), (α ∨ β) und (α → β) besitzen ¨aquivalente Formeln,
die nur aus Atomen, ⊥ und → bestehen.
Induktionsvoraussetzung (IV):
α und β besitzen ¨aquivalente Formeln α0 bzw. β 0 ,
die nur aus Atomen, ⊥ und → bestehen.
Induktionsschluss (IS) – zu zeigen ist:
¬α, (α ∧ β), (α ∨ β) und (α → β) besitzen ¨aquivalente Formeln,
die nur aus Atomen, ⊥ und → bestehen.
Fall 1: ϕ = ¬α.
Es gilt:
¬α
≡ ¬ α0
(IV und Satz 1.7)
≡ (α0 → ⊥)
(Beispiel 4)
Sei also ϕ0 = (α0 → ⊥). Dann gilt ϕ0 ≡ ϕ,
und in ϕ0 kommen gem¨aß IV nur Atome, ⊥ und → vor.
Fall 2: ϕ = (α ∧ β).
Es gilt: (α ∧ β) ≡
≡
≡
≡
≡
≡
(α0 ∧ β 0 )
(¬¬ α0 ∧ ¬¬ β 0 )
¬(¬ α0 ∨ ¬ β 0 )
((¬ α0 ∨ ¬ β 0 ) → ⊥)
((α0 → ¬ β 0 ) → ⊥)
((α0 → (β 0 → ⊥)) → ⊥)
(IV und Satz 1.7)
(Doppelnegation und Satz 1.7)
(deMorgan’s Regel)
(Beispiel 4)
(Implikation und Satz 1.7)
(Beispiel 4 und Satz 1.7)
Sei also ϕ0 = ((α0 → (β 0 → ⊥)) → ⊥). Dann gilt ϕ0 ≡ ϕ,
und in ϕ0 kommen gem¨aß IV nur Atome, ⊥ und → vor.
Fall 3: ϕ = (α ∨ β).
Es gilt:
(α ∨ β)
≡ (α0 ∨ β 0 )
(IV und Satz 1.7)
≡ (¬¬ α0 ∨ β 0 )
(Doppelnegation und Satz 1.7)
≡ (¬ α0 → β 0 )
(Implikation)
≡ ((α0 → ⊥) → β 0 )
(Beispiel 4 und Satz 1.7)
Sei also ϕ0 = ((α0 → ⊥) → β 0 ). Dann gilt ϕ0 ≡ ϕ,
und in ϕ0 kommen gem¨aß IV nur Atome, ⊥ und → vor.
Fall 4: ϕ = (α → β).
Sei ϕ0 = (α0 → β 0 ). Dann gilt ϕ0 ≡ ϕ (IV und Satz 1.7),
und in ϕ0 kommen gem¨aß IV nur Atome, ⊥ und → vor.
X
Satz 1.9 (Ad¨
aquate Mengen von Verkn¨
upfungszeichen)
F¨ur jede aussagenlogische Formel gibt es ¨aquivalente Formeln, die nur
die folgenden Bestandteile haben.
1. Atome und die Verkn¨upfungszeichen ⊥ und →, oder
2. Atome und die Verkn¨upfungszeichen ¬ und ∧, oder
3. Atome und die Verkn¨upfungszeichen ¬ und ∨, oder
4. Atome und die Verkn¨upfungszeichen ¬ und →.
Anders ausgedr¨uckt:
Eine Menge V von Verkn¨upfungszeichen heißt ad¨aquat,
wenn es zu jeder Formel eine ¨aquivalente Formel gibt, die nur
Verkn¨upfungszeichen aus V besitzt.
{⊥, →}, {¬, ∧}, {¬, ∨} und {¬, →} sind ad¨aquat.
{∧} ist ad¨aquat, wobei B α∧β gdw. B 6 α oder B 6 β.
Semantische Folgerung
Definition 1.10 (Semantische Folgerung)
Formel ϕ ist eine semantische Folgerung aus der Formelmenge Γ
wenn jede Belegung, die Γ erf¨
ullt, ebenfalls ϕ erf¨
ullt.
(D.h.: . . . wenn f¨
ur jede Belegung B gilt: wenn B
Γ, dann B
(Γ
ϕ.)
Schreibweisen:
I Mengenklammern und Vereinigungszeichen l¨
asst man gerne weg:
ϕ oder Γ, α
ϕ.
z.B. schreibt man α1 , . . . , αn
I Statt ∅
ϕ schreibt man
ϕ.
Lemma 1.11 (
verallgemeinert
Sei ϕ eine Formel. Dann gilt:
)
ϕ genau dann, wenn
ϕ.
ϕ),
Lemma 1.12 (Eigenschaften von Pr¨
amissen)
Die folgenden Aussagen sind ¨aquivalent
f¨
ur alle n ∈ N und i = 1, 2, . . . , n + 1.
1. α1 , . . . , αn
ϕ
2. α1 , . . . , αi−1
(αi → (αi+1 → . . . (αn → ϕ) . . .))
3. α1 , . . . , αi−1
(
n
V
αj ) → ϕ
j=i
¨
Insbesondere gelten also folgende Aquivalenzen
zu 1.–3. :
I
I
(α1 → (α2 → . . . (αn → ϕ) . . .))
n
V
(( αi ) → ϕ)
i=1
Zentrale algorithmische Fragen
Entscheidungsprobleme
I
Erf¨ullbarkeit (Satisfiability)
gegeben: Formel ϕ
gefragt: ist ϕ erf¨ullbar ?
I
G¨ultigkeit (Validity, Tautology)
gegeben: Formel ϕ
gefragt: ist ϕ g¨ultig ?
I
Unerf¨ullbarkeit (Unsatisfiability)
gegeben: Formel ϕ
gefragt: ist ϕ unerf¨ullbar ?
1.1.21
Zentrale algorithmische Fragen
Entscheidungsprobleme
I
I
I
Folgerung (Consequence)
gegeben: endl. Formelmenge S, Formel ϕ
gefragt: gilt S
ϕ?
¨
Aquivalenz
(Equivalence)
gegeben: Formeln α und ϕ
gefragt: gilt α ≡ ϕ ?
Formelauswertung (Model checking)
gegeben: Formel ϕ und Belegung B
gefragt: ist B ϕ ?
1.1.22
Reduzierbarkeiten
Beziehungen zwischen den Fragen:
I Folgerung reduziert zu G¨
ultigkeit:
ϕ gdw.
(α1 ∧ . . . ∧ αn ) → ϕ
α1 , . . . , α n
gdw. (α1 ∧ . . . ∧ αn ) → ϕ ist g¨ultig
I
I
G¨ultigkeit reduziert zu Unerf¨ullbarkeit:
ϕ ist g¨ultig gdw. ¬ϕ ist unerf¨ullbar
¨
Unerf¨ullbarkeit reduziert zu Aquivalenz:
ϕ ist unerf¨ullbar gdw. ϕ ≡ ⊥
I
¨
Aquivalenz
reduziert zu Folgerung:
α ≡ ϕ gdw. α ϕ und ϕ α
Diese vier Probleme sind also “gleich schwierig”.
Ein Algorithmus f¨ur eines von ihnen liefert direkt
einen “gleichschnellen” Algorithmus f¨ur die anderen Probleme.
1.1.23
Komplexit¨
at der zentralen Fragen
Formelauswertung
NC1
P
P
PSPACE
Aussagenlogik
Intuitionistische Logik
Modallogik
Temporale Logik LTL
Erf¨
ullbarkeit
NP
NP
PSPACE
PSPACE
G¨
ultigkeit
coNP
PSPACE
PSPACE
PSPACE
NP
NC1
P
PSPACE
coNP
parallel
superschnell
polynomielle Zeit
polynomieller Platz
deterministisch nicht-determ.
langsam
schnell
1.1.24
1.2 Der aussagenlogische Tableau-Kalku
¨l
1. Klassische Aussagenlogik
Grundbegriffe
Tableau-Kalk¨
ul
Tableau-Beweise
Korrektheit
Vollst¨andigkeit
Algorithmen
Frege-Kalk¨
ul
Nat¨
urliches Schließen
Vergleich von Beweis-Kalk¨
ulen
[Literatur:
Priest: An introduction to non-classical logic
Nerode, Shore: Logic for applications]
1.2 Der aussagenlogische Tableau-Kalku
¨l
Ein Beweis-Kalk¨ul liefert ein syntaktisches Verfahren zum Nachweis der
G¨ultigkeit von Formeln.
Die Beweise, die er liefert, sollen korrekt und vollst¨andig sein.
I
korrekt: es k¨onnen nur g¨ultige Formeln bewiesen werden
I
vollst¨andig: alle g¨ultigen Formeln k¨onnen bewiesen werden
Der Tableau-Kalk¨ul ist ein einfacher Beweis-Kalk¨ul, der auf der
Zerlegung von Formeln basiert. Wir werden
I
den Tableau-Kalk¨ul definieren und
I
seine Korrektheit und Vollst¨andigkeit beweisen.
1.2.2
Ein erstes Beispiel
(A ∨ B) ∧ (¬A ∨ ¬B)
Ein (semantisches) Tableau ist ein Baum,
dessen Knoten mit Formeln markiert sind.
Man beginnt mit einem Baum, der nur aus einer Wurzel besteht.
Die Knoten werden expandiert und die Markierungen dabei in ihre
Bestandteile zerlegt “bis auf die Literale”.
Die Expansion ist durch Expansionsregeln bestimmt.
Ein erstes Beispiel
(A ∨ B) ∧ (¬A ∨ ¬B)
Expansionsregeln f¨ur ∧ und ∨:
α∧β :
•
α
β
Ein (semantisches) Tableau ist ein Baum,
dessen Knoten mit Formeln markiert sind.
Man beginnt mit einem Baum, der nur aus einer Wurzel besteht.
Die Knoten werden expandiert und die Markierungen dabei in ihre
Bestandteile zerlegt “bis auf die Literale”.
Die Expansion ist durch Expansionsregeln bestimmt.
Ein erstes Beispiel
(A ∨ B) ∧ (¬A ∨ ¬B)
Expansionsregeln f¨ur ∧ und ∨:
A∨B
α∧β :
•
¬A ∨ ¬B
α
β
Ein (semantisches) Tableau ist ein Baum,
dessen Knoten mit Formeln markiert sind.
Man beginnt mit einem Baum, der nur aus einer Wurzel besteht.
Die Knoten werden expandiert und die Markierungen dabei in ihre
Bestandteile zerlegt “bis auf die Literale”.
Die Expansion ist durch Expansionsregeln bestimmt.
Ein erstes Beispiel
(A ∨ B) ∧ (¬A ∨ ¬B)
Expansionsregeln f¨ur ∧ und ∨:
A∨B
α∧β :
•
¬A ∨ ¬B
α
α∨β :
•
α
β
β
Ein (semantisches) Tableau ist ein Baum,
dessen Knoten mit Formeln markiert sind.
Man beginnt mit einem Baum, der nur aus einer Wurzel besteht.
Die Knoten werden expandiert und die Markierungen dabei in ihre
Bestandteile zerlegt “bis auf die Literale”.
Die Expansion ist durch Expansionsregeln bestimmt.
Ein erstes Beispiel
(A ∨ B) ∧ (¬A ∨ ¬B)
A
Expansionsregeln f¨ur ∧ und ∨:
A∨B
α∧β :
•
¬A ∨ ¬B
α
B
α∨β :
•
α
β
β
Ein (semantisches) Tableau ist ein Baum,
dessen Knoten mit Formeln markiert sind.
Man beginnt mit einem Baum, der nur aus einer Wurzel besteht.
Die Knoten werden expandiert und die Markierungen dabei in ihre
Bestandteile zerlegt “bis auf die Literale”.
Die Expansion ist durch Expansionsregeln bestimmt.
Ein erstes Beispiel
Expansionsregeln f¨ur ∧ und ∨:
(A ∨ B) ∧ (¬A ∨ ¬B)
A∨B
α∧β :
•
¬A ∨ ¬B
α
A
¬A
B
¬B
¬A
α∨β :
•
α
β
β
¬B
Ein (semantisches) Tableau ist ein Baum,
dessen Knoten mit Formeln markiert sind.
Man beginnt mit einem Baum, der nur aus einer Wurzel besteht.
Die Knoten werden expandiert und die Markierungen dabei in ihre
Bestandteile zerlegt “bis auf die Literale”.
Die Expansion ist durch Expansionsregeln bestimmt.
Ein erstes Beispiel
Expansionsregeln f¨ur ∧ und ∨:
(A ∨ B) ∧ (¬A ∨ ¬B)
A∨B
α∧β :
•
¬A ∨ ¬B
α
A
¬A
B
¬B
¬A
α∨β :
•
α
β
β
¬B
Wenn alle Knoten expandiert sind,
dann gibt es f¨
ur jede erf¨
ullende Belegung der Wurzel-Formel einen Pfad,
auf dem die Belegung alle Formeln erf¨
ullt,
und jeder nicht-widerspr¨
uchliche Pfad bestimmt
erf¨
ullende Belegungen der Wurzel-Formel.
Erf¨
ullende Belegungen: {A} und {B}
Ein zweites Beispiel
¬(A ∧ (¬A ∨ B)) wird expandiert zu
¬(A ∧ (¬A ∨ B))
1.2.4
Ein zweites Beispiel
¬(A ∧ (¬A ∨ B)) wird expandiert zu
¬(A ∧ (¬A ∨ B))
Expansionsregeln f¨ur ¬:
¬(α ∧ β) :
•
¬α
¬β
1.2.4
Ein zweites Beispiel
¬(A ∧ (¬A ∨ B)) wird expandiert zu
Expansionsregeln f¨ur ¬:
¬(A ∧ (¬A ∨ B))
¬A
¬(¬A ∨ B)
¬(α ∧ β) :
•
¬α
¬β
1.2.4
Ein zweites Beispiel
¬(A ∧ (¬A ∨ B)) wird expandiert zu
Expansionsregeln f¨ur ¬:
¬(α ∧ β) :
•
¬α
¬β
¬(A ∧ (¬A ∨ B))
¬A
¬(¬A ∨ B)
¬(α ∨ β) :
•
¬α
¬β
1.2.4
Ein zweites Beispiel
¬(A ∧ (¬A ∨ B)) wird expandiert zu
Expansionsregeln f¨ur ¬:
¬(α ∧ β) :
•
¬α
¬β
¬(α ∨ β) :
•
¬α
¬(A ∧ (¬A ∨ B))
¬A
¬(¬A ∨ B)
¬¬A
¬B
¬β
1.2.4
Ein zweites Beispiel
¬(A ∧ (¬A ∨ B)) wird expandiert zu
Expansionsregeln f¨ur ¬:
¬(α ∧ β) :
•
¬α
¬β
¬(A ∧ (¬A ∨ B))
¬A
¬(α ∨ β) :
•
¬¬β :
•
¬α
β
¬(¬A ∨ B)
¬¬A
¬B
¬β
1.2.4
Ein zweites Beispiel
¬(A ∧ (¬A ∨ B)) wird expandiert zu
Expansionsregeln f¨ur ¬:
¬(α ∧ β) :
•
¬α
¬β
¬(A ∧ (¬A ∨ B))
¬A
¬(α ∨ β) :
•
¬¬β :
•
¬α
β
¬β
¬(¬A ∨ B)
¬¬A
¬B
A
Erf¨ullende Belegungen: ∅, {A} und {B}
1.2.4
Ein zweites Beispiel
¬(A ∧ (¬A ∨ B)) wird expandiert zu
Expansionsregeln f¨ur ¬:
¬(α ∧ β) :
•
¬α
¬β
¬(A ∧ (¬A ∨ B))
¬A
¬(α ∨ β) :
•
¬¬β :
•
¬α
β
¬β
¬(¬A ∨ B)
¬¬A
¬B
A
Erf¨ullende Belegungen: ∅, {A} und {B}
Disjunktive Normalform: ¬A ∨ (A ∧ ¬B)
1.2.4
Ein zweites Beispiel
¬(A ∧ (¬A ∨ B)) wird expandiert zu
Expansionsregeln f¨ur ¬:
¬(α ∧ β) :
•
¬α
¬β
¬(A ∧ (¬A ∨ B))
¬A
¬(α ∨ β) :
•
¬¬β :
•
¬α
β
¬β
¬(¬A ∨ B)
¬¬A
¬B
A
Erf¨ullende Belegungen: ∅, {A} und {B}
Disjunktive Normalform: ¬A ∨ (A ∧ ¬B) ≡ ¬A ∨ ¬B
1.2.4
Die Expansionsregeln
Typ 1:
Typ 2:
α∧β :
•
¬(α ∨ β) :
•
¬(α → β) :
•
¬¬α :
•
α
¬α
α
α
β
¬β
¬β
¬(α ∧ β) :
•
¬α
¬β
α∨β :
•
α
α→β:
•
β
¬α
β
Expansion eines Knotens v mit Markierung ϕ in einem Tableau heißt:
f¨
ur jeden Pfad, auf dem v vorkommt:
h¨ange die durch die Expansionsregel f¨
ur ϕ bezeichneten Knoten
an das Ende des Pfades an.
In der Expansionsregel steht • f¨
ur den letzten Knoten im Pfad.
Knoten mit Markier. ⊥, ¬⊥, >, ¬>, Ai und ¬Ai werden nicht expandiert.
1.2.5
Tableaux
Ein Tableau ist ein Baum, dessen Knoten mit Formeln markiert sind.
Er entsteht durch wiederholte Expansion von Knoten.
Definition 1.13 (Tableau)
Sei ϕ eine aussagenlogische Formel.
1. Ein Knoten, der mit ϕ markiert ist, ist ein Tableau f¨ur ϕ.
2. Sei v ein Knoten in einem Tableau f¨ur ϕ,
der expandiert werden kann.
Durch Expansion von v entsteht ein weiteres Tableau f¨ur ϕ.
1.2.6
Systematischer Aufbau eines Tableaus
¬[((A → C ) ∨ (B → C )) → ((A ∨ B) → C )]
1.2.7
Systematischer Aufbau eines Tableaus
¬[((A → C ) ∨ (B → C )) → ((A ∨ B) → C )]
(A → C ) ∨ (B → C )
¬((A ∨ B) → C )
1.2.7
Systematischer Aufbau eines Tableaus
¬[((A → C ) ∨ (B → C )) → ((A ∨ B) → C )]
(A → C ) ∨ (B → C )
¬((A ∨ B) → C )
A→C
B→C
1.2.7
Systematischer Aufbau eines Tableaus
¬[((A → C ) ∨ (B → C )) → ((A ∨ B) → C )]
(A → C ) ∨ (B → C )
¬((A ∨ B) → C )
A→C
B→C
A∨B
A∨B
¬C
¬C
1.2.7
Systematischer Aufbau eines Tableaus
¬[((A → C ) ∨ (B → C )) → ((A ∨ B) → C )]
(A → C ) ∨ (B → C )
¬((A ∨ B) → C )
¬A
A→C
B→C
A∨B
A∨B
¬C
¬C
C
×
1.2.7
Systematischer Aufbau eines Tableaus
¬[((A → C ) ∨ (B → C )) → ((A ∨ B) → C )]
(A → C ) ∨ (B → C )
¬((A ∨ B) → C )
¬A
A
×
A→C
B→C
A∨B
A∨B
¬C
¬C
C
×
B
1.2.7
Systematischer Aufbau eines Tableaus
¬[((A → C ) ∨ (B → C )) → ((A ∨ B) → C )]
(A → C ) ∨ (B → C )
¬((A ∨ B) → C )
¬A
A
×
A→C
B→C
A∨B
A∨B
¬C
¬C
C
×
¬B
C
×
B
1.2.7
Systematischer Aufbau eines Tableaus
¬[((A → C ) ∨ (B → C )) → ((A ∨ B) → C )]
(A → C ) ∨ (B → C )
¬((A ∨ B) → C )
¬A
A
×
A→C
B→C
A∨B
A∨B
¬C
¬C
¬B
C
×
B
A
C
×
B
×
1.2.7
Systematischer Aufbau eines Tableaus
¬[((A → C ) ∨ (B → C )) → ((A ∨ B) → C )]
(A → C ) ∨ (B → C )
¬((A ∨ B) → C )
¬A
A→C
B→C
A∨B
A∨B
¬C
¬C
¬B
C
×
A
B
×
Erf¨
ullende Belegungen: {B} und {A}
A
C
×
B
×
1.2.7
Definition 1.14 (Eigenschaften von Pfaden und Tableaux)
Ein Pfad durch ein Tableau heißt widerspr¨uchlich, wenn
er ⊥, ¬> oder zwei widerspr¨uchliche Formeln α und ¬α enth¨alt.
Ein Tableau heißt geschlossen,
wenn jeder Knoten auf allen nicht-widerspr¨uchlichen Pfaden,
auf denen er liegt, expandiert wurde.
(Widerspr¨
uchliche Pfade m¨
ussen nicht weiter expandiert werden.)
Ein Tableau heißt widerspr¨uchlich,
wenn alle Pfade durch das Tableau widerspr¨uchlich sind.
Lemma 1.15 (endliche Tableaux reichen)
F¨ur jede Formel α gibt es ein geschlossenes Tableau mit ≤ 2|α| Pfaden.
¨
Beweis: Ubungsaufgabe.
1.2.8
Definition 1.16 (Tableau-beweisbar)
Eine Formel α heißt Tableau-beweisbar (Schreibweise: Tab α),
falls ¬α ein widerspr¨uchliches Tableau besitzt.
Beispiel:
Tab
(A → (B → A))
¬(A → (B → A))
A
¬(B → A)
B
¬A
×
1.2.9
Definition 1.16 (Tableau-beweisbar)
Eine Formel α heißt Tableau-beweisbar (Schreibweise: Tab α),
falls ¬α ein widerspr¨uchliches Tableau besitzt.
Beispiel:
Tab
(((A → B) ∧ (B → C )) → (A → C ))
¬(((A → B) ∧ (B → C )) → (A → C ))
(A → B) ∧ (B → C )
¬(A → C )
A→B
B→C
A
¬C
¬A
×
B
¬B
×
C
×
1.2.9
Korrektheit und Vollst¨
andigkeit
Der Tableau-Kalk¨ul unterteilt die Menge aller Formeln
in beweisbare und nicht-beweisbare Formeln.
Sind die Tableau-beweisbaren Formeln genau die g¨ultigen Formeln?
Diese Frage besteht aus zwei Teilen:
1) Ist jede Tableau-beweisbare Formel g¨ultig? (Korrektheit des TK)
2) Ist jede g¨ultige Formel Tableau-beweisbar? (Vollst¨andigkeit des TK)
Zur Beantwortung der Frage braucht man einen Zusammenhang
zwischen Tableaux und Belegungen.
Definition 1.17 (ein Erf¨
ullungsbegriff f¨
ur Pfade)
Sei A eine Belegung. Ein Pfad durch ein Tableau heißt A-treu,
wenn A jede Formel auf dem Pfad erf¨ullt.
1.2.10
Bsp: Ein Tableau mit einem {B}-treuen Pfad
¬[((A → C ) ∨ (B → C )) → ((A ∨ B) → C )]
(A → C ) ∨ (B → C )
¬((A ∨ B) → C )
A→C
B→C
A∨B
A∨B
¬C
¬C
¬A
A
×
¬B
C
×
B
A
C
×
B
×
Wir werden zwei Eigenschaften A-treuer Pfade beweisen:
1.) Wenn ein Tableau einen A-treuen Pfad hat,
dann beh¨alt es auch einen nach der Expansion eines Knotens.
1.2.11
Bsp: Ein Tableau mit einem {B}-treuen Pfad
¬[((A → C ) ∨ (B → C )) → ((A ∨ B) → C )]
(A → C ) ∨ (B → C )
¬((A ∨ B) → C )
A→C
B→C
A∨B
A∨B
¬C
¬C
¬A
A
×
¬B
C
×
B
A
C
×
B
×
Wir werden zwei Eigenschaften A-treuer Pfade beweisen:
2.) Wenn ein geschlossenes Tab. einen nicht-widerspr¨uchlichen Pfad hat,
dann gibt es eine Belegung A, zu der er A-treu ist.
1.2.11
Zur Korrektheit . . .
Man betrachtet eine Belegung A, die die Wurzel eines Tableaus erf¨ullt,
und verfolgt die Entwicklung eines A-treuen Pfades beim Aufbau
des Tableaus.
Wenn auf einem A-treuen Pfad ein Knoten expandiert wird,
dann wird der A-treue Pfad verl¨angert.
Lemma 1.18 (Expansion erh¨
alt A-Treue)
Sei ϕ eine Formel mit B ϕ.
Dann besitzt jedes Tableau f¨ur ϕ einen B-treuen Pfad.
Beweis: mittels Induktion u¨ber den Aufbau eines Tableaus f¨ur ϕ.
1.2.12
IA: Das Tableau T besteht aus einem mit ϕ markierten Knoten p1 .
Dann ist dieser Knoten der einzige Pfad durch T , und er ist B-treu.
IV: Ein bel. festes Tableau T f¨ur ϕ besitzt einen B-treuen Pfad.
IS: T 0 entsteht aus T durch Expansion eines Knotens.
Sei π = p1 , p2 , . . . , pk ein B-treuer Pfad durch das Tableau T .
Fall 1: T 0 entsteht aus T durch Expansion eines Knotens,
der nicht auf π liegt.
Dann ist π ein B-treuer Pfad durch T 0 .
Fall 2: T 0 entsteht aus T durch Expansion eines Knotens pi auf π.
Es werden alle m¨oglichen Expansionen betrachtet.
1.2.13
Wir beginnen mit den Expansionen vom Typ 1.
Fall 2.1: pi = α ∧ β.
α∧β :
•
α
β
Dann ist π 0 = p1 , p2 , . . . , pk , α, β ein Pfad durch T 0 .
Laut Voraussetzung erf¨ullt B die Formeln p1 , . . . , pk .
Da B α ∧ β, folgt B α und B β (Semantik von ∧).
Also ist π 0 ein B-treuer Pfad durch T 0 .
Fall 2.2: pi = ¬(α ∨ β) – ¨ahnlich wie Fall 2.1
Fall 2.3: pi = ¬(α → β) – ¨ahnlich wie Fall 2.1.
Fall 2.4: pi = ¬¬α – ¨ahnlich wie Fall 2.1.
1.2.14
Es folgen die Expansionen vom Typ 2.
Fall 2.5: pi = α ∨ β.
Dann sind π10 = p1 , p2 , . . . , pk , α und
π20 = p1 , p2 , . . . , pk , β Pfade durch T 0 .
α∨β :
Laut Voraussetzung erf¨ullt B die Formeln p1 , . . . , pk .
•
Da B α ∨ β, folgt B α oder B β (Semantik von ∨).
α
β
Also ist π10 ein B-treuer Pfad durch T 0
oder π20 ist ein B-treuer Pfad durch T 0 .
Fall 2.6: pi = ¬(α ∧ β) – ¨ahnlich wie Fall 2.5.
Fall 2.7: pi = (α → β) – ¨ahnlich wie Fall 2.5.
X
Lemma 1.19 (Korrektheit des Tableau-Kalk¨
uls)
Wenn
Tab
α, dann
α.
Beweis: wir zeigen die Kontraposition:
wenn α nicht g¨
ultig ist, dann ist α nicht Tableau-beweisbar,
d.h. wenn ¬α erf¨
ullbar ist, dann ist α nicht Tableau-beweisbar.
Sei ¬α erf¨
ullbar.
Dann gibt es eine Belegung B mit B ¬α.
Gem¨aß Lemma 1.18 hat jedes Tableau f¨
ur ¬α einen B-treuen Pfad.
Kein B-treuer Pfad ist widerspr¨
uchlich.
Also besitzt jedes Tableau f¨
ur ¬α einen nicht-widerspr¨
uchlichen Pfad.
Folglich gibt es kein widerspr¨
uchliches Tableau f¨
ur ¬α.
D.h. α ist nicht Tableau-beweisbar.
X
1.2.16
Zur Vollst¨
andigkeit . . .
Man betrachtet die Belegung A,
die die Atome auf einem nicht-widerspr¨
uchlichen Pfad π bilden,
und zeigt, dass der Pfad π A-treu ist.
Lemma 1.20 (Pfad bestimmt Belegung)
Sei T ein Tableau und π ein nicht-widerspr¨uchlicher Pfad durch T ,
auf dem jeder Knoten expandiert ist.
Dann gibt es eine Belegung A, so dass π A-treu ist.
Beweis:
Sei π = p1 , p2 , . . . , pm ein solcher Pfad (wir fassen die pi als Formeln auf).
Sei Aπ die Belegung, die genau aus den Atomen auf dem Pfad besteht.
Wir zeigen induktiv, dass Aπ pi f¨
ur i = m, m − 1, . . . , 1.
IA: zu zeigen: Aπ
pm .
Da (1) pm = Ai mit Ai ∈ Aπ ,
oder (2) pm = ¬Ai mit Ai 6∈ Aπ
oder (3) pm = > oder pm = ¬⊥,
folgt Aπ pm .
IV: Aπ
pj , Aπ
pj+1 , . . . , Aπ
(da π nicht widerspr¨
uchlich ist)
pm (f¨
ur ein bel. festes j > 1)
1.2.18
IS: zu zeigen: Aπ pj−1 .
Es muss nachgeschaut werden, wie pj−1 aussieht.
Fall 1: pj−1 ist ein Literal oder pj−1 = > oder pj−1 = ¬⊥.
Dann gilt Aπ pj−1 wie bereits im IA gezeigt.
Fall 2: pj−1 = α ∧ β.
α∧β :
Da jeder Knoten auf π expandiert ist,
•
gibt es i ≥ j mit pi = α und pi+1 = β.
α
Da Aπ α und Aπ β (gem¨aß IV),
folgt Aπ α ∧ β (gem¨aß der Semantik von ∧).
β
Fall 6: pj−1 = ¬(α ∧ β).
Dann gibt es i ≥ j mit pi = ¬α oder pi = ¬β.
¬(α ∧ β) :
Da Aπ pi (IV), folgt Aπ ¬α ∨ ¬β (Semantik von ∨),
•
und mit ¬α ∨ ¬β ≡ ¬(α ∧ β)
¬α
¬β erhalten wir Aπ ¬(α ∧ β).
Die u
¨brigen F¨alle gehen entsprechend.
X
1.2.19
Lemma 1.21 (Vollst¨
andigkeit des Tableau-Kalk¨
uls)
Wenn
α, dann
Tab
α.
Beweis: Wir zeigen die Kontraposition.
Sei α nicht Tableau-beweisbar.
Dann gibt es f¨ur ¬α ein geschlossenes Tableau T¬α (Lemma 1.15),
das nicht widerspr¨uchlich ist.
Also gibt es einen nicht-widerspr¨uchlichen Pfad π durch T¬α ,
auf dem jeder Knoten expandiert ist.
Nach Lemma 1.20 gibt es eine Belegung, die jede Formel auf π erf¨ullt.
Da ¬α am Anfang von π steht, ist ¬α erf¨ullbar.
D.h. α ist nicht g¨ultig.
X
1.2.20
Vollst¨
andigkeitssatz fu
¨r den Tableau-Kalku
¨l
Satz 1.22 (Vollst¨
andigkeitssatz f¨
ur den Tableau-Kalk¨
ul)
Sei α eine aussagenlogische Formel.
α ist g¨ultig genau dann, wenn α Tableau-beweisbar ist,
d.h.
α genau dann, wenn Tab α.
Beweis: folgt aus Lemmas 1.19 und 1.21.
I
“G¨ultigkeit” ist u¨ber Belegungen definiert: semantisch.
I
“Tableau-Beweisbarkeit” ist u¨ber Formeln definiert: syntaktisch.
1.3 Algorithmen aus dem Tableau-Kalku
¨l
Aus dem Beweis des Vollst¨andigkeitssatzes f¨ur den aussagenlogischen
Tableau-Kalk¨ul ergibt sich:
Folgerung 1.23
Sei α eine aussagenlogische Formel.
α ist erf¨ullbar genau dann, wenn es ein geschlossenes Tableau f¨ur α
gibt, das einen nicht-widerspr¨uchlichen Pfad hat.
Wir betrachten im Folgenden Erf¨ullbarkeitstests.
Erinnerung: α ist erf¨ullbar gdw. ¬α ist nicht g¨ultig.
Algorithmische Umsetzung des Tableau-Aufbaus
Pfade werden durch Mengen von Formeln, die auf ihnen noch nicht expandiert
wurden, dargestellt.
¬[((A → C ) ∨ (B → C )) → ((A ∨ B) → C )]
(A → C ) ∨ (B → C )
¬((A ∨ B) → C )
A→C
B→C
A∨B
A∨B
¬C
¬C
¬A
A
×
¬B
C
×
B
A
C
×
B
×
1.3.23
Algorithmische Umsetzung des Tableau-Aufbaus
Pfade werden durch Mengen von Formeln, die auf ihnen noch nicht expandiert
wurden, dargestellt.
{¬[((A → C ) ∨ (B → C )) → ((A ∨ B) → C )]}
(A → C ) ∨ (B → C )
¬((A ∨ B) → C )
A→C
B→C
A∨B
A∨B
¬C
¬C
¬A
A
×
¬B
C
×
B
A
C
×
B
×
1.3.23
Algorithmische Umsetzung des Tableau-Aufbaus
Pfade werden durch Mengen von Formeln, die auf ihnen noch nicht expandiert
wurden, dargestellt.
{¬[((A → C ) ∨ (B → C )) → ((A ∨ B) → C )]}
{(A → C ) ∨ (B → C ), ¬((A ∨ B) → C )}
A→C
B→C
A∨B
A∨B
¬C
¬C
¬A
A
×
¬B
C
×
B
A
C
×
B
×
1.3.23
Algorithmische Umsetzung des Tableau-Aufbaus
Pfade werden durch Mengen von Formeln, die auf ihnen noch nicht expandiert
wurden, dargestellt.
{(A → C ) ∨ (B → C ), ¬((A ∨ B) → C )}
A→C
B→C
A∨B
A∨B
¬C
¬C
¬A
A
×
¬B
C
×
B
A
C
×
B
×
1.3.23
Algorithmische Umsetzung des Tableau-Aufbaus
Pfade werden durch Mengen von Formeln, die auf ihnen noch nicht expandiert
wurden, dargestellt.
{(A → C ) ∨ (B → C ), ¬((A ∨ B) → C )}
{A → C , ¬((A ∨ B) → C )}
B→C
A∨B
A∨B
¬C
¬C
¬A
A
×
¬B
C
×
B
A
C
×
B
×
1.3.23
Algorithmische Umsetzung des Tableau-Aufbaus
Pfade werden durch Mengen von Formeln, die auf ihnen noch nicht expandiert
wurden, dargestellt.
{A → C , ¬((A ∨ B) → C )}
B→C
A∨B
A∨B
¬C
¬C
¬A
A
×
¬B
C
×
B
A
C
×
B
×
1.3.23
Algorithmische Umsetzung des Tableau-Aufbaus
Pfade werden durch Mengen von Formeln, die auf ihnen noch nicht expandiert
wurden, dargestellt.
{A → C , ¬((A ∨ B) → C )}
B→C
A∨B
{A → C , A ∨ B, ¬C }
¬A
A
×
¬C
¬B
C
×
B
A
C
×
B
×
1.3.23
Algorithmische Umsetzung des Tableau-Aufbaus
Pfade werden durch Mengen von Formeln, die auf ihnen noch nicht expandiert
wurden, dargestellt.
B→C
A∨B
{A → C , A ∨ B, ¬C }
¬A
A
×
¬C
¬B
C
×
B
A
C
×
B
×
1.3.23
Algorithmische Umsetzung des Tableau-Aufbaus
Pfade werden durch Mengen von Formeln, die auf ihnen noch nicht expandiert
wurden, dargestellt.
B→C
A∨B
{A → C , A ∨ B, ¬C }
{¬A, A ∨ B, ¬C }
A
×
B
¬C
¬B
C
×
A
C
×
B
×
1.3.23
Algorithmische Umsetzung des Tableau-Aufbaus
Pfade werden durch Mengen von Formeln, die auf ihnen noch nicht expandiert
wurden, dargestellt.
B→C
A∨B
¬C
{¬A, A ∨ B, ¬C }
A
×
B
¬B
C
×
A
C
×
B
×
1.3.23
Algorithmische Umsetzung des Tableau-Aufbaus
Pfade werden durch Mengen von Formeln, die auf ihnen noch nicht expandiert
wurden, dargestellt.
B→C
A∨B
¬C
{¬A, A ∨ B, ¬C }
A
×
{¬A, B, ¬C }
¬B
C
×
A
C
×
B
×
1.3.23
Algorithmische Umsetzung des Tableau-Aufbaus
Pfade werden durch Mengen von Formeln, die auf ihnen noch nicht expandiert
wurden, dargestellt.
B→C
A∨B
¬C
¬B
C
×
A
×
{¬A, B, ¬C }
A
C
×
B
×
1.3.23
Typen von Tableau-Knoten
In Tableaux f¨ur Aussagenlogik gibt es zwei Typen von Regeln.
Typ 1: Markierung α ∧ β, ¬(α ∨ β), ¬(α → β), ¬¬α:
es werden Knoten mit allen Zerlegungsformeln
angeh¨angt
•
α
α ∧ β hat Zerlegungsformeln α und β,
β
¬(α ∨ β) hat Zerlegungsformeln ¬α und ¬β etc.
•
α
β
Typ 2: Markierung α ∨ β, α → β, ¬(α ∧ β):
es wird zu zwei Knoten mit jeweils einer
Zerlegungsformel verzweigt
Algorithmische Umsetzung
Wenn man Pfade durch Mengen zu zerlegender Formeln ausdr¨uckt,
dann hat ein Expansionsschritt folgende Wirkung:
I
f¨ur eine Formel vom Typ 1 (α ∧ β, ¬(α ∨ β), ¬(α → β), ¬¬α):
ersetze sie durch alle ihre Zerlegungsformeln;
z.B wenn α ∧ β ∈ S, dann wird S := (S − {α ∧ β}) ∪ {α, β}
I
f¨ur eine Formel vom Typ 2 (α ∨ β, α → β, ¬(α ∧ β)):
ersetze sie nichtdeterministisch nur durch eine ihrer
Zerlegungsformeln;
z.B. wenn α ∨ β ∈ S, dann entscheide nichtdeterministisch,
ob mit S := (S − {α ∨ β}) ∪ {α}
oder mit S := (S − {α ∨ β}) ∪ {β} weitergemacht wird.
. . . aus Verzweigung im Tableau wird Nichtdeterminismus . . .
1.3.25
Methode zum Bestimmen der
Zerlegungsformeln
Methodenaufruf zerlege(ϕ,i) ergibt die i-te Zerlegungsformel von ϕ.
Methode zerlege (Formel ϕ, Index i)
falls i = 1 dann
(∗ bestimme die erste Zerlegungsformel ∗)
falls ϕ ∈ {α ∧ β, α ∨ β, ¬(α → β), ¬¬α} dann return α
falls ϕ ∈ {¬(α ∧ β), ¬(α ∨ β), α → β} dann return ¬α
sonst
(∗ bestimme die zweite Zerlegungsformel ∗)
falls ϕ ∈ {α ∧ β, α ∨ β, α → β} dann return β
falls ϕ ∈ {¬(α ∧ β), ¬(α ∨ β), ¬(α → β)} dann return ¬β
Erfu
aß Tableau-Kalku
¨llbarkeitstest gem¨
¨l
f¨
ur aussagenlogische Formeln als nichtdeterministischer Algorithmus
Eingabe ϕ
S := {ϕ}
(∗ ϕ ist eine aussagenlogische Formel ∗)
solange S eine Formel vom Typ 1 oder 2 enth¨alt
und nicht widerspr¨
uchlich ist wiederhole
{
falls S eine Formel ψ vom Typ 1 enth¨alt dann
(∗ ersetze ψ durch alle ihre Zerlegungsformeln ∗)
S := (S − ψ) ∪ {zerlege(ψ, 1), zerlege(ψ, 2)}
sonst sei ψ eine Formel vom Typ 2 in S
(∗ ersetze ψ durch eine ihrer Zerlegungsformel, die nichtdeterministisch gew¨
ahlt wurde ∗)
w¨ahle nichtdeterministisch b ∈ {1, 2}
S := (S − ψ) ∪ {zerlege(ψ, b)}
}
(∗ S ist widerspr¨
uchlich oder enth¨
alt nur noch Literale ∗)
falls S nicht widerspr¨
uchlich ist
dann akzeptiere
sonst verwirf
(∗ S ist erf¨
ullende Belegung von ϕ ∗)
Grobe Analyse des Tableau-Algorithmus
f¨
ur Aussagenlogik
Der Algorithmus simuliert das Tableau-Verfahren.
Jeder (nichtdeterministische) Berechnungspfad
entspricht einem Pfad durch das Tableau.
Die Menge S enth¨alt stets die Knoten-Markierungen auf dem Pfad,
die noch nicht zerlegt wurden.
Da jede Formel der L¨ange n h¨ochstens 2n Teilformeln besitzt,
l¨auft der nichtdeterministische Algorithmus in polynomieller Zeit.
Aufgrund der Korrektheit und Vollst¨andigkeit des Tableau-Kalk¨uls
zeigt der Algorithmus,
dass das Erf¨ullbarkeitsproblem der Aussagenlogik in NP ist.
Entspechend ist das G¨ultigkeitsproblem der Aussagenlogik in coNP.
1.3.28
Jedes Tableau bestimmt einen Formelmengenbaum
{¬[((A → C ) ∨ (B → C )) → ((A ∨ B) → C )]}
{(A → C ) ∨ (B → C ), ¬((A ∨ B) → C )}
{A → C , ¬((A ∨ B) → C )}
{B → C , ¬((A ∨ B) → C )}
{A → C , A ∨ B, ¬C }
{B → C , A ∨ B, ¬C }
{¬A, A ∨ B, ¬C }
{C , A ∨ B, ¬C } {¬B, A ∨ B, ¬C } {C , A ∨ B, ¬C }
×
×
{¬A, A, ¬C } {¬A, B, ¬C }
{¬B, A, ¬C } {¬B, B, ¬C }
×
×
Jede Menge repr¨asentiert einen Pr¨afix eines Pfades durch das Tableau.
1.3.29
Erfu
aß Tableau-Kalku
¨llbarkeitstest gem¨
¨l
f¨
ur aussagenlogische Formeln als rekursive Methode
mittels Tiefensuche durch den Formelmengenbaum
Methode suche(Formelmenge S) {
falls S widerspr¨
uchlich ist dann return 0
falls S eine Formel ψ vom Typ 1 enth¨alt
(∗ S ist widerspr¨
uchlich ∗)
(∗ ersetze ψ durch alle ihre Zerlegungsformeln ∗)
return suche((S − ψ) ∪ {zerlege(ψ, 1), zerlege(ψ, 2)})
sonst: falls S eine Formel ψ vom Typ 2 enth¨alt
(∗ ersetze ψ durch eine ihrer Zerlegungsformel, die nichtdet. gew¨
ahlt wurde ∗)
return max suche((S − ψ) ∪ {zerlege(ψ, b)})
b∈{1,2}
sonst: (∗ S ist nicht widerspr¨uchlich und enth¨alt nur noch Literale ∗)
return 1
(∗ S ist erf¨
ullende Belegung von ϕ ∗)
}
Hauptprogramm
(liefert Ergebnis 1, falls ϕ erf¨
ullbar ist, und Erg. 0 sonst)
Eingabe Formel ϕ
Ausgabe suche({ϕ})
1.3.30
1.4 Ein klassischer Beweis-Kalku
¨l:
der Frege-Kalku
¨l
1. Klassische Aussagenlogik
Grundbegriffe
Tableau-Kalk¨
ul
Algorithmen
Frege-Kalk¨
ul
Axiome, Regeln und Beweise
Das Deduktionstheorem
Korrektheit
Vollst¨andigkeit
¨
Ahnliche
Theorien
Nat¨
urliches Schließen
Vergleich von Beweis-Kalk¨
ulen
[Literatur: Mendelson: Introduction to Mathematical Logic]
1.4.1
Gottlob Frege (1848-1925) war Professor in Jena und gilt als
Gr¨undungsvater der formalen Logik.
Der (nach ihm benannte) Frege-Kalk¨ul ist ein Beweis-Kalk¨ul, der auf
dem strukturellen Aufbau von Formeln basiert. Wir werden
I
den Frege-Kalk¨ul definieren und
I
seine Korrektheit und Vollst¨andigkeit beweisen.
1.4.2
Ein Frege-Kalku
¨l
Der Frege-Kalk¨ul dient zur Herleitung von Formeln aus Axiomen.
1. Die Elemente des Frege-Kalk¨uls sind
die aussagenlogischen Formeln aus Atomen, ⊥ und →
(¬α ist abk¨
urzende Schreibweise f¨
ur α → ⊥; > ist Abk¨
urzung f¨
ur ¬⊥).
2. Die Axiome Ax des Frege-Kalk¨uls sind f¨ur alle Formeln α, β, ϕ:
(A1) α → (β → α)
(A2) (α → (β → ϕ)) → ((α → β) → (α → ϕ))
(A3) ((¬β) → (¬α)) → (((¬β) → α) → β)
3. Die einzige Schlussregel des Frege-Kalk¨uls ist modus ponens (MP):
aus α und α → β kann man in einem Schritt β herleiten.
α
α→β
.
Das wird auch beschrieben durch
β
1.4.3
4. Eine Herleitung einer Formel α im Frege-Kalk¨ul ist eine Folge
α1 , α2 , . . . , α` von Formeln, an deren Ende α(= α` ) steht und
deren Elemente folgende Eigenschaften haben (f¨ur i = 1, 2, . . . , `):
I
I
αi ist ein Axiom, oder
es gibt αa , αb mit a, b < i, aus denen αi in einem Schritt mit
modus ponens hergeleitet werden kann
(d.h. es gibt a, b < i mit αb = αa → αi ).
(Statt Herleitung verwendet man gerne auch Beweis.)
5. Formel α ist ein Theorem des Frege-Kalk¨uls (Schreibweise:
wenn es eine Herleitung von α im Frege-Kalk¨ul gibt.
Fre
α),
1.4.4
Ein Beweis fu
¨r B → B im Frege-Kalku
¨l
α1 =
B → ( (B → B) → B )
Axiom (A1)
α2 = ( B → ( (B → B) → B )) → (( B → (B → B) ) → ( B → B ))
Axiom (A2)
α3 = (B → (B → B)) → (B → B) MP mit α1 und α2
α4 =
B →(B → B )
α5 = B → B
Axiom (A1)
MP mit α4 und α3
Nimmt man statt B eine beliebige Formel β,
dann hat man einen Beweis f¨
ur β → β f¨
ur alle β.
Also: f¨
ur alle Formeln β gilt: Fre β → β.
1.4.5
Lemma 1.24
Fre
β → β, f¨ur jede Formel β.
Beweis:
Wir zeigen, dass β → β im Frege-Kalk¨ul herleitbar ist.
(1)
(2)
(3)
(4)
(5)
β → ((β → β) → β)
(A1)
(β → ((β → β) → β)) → ((β → (β → β)) → (β → β)) (A2)
(β → (β → β)) → (β → β) MP (1), (2)
β → (β → β)
(A1)
β→β
MP (4), (3)
X
1.4.6
Beweise mit Hypothesen
Sei Γ eine Menge von Formeln.
Γ Fre α bedeutet “α ist in Fre beweisbar, wenn Formeln aus Γ wie
Axiome benutzt werden k¨onnen”
Lemma 1.25 (TRANS)
{α → β, β → γ}
Fre
α → γ, f¨ur alle Formeln α, β, γ.
Beweis:
(1) β → γ
(2) (β → γ) → (α → (β → γ))
(3) α → (β → γ)
(4) (α → (β → γ)) → ((α → β) → (α → γ))
(5) (α → β) → (α → γ)
(6) α → β
(7) α → γ
Hypothese
(A1)
MP (1), (2)
(A2)
MP (3), (4)
Hypothese
MP (6), (5)
X
1.4.7
Das Deduktionstheorem
Satz 1.26 (DT)
Sei Γ eine Menge von Formeln, α und β seien Formeln.
Dann gilt: Γ ∪ {α} Fre β genau dann, wenn Γ Fre α → β.
Beweis:
⇐: Sei Γ Fre α → β.
Dann gibt es folgenden Beweis mit Hypothesen aus Γ ∪ {α}.
)
(1)
...
..
..
hier steht der Beweis f¨ur Γ Fre α → β
.
.
(k)
α→β
(k + 1) α
Hypothese
(k + 2) β
MP (k + 1), (k)
Damit folgt Γ ∪ {α}
Fre
β.
⇒: Wir f¨uhren einen Induktionsbeweis u¨ber die L¨ange `
eines Beweises α1 , . . . , α` von β aus Γ ∪ {α}.
IA ` = 1: dann ist β ∈ Ax ∪ Γ ∪ {α}.
Zu zeigen ist nun: Γ
Fre
α → β.
Fall 1: β ∈ Ax ∪ Γ: (1) β
Hyp. aus Γ oder Axiom
(2) β → (α → β) (A1)
(3) α → β
MP (1),(2)
Also folgt Γ Fre α → β.
Fall 2: β = α: es gilt Fre β → β f¨ur jede Formel β (Lemma 1.24).
Also gilt auch Γ Fre β → β, d.h. hier Γ Fre α → β.
Das sind alle M¨oglichkeiten f¨ur β, und stets folgt Γ
Fre
α → β.
1.4.9
IV: die Behauptung gilt f¨ur Beweise der L¨ange ` ≤ k.
D.h. wenn es einen Beweis von β mit ` ≤ k Schritten aus Γ ∪ {α} gibt,
dann folgt Γ Fre α → β.
IS ` = k + 1: α1 , . . . , αk+1 sei Beweis von β
Zu zeigen ist: es gilt Γ
Fre
(= αk+1 )
aus Γ ∪ {α}.
α → β.
Fall 1: β ∈ Ax ∪ Γ ∪ {α}. Dann folgt Γ
Fre
α → β wie im IA.
1.4.10
Fall 2: β entsteht mit MP aus αi und αj (i, j ≤ k).
Dann ist αj = αi → β.
Nach IV gilt Γ Fre α → (αi → β) und Γ
Folgender Beweis zeigt Γ Fre α → β.
(1)
..
.
(s)
(s + 1)
..
.
(m)
...
..
.
α → αi
α → αi .
)
Beweis f¨ur
Γ Fre α → (αi → β) gem¨aß IV
)
Beweis f¨ur
Γ Fre α → αi gem¨aß IV
α → (αi → β)
...
..
.
Fre
(m + 1) (α → (αi → β)) → ((α → αi ) → (α → β)) (A2)
(m + 2) (α → αi ) → (α → β) MP (s), (m + 1)
(m + 3) α → β
MP (m), (m + 2)
X
1.4.11
Bsp.: Anwendung des Deduktionstheorems
zur Vereinfachung von Beweisen
Lemma 1.27 (ex falso quod libet)
Fre
¬α → (α → β),
f¨ur alle Formeln α und β.
Beweis: zuerst zeigen wir {α, ¬α}
(1)
(2)
(3)
(4)
(5)
(6)
(7)
(8)
Fre
α
α → (¬β → α)
¬β → α
¬α
¬α → (¬β → ¬α)
¬β → ¬α
(¬β → ¬α) → ((¬β → α) → β)
β
β.
Hyp
(A1)
MP (1),(2)
Hyp
(A1)
MP (4),(5)
(A3)
2mal MP auf (7) mit (6) und (5)
Damit ist {α, ¬α} Fre β bewiesen.
Mit einer Anwendung des Deduktionstheorems 1.26 erh¨alt man {¬α}
und mit einer weiteren Anwendung von DT schließlich
Fre
Fre
α → β,
¬α → (α → β).
X
1.4.12
Bsp.:Anwendung des Deduktionstheorems
Vereinfachte Schreibweise f¨ur Hypothesenmengen:
Mengenklammern und ∪ weglassen . . .
Lemma 1.28 (MID)
α → (β → γ), β
Fre
α → γ,
f¨ur alle Formeln α, β, γ.
Beweis:
Wir beginnen mit einem einzeiligen Beweis.
(1) α → (β → γ)
Hypothese
Das beweist
α → (β → γ)
α → (β → γ).
Fre
Mit DT (1.26) folgt
α → (β → γ), α
β → γ,
Fre
und daraus folgt erneut mit DT α → (β → γ), α, β Fre γ.
Mit einer weiteren Anwendung von DT erhalten wir schließlich
α → (β → γ), β
α → γ.
X
Fre
Weitere Vereinfachungen von Beweisen
Bewiesene Formeln (Theoreme) k¨onnen in Beweisen benutzt werden.
Mit Hypothesen bewiesene Formeln k¨onnen wie Regeln benutzt werden.
Lemma 1.29
Fre
¬¬β → β,
f¨ur alle Formeln β.
Beweis:
(1) (¬β → ¬¬β) → ((¬β → ¬β) → β)
(2) ¬β → ¬β
(3) (¬β → ¬¬β) → β
(4) ¬¬β → (¬β → ¬¬β)
(5) ¬¬β → β
(A3)
Lemma 1.24
Lemma 1.28 MID (1),(2)
(A1)
Lemma 1.25 TRANS (4), (3)
X
1.4.14
Folgerung 1.30
Fre
⊥→α
f¨ur alle Formeln α.
Beweis:
(1) (⊥ → ⊥) → (⊥ → β) Lemma 1.27
(2) ⊥ → ⊥
Lemma 1.24
(3) ⊥ → β
MP (2),(1)
1.4.15
Verallgemeinerung von TRANS
Lemma 1.31
F¨
ur k ≥ 1 und alle Formeln α1 , . . . , αk , β, γ gilt
α1 → (α2 → (. . . → (αk → β) . . .)), β → γ Fre α1 → (α2 → (. . . → (αk → γ) . . .))
Beweis mittels Induktion u
¨ber k.
IA k = 1: f¨
ur k = 1 ist die Behauptung gleich TRANS (Lemma 1.25).
IV: die Behauptung gilt f¨
ur k.
=:ψ
z
}|
{
IS: zu zeigen: α1 → (α2 → (. . . → (αk+1 → β) . . .)), β → γ Fre
α1 → (α2 → (. . . → (αk+1 → γ) . . .))
(1)
(2)
(3)
(4)
(5)
ψ, β → γ
ψ, β → γ
ψ, β → γ, α1
ψ, β → γ, α1
ψ, β → γ
Fre
Fre
Fre
Fre
Fre
β →γ
α1 → (α2 → (. . . → (αk+1 → β) . . .))
α2 → (. . . → (αk+1 → β) . . .)
α2 → (. . . → (αk+1 → γ) . . .)
α1 → (α2 → (. . . → (αk+1 → γ) . . .))
Hyp
Hyp
DT
IV (3),(1)
DT
X
1.4.16
“Wichtige” Theoreme von Fre
Satz 1.32
F¨ur alle Formeln α, β, γ gilt:
1.
Fre
α→α
(Lemma 1.24)
2.
Fre
¬¬α → α
(Lemma 1.29)
3.
Fre
α → ¬¬α
4.
Fre
¬α → (α → β)
5.
Fre
(¬β → ¬α) → (α → β)
6.
Fre
(α → β) → (¬β → ¬α)
7.
Fre
α → (¬β → (¬(α → β)))
8.
Fre
(α → β) → ((¬α → β) → β)
(Lemma 1.27)
(3)
(1)
(2)
(3)
(4)
(5)
Fre
α → ¬¬α
(¬¬¬α → ¬α) → ((¬¬¬α → α) → ¬¬α) (A3)
¬¬¬α → ¬α
Satz 1.32(2)
(¬¬¬α → α) → ¬¬α
MP (1),(2)
α → (¬¬¬α → α)
(A1)
α → ¬¬α
TRANS (4),(3)
1.4.18
(5)
(1)
(2)
(3)
(4)
(5)
(6)
Fre
(¬β → ¬α) → (α → β)
¬β → ¬α
(¬β → ¬α) → ((¬β → α) → β)
(¬β → α) → β
α → (¬β → α)
α→β
(¬β → ¬α) → (α → β)
Hyp
(A3)
MP (1),(2)
(A1)
TRANS (4),(3)
DT Hyp (1),(5)
(6)
(1)
(2)
(3)
(4)
(5)
(6)
(7)
(8)
Fre
(α → β) → (¬β → ¬α)
α→β
¬¬α → α
¬¬α → β
β → ¬¬β
¬¬α → ¬¬β
(¬¬α → ¬¬β) → (¬β → ¬α)
¬β → ¬α
(α → β) → (¬β → ¬α)
Hyp
Satz 1.32(2)
TRANS (2),(1)
Satz 1.32(3)
TRANS (3),(4)
Satz 1.32(5)
MP (5),(6)
DT Hyp (1), (7)
1.4.20
(7)
Fre
(i) α, α → β
α → (¬β → ¬(α → β))
Fre
β
gilt offensichtlich
(ii)
Fre
α → ((α → β) → β)
(iii)
Fre
((α → β) → β) → (¬β → ¬(α → β))
(iv)
Fre
α → (¬β → ¬(α → β))
folgt aus (i) mit DT (2mal)
Satz 1.32(6)
folgt aus (ii) und (iii) mit TRANS
1.4.21
(8)
(1)
(2)
(3)
(4)
(5)
(6)
(7)
(8)
(9)
(10)
(11)
Fre
(α → β) → ((¬α → β) → β)
α→β
¬α → β
(α → β) → (¬β → ¬α)
¬β → ¬α
(¬α → β) → (¬β → ¬¬α)
¬β → ¬¬α
(¬β → ¬¬α) → ((¬β → ¬α) → β)
(¬β → ¬α) → β
β
(¬α → β) → β
(α → β) → ((¬α → β) → β)
Hyp
Hyp
Satz 1.32(6)
MP (1),(3)
Satz 1.32(6)
MP (2),(5)
(A3)
MP (6),(7)
MP (4),(7)
DT Hyp (2), (9)
DT Hyp (1), (10)
1.4.22
Gottlob Frege (1848-1925)
Grundgesetze der Arithmetik (1893, 1902)
Gottlob Frege (1848-1925)
Grundgesetze der Arithmetik (1893, 1902)
Auf dem Weg zum Korrektheitslemma
Lemma 1.33 (Alle Axiome sind g¨
ultig)
F¨ur alle Formeln α, β und ϕ gilt
1. α → (β → α) ist g¨ultig,
2. (α → (β → ϕ)) → ((α → β) → (α → ϕ)) ist g¨ultig und
3. (¬β → ¬α) → ((¬β → α) → β) ist g¨ultig.
Beweis: Sei A eine Belegung. Wir zeigen A γ f¨ur jedes Axiom γ.
zu (A1): Es gilt
A α → (β → α) ⇔ A 6 α oder A β → α
⇔ A 6 α oder A 6 β oder A α
Da A 6 α oder A
α, folgt A
α → (β → α).
zu (A2): Es gilt
A (α → (β → ϕ)) → ((α → β) → (α → ϕ))
⇔ A 6 α → (β → ϕ) oder A 6 α → β oder A 6 α oder A ϕ
⇔ A 6 α oder A ϕ oder (A α und A β und A 6 ϕ)
oder (A α und A 6 β)
Da jede Kombination von Erf¨
ullungen von α, β und ϕ diesen Ausdruck
erf¨
ullt, folgt A (α → (β → ϕ)) → ((α → β) → (α → ϕ)).
zu (A3): Es gilt
A
(¬β → ¬α) → ((¬β → α) → β)
⇔ A 6 ¬β → ¬α oder A 6 ¬β → α oder A β
⇔ [A ¬β und (A 6 α oder A 6 ¬α)] oder A β
⇔ [A 6 β und (A 6 α oder A α)] oder A β (∗)
Offensichtlich ist die letzte Aussage (∗) g¨
ultig. Folglich gilt die ¨aquivalente
Aussage A (¬β → ¬α) → ((¬β → α) → β).
Da A beliebig gew¨ahlt wurde,
folgt A γ f¨
ur jede Belegung A und jedes Axiom γ.
X
1.4.25
Lemma 1.34 (Korrektheit von
Fre
)
Sei α eine Formel. Aus Fre α folgt
α.
D.h. jedes Theorem von Fre ist eine g¨ultige Formel.
Beweis: Induktion u¨ber die L¨ange ` des Beweises von α.
IA ` = 1: dann ist α ein Axiom.
Da jedes Axiom g¨ultig ist (Lemma 1.33), folgt α.
IV: die Behauptung gilt f¨ur Formeln mit Beweisen der L¨ange ` ≤ k.
IS ` = k + 1: falls α ein Axiom ist, dann ist α g¨ultig (Lemma 1.33).
Sonst entsteht α mit MP aus αi und αj = αi → α (mit i, j ≤ k).
αi und
αi → α.
Nach IV gilt
¨
Dann muss auch
α gelten (das hatten wir mal als Ubungsaufgabe)
.
X
Lemma 1.35 (Verallgemeinerung der Korrektheit von
Sei α eine Formel und Γ eine Formelmenge. Aus Γ
Der Beweis geht entsprechend dem von Lemma 1.34.
Fre
Fre
)
α folgt Γ
α.
Der Weg zum Vollst¨
andigkeitslemma . . .
I
I
Wir wollen Lemma 1.50 zeigen:
wenn α (“α ist g¨ultig”), dann
Fre
α (“α ist beweisbar”).
Dazu zeigen wir “wenn Fre
6 α, dann 6 α” wie folgt:
6
Fre
1.40
α ⇒
{¬α} Fre
6 ⊥, d.h. {¬α} ist konsistent
1.44
⇒ es gibt eine Menge Γ∗ ⊇ {¬α}, die
maximal bezgl. Konsistenz ist und aus negierten und
nicht-negierten Teilformeln von α besteht
{z
|
α-maximal konsistent
}
1.49
⇒ es gibt eine erf¨ullende Belegung f¨ur dieses Γ∗ ⊇ {¬α}
⇒ es gibt eine erf¨ullende Belegung f¨ur {¬α}
⇒ 6 α
1.4.27
Konsistente Formelmengen
Definition 1.36 (konsistente Formelmenge)
Eine Formelmenge Γ heißt konsistent, falls Γ Fre
6 ⊥.
Beispiel 1.37
Die leere Formelmenge ∅ ist konsistent (d.h. Fre
6 ⊥).
Bew.: Aus ∅ 6
⊥ folgt ∅ Fre
6 ⊥ (Korrektheitslemma 1.34).
X
Beispiel 1.38
Wenn Ai , ¬Ai ∈ Γ (f¨ur ein i), dann ist Γ nicht konsistent (d.h. Γ
Also ist die Menge aller Formeln nicht konsistent.
Bew.: sei Ai , ¬Ai ∈ Γ.
Dann gilt Γ Fre Ai und Γ
Mit MP folgt Γ Fre ⊥.
Fre
¬Ai , d.h. Γ
Fre
Fre
⊥).
Ai → ⊥.
X
1.4.28
Eigenschaften nicht-konsistenter Mengen
Beispiel 1.39
Sei Γ nicht konsistent. Dann gilt
1. Γ
Fre
α f¨ur alle Formeln α, und
2. Γ ist unerf¨ullbar – d.h. A 6 Γ f¨ur alle Belegungen A.
Beweis:
1.) Es gilt Fre (⊥ → ⊥) → (⊥ → α) (Satz 1.32(4)),
und mit Fre ⊥ → ⊥ (Lemma 1.24) und MP folgt
Mit Γ Fre ⊥ folgt Γ Fre α.
Fre
⊥ → α.
2.) Aus Γ Fre ⊥ folgt Γ ⊥ (Korrektheitslemma 1.35).
Da A 6 ⊥ f¨ur jede Belegung A, folgt A 6 Γ f¨ur jedes A.
X
Schritt 1: aus
6
Fre
α folgt {¬α} Fre
6 ⊥
Lemma 1.40 (Nicht-Herleitbarkeit und Konsistenz)
Sei α eine Formel.
Wenn Fre
6 α , dann ist {¬α} konsistent.
Beweis: wir zeigen die Kontraposition:
wenn {¬α}
Aus {¬α}
und mit
Fre
Fre
Fre
⊥
(d.h. {¬α} ist nicht konsistent),
⊥ folgt
Fre
¬¬α
dann
Fre
α.
(DT 1.26),
¬¬α → α (Satz 1.32(2)) und MP folgt
Fre
α.
X
1.4.30
Schritt 2: Maximal konsistente Mengen
Definition 1.41 (maximal konsistente Mengen)
Eine konsistente Menge Γ heißt maximal konsistent,
wenn keine echte Obermenge von Γ konsistent ist.
Definition 1.42 (Teilformeln und deren Negationen)
Tf(α) ist die Menge aller Teilformeln der Formel α.
Tfn(α) = Tf(α) ∪ {¬β | β ∈ Tf(α)}
ist die Menge aller Teilformeln von α und deren Negationen.
Definition 1.43 (maximale Konsistenz relativ zu einer Formel)
Sei α eine Formel.
Eine konsistente Menge Γ ⊆ Tfn(α) heißt α-maximal konsistent,
wenn keine Menge A mit Γ ( A ⊆ Tfn(α) konsistent ist.
Lemma 1.44 (Konsistente Mengen k¨
onnen maximiert werden)
Sei α eine Formel.
Jede konsistente Teilmenge von Tfn(α) besitzt eine α-maximal
konsistente Obermenge.
Beweis: Sei Γ ⊆ Tfn(α) eine konsistente Formelmenge.
Sei ϕ1 , ϕ2 , ϕ3 , . . . , ϕm eine Aufz¨ahlung aller Formeln in Tfn(α).
Definiere Γ0 , Γ1 , . . . , Γm wie folgt.
Γ0 := Γ
(
Γi ∪ {ϕi+1 },
Γi+1 :=
Γi ,
falls Γi ∪ {ϕi+1 } konsistent ist
sonst
Wir zeigen nun, dass Γm α-maximal konsistente Obermenge von Γ ist.
1.) Γm ist eine konsistente Obermenge von Γ und Γm ⊆ Tfn(α):
Das folgt (induktiv) direkt aus der Definition von Γm .
2.) Γm ist α-maximal konsistent:
Zu zeigen: f¨ur jedes ϕr ∈ Tfn(α) − Γm ist Γm ∪ {ϕr } nicht konsistent.
Sei ϕr eine Formel in Tfn(α) − Γm .
Dann ist Γr −1 ∪ {ϕr } nicht konsistent,
und folglich ist auch Γm ∪ {ϕr } nicht konsistent.
X
1.4.33
Sch¨
one Eigenschaften maximal konsistenter Mengen
Lemma 1.45
Sei α eine Formel und Γ eine α-maximal konsistente Menge.
6 β.
F¨ur alle β ∈ Tfn(α) gilt: wenn β 6∈ Γ, dann Γ Fre ¬β und Γ Fre
Beweis: Sei β 6∈ Γ.
Dann folgt Γ ∪ {β} Fre ⊥ (da Γ maximal konsistent und β ∈ Tfn(α) ist)
und damit Γ Fre ¬β (DT 1.26).
Da Γ konsistent ist, folgt Γ Fre
6 β (Bsp. 1.38).
Folgerung 1.46 (Abgeschlossenheit unter Herleitbarkeit)
Sei α eine Formel und Γ eine α-maximal konsistente Menge.
F¨ur alle β ∈ Tfn(α) gilt: wenn Γ Fre β, dann β ∈ Γ.
X
Sch¨
one Eigenschaften maximal konsistenter Mengen
Lemma 1.47
Sei α eine Formel.
F¨ur jede α-maximal konsistente Menge Γ und f¨ur jede Formel
β ∈ Tf (α) gilt:
entweder β ∈ Γ oder ¬β ∈ Γ (und nicht β, ¬β ∈ Γ).
Beweis: Sei Γ α-maximal konsistent und β ∈ Tf(α).
Aus β 6∈ Γ folgt Γ Fre ¬β (Lemma 1.45).
Da Γ α-maximal konsistent ist und ¬β ∈ Tfn(α) ist,
folgt ¬β ∈ Γ (Folgerung 1.46).
(β, ¬β ∈ Γ steht im Widerspruch zur Konsistenz von Γ – siehe Bsp. 1.38.) X
1.4.35
Sch¨
one Eigenschaften maximal konsistenter Mengen
Lemma 1.48
Sei Γ α-maximal konsistent und (β → γ) ∈ Tfn(α).
Dann gilt (β → γ) ∈ Γ genau dann, wenn β 6∈ Γ oder γ ∈ Γ.
(⇐):
(1) Sei γ ∈ Γ. Dann folgt Γ Fre γ.
Mit Axiom (A1) Fre γ → (β → γ) und MP folgt Γ
und mit (1.46) dann β → γ ∈ Γ.
Fre
β→γ
(2) Sei β 6∈ Γ. Da β ∈ Tf(α), folgt ¬β ∈ Γ (1.47) und damit Γ
Mit Fre ¬β → (β → γ) (1.32(4)) folgt Γ Fre β → γ
und mit (1.46) dann β → γ ∈ Γ.
(⇒): Sei β → γ ∈ Γ und β ∈ Γ. Dann folgt Γ Fre β → γ und Γ
Daraus erhalten wir Γ Fre γ und damit γ ∈ Γ (1.46).
Fre
Fre
¬β.
β.
X
1.4.36
Schritt 3: Erfu
¨llbarkeit konsistenter Mengen
Lemma 1.49
Sei α eine Formel. Jede konsistente Teilmenge von Tfn(α) ist erf¨ullbar.
Beweis:
Sei ∆ ⊆ Tfn(α) konsistent.
Dann besitzt ∆ eine α-maximal konsistente Obermenge Γ ⊇ ∆
(Lemma 1.44).
Definiere die Belegung AΓ = Γ ∩ {A0 , A1 , A2 , . . .} aller Atome in Γ.
Behauptung
F¨ur jedes β ∈ Tfn(α) gilt: AΓ
β genau dann, wenn β ∈ Γ.
Behauptung
F¨ur jedes β ∈ Tfn(α) gilt: AΓ
β genau dann, wenn β ∈ Γ.
Beweis mittels Induktion u¨ber den Formelaufbau von β:
Ai gdw. Ai ∈ Γ” gilt
gem¨aß der Definition von AΓ .
Fall 2: β = ⊥: AΓ 6 ⊥ und ⊥ 6∈ Γ, da Γ konsistent ist.
IA: Fall 1: β = Ai ist ein Atom: “AΓ
IV: AΓ
ϕ gdw. ϕ ∈ Γ, und AΓ
IS: zu zeigen: f¨ur β = ϕ → ψ gilt AΓ
¨
Es gelten folgende Aquivalenzen:
AΓ
ψ gdw. ψ ∈ Γ.
β gdw. β ∈ Γ.
gdw. AΓ 6 ϕ oder AΓ ψ
gdw. ϕ 6∈ Γ oder ψ ∈ Γ
gdw. ϕ → ψ ∈ Γ, also β ∈ Γ
Damit ist die Behauptung bewiesen.
β
Mit der Behauptung folgt AΓ
(Semantik von →)
(IV)
(Lemma 1.48)
Γ und wg. Γ ⊇ ∆ auch AΓ
∆.
X
1.4.38
Schritt 4 und Schritt 5, und alles zusammen
Lemma 1.50 (Vollst¨
andigkeitslemma f¨
ur
Fre
)
Sei α eine Formel. Wenn
Fre
α.
α, dann folgt
Beweis: wir zeigen die Kontraposition.
Gelte Fre
6 α.
Dann ist {¬α} konsistent (Lemma 1.40)
und folglich auch erf¨ullbar (Lemma 1.49).
Also gibt es eine erf¨ullende Belegung A von ¬α, d.h. A
Dann folgt A 6 α.
Also ist α nicht g¨ultig.
¬α.
X
Das Vollst¨andigkeitslemma kann auch allgemeiner mit Hypothesen
formuliert werden.
Lemma 1.51 (Verallgemeinertes Vollst¨
andigkeitslemma f¨
ur
Sei Γ eine Formelmenge und α eine Formel.
Aus Γ α folgt Γ Fre α.
Der Beweis geht “im Prinzip” wie bei der Formulierung ohne
Hypothesen.
Fre
)
Der Vollst¨
andigkeitssatz fu
¨r den
Frege-Kalku
¨l
Satz 1.52 (Vollst¨
andigkeitssatz f¨
ur
Fre
Sei α eine Formel.
α genau dann, wenn
Fre
α.
)
Beweis: Folgt aus Lemmas 1.34 und 1.50.
Satz 1.53 (Verallgemeinerter Vollst¨
andigkeitssatz f¨
ur
X
Fre
)
Sei Γ eine Formelmenge und α eine Formel.
Γ Fre α genau dann, wenn Γ α.
Beweis: Folgt aus Lemmas 1.35 und 1.51.
X
1.4.41
¨
Ahnliche
Theorien I
Die Auswahl der Axiome in diesem Frege-Kalk¨
ul stammt aus dem Buch von
Mendelson und hat das Ziel, den Beweis des Vollst¨andigkeitssatzes technisch einfach
zu machen.
Eine Theorie von Kleene (1952) hat Modus Ponens und die folgenden Axiome
(f¨
ur Formeln mit Operatoren →, ∧, ∨ und ¬).
1. α → (β → α)
2. (α → (β → γ)) → ((α → β) → (α → γ))
3. (α ∧ β) → α und (α ∧ β) → β
4. α → (β → (α ∧ β))
5. α → (α ∨ β) und β → (α ∨ β)
6. (α → γ) → ((β → γ) → ((α ∨ β) → γ))
7. (α → β) → ((α → ¬β) → ¬α)
8. ¬¬α → α
Durch Weglassen des letzten Axioms (Doppelnegationsgesetz)
erh¨alt man eine Theorie f¨
ur die intuitionistische Logik.
¨
Ahnliche
Theorien II
Eine Theorie, die auf Arbeiten von Frege basiert,
hat Modus Ponens und die folgenden Axiome
(f¨ur Formeln mit Operatoren → und ¬).
1. α → (β → α)
2. (α → (β → γ)) → ((α → β) → (α → γ))
3. (α → (β → γ)) → (β → (α → γ))
4. (α → β) → (¬β → ¬α)
5. α → ¬¬α
6. ¬¬α → α
1.5 Natu
¨rliches Schließen
1. Klassische Aussagenlogik
Grundbegriffe
Tableau-Kalk¨
ul
Algorithmen
Frege-Kalk¨
ul
Nat¨
urliches Schließen
Formeln und Schlussregeln
Vollst¨andigkeit und Korrektheit
Schlussregeln f¨
ur ∧ und ∨
Vergleich von Beweis-Kalk¨
ulen
Wir geben eine kurze und eher informelle Einf¨
uhrung.
[Literatur:
van Dalen: Logic and Structure]
Natu
¨rliches Schließen
W¨ahrend der Frege-Kalk¨
ul einige Axiome und nur eine Schlussregel hat,
haben wir beim Nat¨
urlichen Schließen
mehrere Schlussregeln und “keine richtigen Axiome”.
Wir betrachten zun¨achst nur Formeln aus
I Atomen,
I dem Konstantensymbol ⊥ (“falsum”,
I dem Verkn¨
upfungszeichen →.
A6
⊥ f¨
ur alle Belegungen A)
und
¬α ist jetzt abk¨
urzende Schreibweise f¨
ur α → ⊥ . . .
Wir schauen uns erstmal etwas informell die Schlussregeln an.
1.5.2
Schlussregeln fu
¨r die Implikation
Die Implikations-Elimination sieht aus wie der modus ponens.
α
α→β
(→ E )
β
Die Implikations-Introduktion ohne und mit Aufl¨osung einer Hypothese.
[α]
..
β
.
(→ I )
α→β
β
(→ I )
α→β
Beweise werden als B¨aume dargestellt,
die mit Hypothesen beginnen (Bl¨atter)
und an deren Wurzel die bewiesene Formel steht.
Statt Kanten werden waagerechte Striche
f¨ur Anwendungen von Schlussregeln gezeichnet.
1.5.3
Beispiele fu
¨r Beweise: (A1)
Ein Beweis f¨ur A → (B → A) (d.h.
Nat
A → (B → A))
[α]
..
.
Die Implikations-Regeln:
β
α→β
(→ I )
β
α→β
(→ I )
Beispiele fu
¨r Beweise: (A1)
Ein Beweis f¨ur A → (B → A) (d.h.
Nat
A → (B → A))
A
[α]
..
.
Die Implikations-Regeln:
β
α→β
(→ I )
β
α→β
(→ I )
Beispiele fu
¨r Beweise: (A1)
Ein Beweis f¨ur A → (B → A) (d.h.
A
B →A
Nat
A → (B → A))
(→ I )
[α]
..
.
Die Implikations-Regeln:
β
α→β
(→ I )
β
α→β
(→ I )
Beispiele fu
¨r Beweise: (A1)
Ein Beweis f¨ur A → (B → A) (d.h.
[A]1
B →A
Nat
A → (B → A))
(→ I )
A → (B → A)
(→ I )1
[α]
..
.
Die Implikations-Regeln:
β
α→β
(→ I )
β
α→β
(→ I )
Beispiele fu
¨r Beweise: (A1)
Ein Beweis f¨ur A → (B → A) (d.h.
[A]1
B →A
Nat
α
(→ I )
A → (B → A)
A → (B → A))
(→ I )1
[α]
..
.
Die Implikations-Regeln:
β
α→β
(→ I )
β
α→β
(→ I )
Beispiele fu
¨r Beweise: (A1)
Ein Beweis f¨ur A → (B → A) (d.h.
[A]1
B →A
Nat
α
(→ I )
A → (B → A)
A → (B → A))
β→α
(→ I )1
(→ I )
[α]
..
.
Die Implikations-Regeln:
β
α→β
(→ I )
β
α→β
(→ I )
Beispiele fu
¨r Beweise: (A1)
Ein Beweis f¨ur A → (B → A) (d.h.
[A]1
B →A
Nat
[α]1
(→ I )
A → (B → A)
A → (B → A))
β→α
(→ I )1
(→ I )
(→ I )1
α → (β → α)
Damit sind alle Axiome (A1) des Frege-Kalk¨uls Fre bewiesen.
[α]
..
.
Die Implikations-Regeln:
β
α→β
(→ I )
β
α→β
(→ I )
Beweis von (A2)
Nat
(α → (β → γ)) → ((α → β) → (α → γ))
Die Implikations-Regeln:
β
α→β
(→ I )
[α]
..
.
β
α→β
(→ I )
α
α→β
β
(→ E )
1.5.5
Beweis von (A2)
Nat
α
(α → (β → γ)) → ((α → β) → (α → γ))
α→β
Die Implikations-Regeln:
β
α→β
(→ I )
[α]
..
.
β
α→β
(→ I )
α
α→β
β
(→ E )
1.5.5
Beweis von (A2)
Nat
(α → (β → γ)) → ((α → β) → (α → γ))
α→β
α
(→ E )
β
Die Implikations-Regeln:
β
α→β
(→ I )
[α]
..
.
β
α→β
(→ I )
α
α→β
β
(→ E )
1.5.5
Beweis von (A2)
Nat
(α → (β → γ)) → ((α → β) → (α → γ))
α→β
α
(→ E )
α → (β → γ)
α
β
Die Implikations-Regeln:
β
α→β
(→ I )
[α]
..
.
β
α→β
(→ I )
α
α→β
β
(→ E )
1.5.5
Beweis von (A2)
Nat
(α → (β → γ)) → ((α → β) → (α → γ))
α→β
α
(→ E )
α → (β → γ)
α
β→γ
β
Die Implikations-Regeln:
β
α→β
(→ I )
(→ E )
[α]
..
.
β
α→β
(→ I )
α
α→β
β
(→ E )
1.5.5
Beweis von (A2)
Nat
(α → (β → γ)) → ((α → β) → (α → γ))
α→β
α
α → (β → γ)
α
(→ E )
β→γ
β
(→ E )
(→ E )
γ
Die Implikations-Regeln:
β
α→β
(→ I )
[α]
..
.
β
α→β
(→ I )
α
α→β
β
(→ E )
1.5.5
Beweis von (A2)
Nat
(α → (β → γ)) → ((α → β) → (α → γ))
α→β
[α]1
α → (β → γ)
[α]1
(→ E )
β→γ
β
(→ E )
(→ E )
γ
α→γ
Die Implikations-Regeln:
β
α→β
(→ I )
(→ I )1
[α]
..
.
β
α→β
(→ I )
α
α→β
β
(→ E )
1.5.5
Beweis von (A2)
Nat
(α → (β → γ)) → ((α → β) → (α → γ))
[α]1
[α → β]2
α → (β → γ)
[α]1
(→ E )
β→γ
β
(→ E )
(→ E )
γ
α→γ
(→ I )1
(α → β) → (α → γ)
Die Implikations-Regeln:
β
α→β
(→ I )
(→ I )2
[α]
..
.
β
α→β
(→ I )
α
α→β
β
(→ E )
1.5.5
Beweis von (A2)
Nat
(α → (β → γ)) → ((α → β) → (α → γ))
[α]1
[α → β]2
[α → (β → γ)]3
[α]1
(→ E )
β→γ
β
(→ E )
(→ E )
γ
α→γ
(→ I )1
(α → β) → (α → γ)
(→ I )2
(→ I )3
(α → (β → γ)) → ((α → β) → (α → γ))
Die Implikations-Regeln:
β
α→β
(→ I )
[α]
..
.
β
α→β
(→ I )
α
α→β
β
(→ E )
1.5.5
Beweis-Beispiel: Doppelnegation
Nat
α → ¬¬α
Die Regeln:
β
α→β
(→ I )
d.h.
Nat
(erste H¨
alfte)
α → ((α → ⊥) → ⊥)
[α]
..
.
β
α→β
(→ I )
α
α→β
(→ E )
β
1.5.6
Beweis-Beispiel: Doppelnegation
Nat
α → ¬¬α
α
¬α
Die Regeln:
β
α→β
(→ I )
d.h.
Nat
(erste H¨
alfte)
α → ((α → ⊥) → ⊥)
[α]
..
.
β
α→β
(→ I )
α
α→β
(→ E )
β
1.5.6
Beweis-Beispiel: Doppelnegation
Nat
α → ¬¬α
α
¬α
⊥
Die Regeln:
β
α→β
(→ I )
d.h.
Nat
(erste H¨
alfte)
α → ((α → ⊥) → ⊥)
(→ E )
[α]
..
.
β
α→β
(→ I )
α
α→β
(→ E )
β
1.5.6
Beweis-Beispiel: Doppelnegation
Nat
α → ¬¬α
α
[¬α]1
⊥
¬¬α
α→β
Nat
α → ((α → ⊥) → ⊥)
(→ E )
(→ I )1
Die Regeln:
β
d.h.
(erste H¨
alfte)
(→ I )
[α]
..
.
β
α→β
(→ I )
α
α→β
(→ E )
β
1.5.6
Beweis-Beispiel: Doppelnegation
Nat
α → ¬¬α
[α]2
[¬α]1
⊥
¬¬α
Die Regeln:
α→β
Nat
α → ((α → ⊥) → ⊥)
(→ E )
(→ I )1
α → ¬¬α
β
d.h.
(erste H¨
alfte)
(→ I )
(→ I )2
[α]
..
.
β
α→β
(→ I )
α
α→β
(→ E )
β
1.5.6
Beweis-Beispiel: Doppelnegation
Nat
α → ¬¬α
[α]2
[¬α]1
⊥
¬¬α
Die Regeln:
α→β
Nat
α → ((α → ⊥) → ⊥)
α→⊥
α
(→ E )
(→ I )1
α → ¬¬α
β
d.h.
(erste H¨
alfte)
(→ I )
(→ I )2
[α]
..
.
β
α→β
(→ I )
α
α→β
(→ E )
β
1.5.6
Beweis-Beispiel: Doppelnegation
Nat
α → ¬¬α
[α]2
[¬α]1
⊥
¬¬α
Die Regeln:
α→β
Nat
α → ((α → ⊥) → ⊥)
α→⊥
α
(→ E )
⊥
(→ I )1
α → ¬¬α
β
d.h.
(→ I )
(erste H¨
alfte)
(→ E )
(→ I )2
[α]
..
.
β
α→β
(→ I )
α
α→β
(→ E )
β
1.5.6
Beweis-Beispiel: Doppelnegation
Nat
α → ¬¬α
[α]2
[¬α]1
⊥
¬¬α
Die Regeln:
α→β
Nat
α → ((α → ⊥) → ⊥)
(→ I )
[α → ⊥]1
α
(→ E )
⊥
(→ I )1
α → ¬¬α
β
d.h.
(erste H¨
alfte)
(α → ⊥) → ⊥
(→ I )2
(→ E )
(→ I )1
[α]
..
.
β
α→β
(→ I )
α
α→β
(→ E )
β
1.5.6
Beweis-Beispiel: Doppelnegation
Nat
α → ¬¬α
[α]2
[¬α]1
⊥
¬¬α
Die Regeln:
α→β
Nat
α → ((α → ⊥) → ⊥)
[α]2 [α → ⊥]1
(→ E )
⊥
(→ I )1
α → ¬¬α
β
d.h.
(→ I )
(α → ⊥) → ⊥
(→ I )2
(erste H¨
alfte)
(→ E )
(→ I )1
α → ((α → ⊥) → ⊥)
(→ I )2
[α]
..
.
β
α→β
(→ I )
α
α→β
(→ E )
β
1.5.6
Schlussregeln fu
¨r ⊥
Ex falso quod libet
⊥
(⊥)
α
Reductio ad absurdum
[¬α]
..
.
⊥
(RAA)
α
(“(→ I ) mit Doppelnegationsregel”)
1.5.7
Beweis-Beispiel: Doppelnegation
Nat
(zweite H¨
alfte)
¬¬α → α
Die Regeln:
β
α→β
(→ I )
[α]
..
.
β
α→β
[¬α]
..
.
(→ I )
α
α→β
β
(→ E )
⊥
α
(RAA)
Beweis-Beispiel: Doppelnegation
Nat
(zweite H¨
alfte)
¬¬α → α
¬¬α
¬α
Die Regeln:
β
α→β
(→ I )
[α]
..
.
β
α→β
[¬α]
..
.
(→ I )
α
α→β
β
(→ E )
⊥
(RAA)
α
1.5.8
Beweis-Beispiel: Doppelnegation
Nat
(zweite H¨
alfte)
¬¬α → α
¬¬α
¬α
⊥
Die Regeln:
β
α→β
(→ I )
(→ E )
[α]
..
.
β
α→β
[¬α]
..
.
(→ I )
α
α→β
β
(→ E )
⊥
(RAA)
α
1.5.8
Beweis-Beispiel: Doppelnegation
Nat
(zweite H¨
alfte)
¬¬α → α
¬¬α
[¬α]1
⊥
α
Die Regeln:
β
α→β
(→ I )
(→ E )
(RAA)1
[α]
..
.
β
α→β
[¬α]
..
.
(→ I )
α
α→β
β
(→ E )
⊥
(RAA)
α
1.5.8
Beweis-Beispiel: Doppelnegation
Nat
(zweite H¨
alfte)
¬¬α → α
[¬¬α]2
[¬α]1
⊥
α
(RAA)1
¬¬α → α
Die Regeln:
β
α→β
(→ I )
(→ E )
(→ I )2
[α]
..
.
β
α→β
[¬α]
..
.
(→ I )
α
α→β
β
(→ E )
⊥
(RAA)
α
1.5.8
Beweis-Beispiel: Doppelnegation
Nat
(zweite H¨
alfte)
¬¬α → α
[¬¬α]2
[¬α]1
⊥
α
β
α→β
(→ I )
α→⊥
(RAA)1
¬¬α → α
Die Regeln:
(α → ⊥) → ⊥
(→ E )
(→ I )2
[α]
..
.
β
α→β
[¬α]
..
.
(→ I )
α
α→β
β
(→ E )
⊥
(RAA)
α
1.5.8
Beweis-Beispiel: Doppelnegation
Nat
(zweite H¨
alfte)
¬¬α → α
[¬¬α]2
[¬α]1
⊥
α
β
α→β
(→ I )
α→⊥
⊥
(RAA)1
¬¬α → α
Die Regeln:
(α → ⊥) → ⊥
(→ E )
(→ E )
(→ I )2
[α]
..
.
β
α→β
[¬α]
..
.
(→ I )
α
α→β
β
(→ E )
⊥
(RAA)
α
1.5.8
Beweis-Beispiel: Doppelnegation
Nat
(zweite H¨
alfte)
¬¬α → α
[¬¬α]2
[¬α]1
⊥
α
β
α→β
(→ I )
⊥
(RAA)1
¬¬α → α
Die Regeln:
(α → ⊥) → ⊥
(→ E )
α
(→ I )2
[α]
..
.
β
α→β
[α → ⊥]1
(→ E )
(→ RAA)1
[¬α]
..
.
(→ I )
α
α→β
β
(→ E )
⊥
(RAA)
α
1.5.8
Beweis-Beispiel: Doppelnegation
Nat
(zweite H¨
alfte)
¬¬α → α
[¬¬α]2
[¬α]1
⊥
α
β
α→β
(→ I )
⊥
(RAA)1
¬¬α → α
Die Regeln:
[(α → ⊥) → ⊥]2
(→ E )
α
(→ I )2
α→β
(→ E )
(→ RAA)1
((α → ⊥) → ⊥) → α
[α]
..
.
β
[α → ⊥]1
(→ I )2
[¬α]
..
.
(→ I )
α
α→β
β
(→ E )
⊥
(RAA)
α
1.5.8
Beweis von (A3)
Nat
(¬β → ¬α) → ((¬β → α) → β)
1.5.9
Beweis von (A3)
Nat
(¬β → ¬α) → ((¬β → α) → β)
¬β → α
¬β
1.5.9
Beweis von (A3)
Nat
(¬β → ¬α) → ((¬β → α) → β)
¬β → α
¬β
(→ E )
α
1.5.9
Beweis von (A3)
Nat
(¬β → ¬α) → ((¬β → α) → β)
¬β → α
¬β
(→ E )
¬β → ¬α
¬β
α
1.5.9
Beweis von (A3)
Nat
(¬β → ¬α) → ((¬β → α) → β)
¬β → α
¬β
α
(→ E )
¬β → ¬α
¬α
¬β
(→ E )
1.5.9
Beweis von (A3)
Nat
(¬β → ¬α) → ((¬β → α) → β)
¬β → α
¬β
(→ E )
α
⊥
¬β → ¬α
¬α
¬β
(→ E )
(→ E )
1.5.9
Beweis von (A3)
Nat
(¬β → ¬α) → ((¬β → α) → β)
¬β → α
[¬β]1
(→ E )
¬β → ¬α
¬α
α
⊥
β
[¬β]1
(→ E )
(→ E )
(RAA)1
1.5.9
Beweis von (A3)
Nat
(¬β → ¬α) → ((¬β → α) → β)
[¬β → α]2
[¬β]1
¬β → ¬α
(→ E )
¬α
α
⊥
β
[¬β]1
(→ E )
(→ E )
(RAA)1
(¬β → α) → β
(→ I )2
1.5.9
Beweis von (A3)
Nat
(¬β → ¬α) → ((¬β → α) → β)
[¬β → α]2
[¬β]1
[¬β → ¬α]3 [¬β]1
(→ E )
¬α
α
⊥
β
(→ E )
(→ E )
(RAA)1
(¬β → α) → β
(→ I )2
(¬β → ¬α) → ((¬β → α) → β)
(→ I )3
1.5.9
Natu
¨rliches Schließen – formaler
Anders als beim Frege-Kalk¨ul geht es beim Nat¨urlichen Schließen nicht
um das Herleiten von Formeln, sondern um das Herleiten von
Sequenten.
Definition 1.54 (Sequent)
Ein Sequent ist ein Paar Γ I ϕ,
wobei Γ eine Formelmenge und ϕ eine Formel ist.
Statt Γ ∪ {α} I ϕ schreiben wir vereinfachend Γ, α I ϕ etc.
Wir k¨onnen nun die Regeln des Nat¨urlichen Schließens als Regeln f¨ur
Sequenten aufschreiben – dadurch wird das bisher etwas schwammige
“Aufl¨osen von Hypothesen” klar definiert.
Natu
¨rliches Schließen
1. Die Elemente des Nat¨urlichen Schließens sind Sequenten aus
Formeln aus Atomen, ⊥ und →.
2. Die Axiome des Nat¨urlichen Schließens sind Sequenten α I α f¨ur
alle Formeln α.
3. Die Schlussregeln des Nat¨urlichen Schließens sind f¨ur
Formelmengen Γ, ∆ und Formeln α, β:
Γ, β I α
ΓIβ→α
(→ I )
Γ, ¬β I ⊥
ΓIβ
“Γ, ∆” steht f¨
ur Γ ∪ ∆.
ΓIα ∆Iα→β
(→ E )
Γ, ∆ I β
(RAA)
ΓIα
Γ, β I α
(Hyp)
4. Eine Herleitung eines Sequenten Γ I α mittels Nat¨urlichem
Schließen ist eine Folge Γ1 I α1 , Γ2 I α2 , . . . , Γ` I α` von
Sequenten, an deren Ende Γ I α(= Γ` I α` ) steht und deren
Elemente folgende Eigenschaften haben
(f¨
ur i = 1, 2, . . . , `):
I
I
Γi I αi ist ein Axiom, oder
es gibt Γa I αa und ggf. Γb I αb mit a, b < i, aus denen Γi I αi
in einem Schritt mit einer Schlussregel hergeleitet werden kann.
(Statt Herleitung verwendet man gerne auch Beweis.)
5. Formel α ist ein Theorem des Nat¨urlichen Schließens
(Schreibweise: Nat α), wenn es eine Herleitung von I α mittels
Nat¨urlichem Schließen gibt.
Allgemeiner schreiben wir Γ Nat α, wenn es eine Herleitung von
Γ I α mittels Nat¨urlichem Schließen gibt.
1.5.12
Nat
α → (β → α)
(1)
α I
(2) α, β I
(3)
α I
(4)
I
formal
α
α
(Hyp)(1)
β→α
(→ I )(2)
α → (β → α) (→ I )(3)
1.5.13
Nat
α → ¬¬α
(1)
α I
(2)
¬α I
(3) α, ¬α I
(4)
α I
(5)
I
formal
α
¬α
⊥
(→ E )(1), (2)
¬¬α
(→ I )(3)
α → ¬¬α (→ I )(4)
1.5.14
Nat
¬¬α → α
(1)
¬α I
(2)
¬¬α I
(3) ¬α, ¬¬α I
(4)
¬¬α I
(5)
I
formal
¬α
¬¬α
⊥
(→ E )(1), (2)
α
(RAA)(3)
¬¬α → α (→ I )(4)
1.5.15
Nat
(α → (β → γ)) → ((α → β) → (α → γ))
formal
(1)
α I α
(2)
α→β I α→β
(3)
α, α → β I β
(4)
α → (β → γ) I α → (β → γ)
(5)
α, α → (β → γ) I β → γ
(6) α, α → (β → γ), α → β I γ
(7)
α → (β → γ), α → β I α → γ
(8)
α → (β → γ) I (α → β) → (α → γ)
(9) I (α → (β → γ)) → ((α → β) → (α → γ))
(→ E )(1), (2)
(→ E )(1), (4)
(→ E )(3), (5)
(→ I )(6)
(→ I )(7)
(→ I )(8)
1.5.16
Nat
(¬β → ¬α) → ((¬β → α) → β))
formal
(1)
¬β I ¬β
(2)
¬β → ¬α I ¬β → ¬α
(3)
¬β, ¬β → ¬α I ¬α
(4)
¬β → α I ¬β → α
(5)
¬β, ¬β → α I α
(6) ¬β, ¬β → ¬α, ¬β → α I ⊥
(7)
¬β → ¬α, ¬β → α I β
(8)
¬β → ¬α I (¬β → α) → β
(9)
I (¬β → ¬α) → ((¬β → α) → β)
(→ E )(1), (2)
(→ E )(1), (4)
(→ E ), (3)(5)
(RAA)(6)
(→ I )(7)
(→ I )(8)
1.5.17
Zusammenfassung der bisherigen Resultate
Satz 1.55
F¨ur alle Formeln α, β und γ gilt:
1.
Nat
α → (β → α)
2.
Nat
(α → (β → γ)) → ((α → β) → (α → γ))
3.
Nat
(¬β → ¬α) → ((¬β → α) → β)
4.
Nat
¬¬α → α
5.
Nat
α → ¬¬α
Vollst¨
andigkeit von
Nat
Lemma 1.56 (Vollst¨
andigkeitslemma f¨
ur
Sei α eine Formel.
Aus
α folgt
Nat
Nat
)
α.
Beweis:
Sei α g¨ultig.
Dann gilt Fre α (Lemma 1.34).
Also gibt es eine Herleitung β1 , β2 , . . . , β` von α gem¨aß Fre .
Dann ist I β1 , I β2 , . . . , I β` eine Herleitung von I α mittels
Nat¨urlichem Schließen mit folgenden Begr¨undungen.
I Wenn βi ein Axiom des Frege-Kalk¨
uls ist, dann gilt I βi gem¨aß
Satz 1.55).
I Wenn βi aus βa und βb (a, b < i) mittels MP entsteht, dann
entsteht I βi aus I βa und I βb mittels (→ E ).
Also ist I α herleitbar mittels Nat¨urlichem Schließen, d.h. Nat α.
X
Korrektheit von
Nat
Beispiel zur Umwandlung eines Nat -Beweises in einen
(1)
¬α I ¬α
(2)
¬¬α I ¬¬α
(3) ¬α, ¬¬α I ⊥
(→ E )(1), (2)
(4)
¬¬α I α
(RAA)(3)
(5)
I ¬¬α → α (→ I )(4)
(1)
¬α
(2)
¬¬α
(3) ¬α, ¬¬α
(4a)
¬¬α
(4b)
¬¬α
(4)
¬¬α
(5)
Fre
Fre
Fre
Fre
Fre
Fre
Fre
¬α
¬¬α
⊥
¬α → ⊥
¬¬α → α
α
¬¬α → α
Fre
-Beweis:
MP(1), (2) und Vereinigung der Hypothesenmen
DT(3)
Satz 1.32(2)
MP(4a), (4b)
DT(4)
1.5.20
Simulation in die umgekehrte Richtung
Lemma 1.57 (Korrektheitslemma f¨
ur
Sei α eine Formel.
Wenn
Nat
α, dann
Nat
Fre
)
α.
Beweis:
Sei Γ1 I α1 , . . . , Γ` I α` eine Herleitung von I α mittels Nat¨urlichem
Schließen.
Behauptung 1
F¨ur j = 1, 2, . . . , ` gilt Γj
Fre
αj .
Wir beweisen die Behauptung mittels Induktion u¨ber j.
IA: Γ1 I α1 ist α1 I α1 . Es gilt offensichtlich α1
IV: Γi
Fre
αi gilt f¨ur i = 1, 2, . . . , j.
Fre
α1 .
IS: zu zeigen: Γj+1
Fre
αj+1 .
Fall 1: Γj+1 I αj+1 ist αj+1 I αj+1 .
αj+1
Fre
αj+1 gilt offensichtlich.
Fall 2: Γj+1 I αj+1 ensteht aus Γa I αa mittels (→ I ).
Dann ist αj+1 = β → αa und Γj+1 ∪ {β} = Γa .
Nach IV gilt Γa Fre αa , also Γj+1 , β Fre αa .
Mit DT folgt Γj+1 Fre β → αa , also Γj+1 Fre αj+1 .
Fall 3: Γj+1 I αj+1 ensteht aus Γa I αa und Γb I αb mittels (→ E ).
Dann ist Γj+1 = Γa ∪ Γb und αb = αa → αj+1 .
Nach IV gilt Γa Fre αa und Γb Fre αb .
Da Γj+1 ⊇ Γa und Γj+1 ⊇ Γb , gilt ebenso Γj+1 Fre αa und Γj+1
Mit MP folgt dann Γj+1 Fre αj+1 .
Fre
αb .
1.5.22
Fall 4: Γj+1 I αj+1 ensteht aus Γa I αa mittels (RAA).
Dann ist Γj+1 ∪ {¬αj+1 } = Γa und αa = ⊥.
Nach IV gilt Γa Fre ⊥, d.h. Γj+1 , ¬αj+1 Fre ⊥.
Mit DT folgt Γj+1 Fre ¬¬αj+1 .
Mit Fre ¬¬αj+1 → αj+1 (Satz 1.32(2)) und MP folgt Γj+1
Fre
αj+1 .
Fall 5: Γj+1 I αj+1 ensteht aus Γa I αa mittels (Hyp).
Dann ist αj+1 = αa und Γj+1 = Γa ∪ {β}.
Nach IV gilt Γa Fre αa , d.h. Γa Fre αj+1 .
Da Γj+1 ⊇ Γa , folgt ebenso Γj+1 Fre αj+1 .
Damit ist die Behauptung bewiesen.
Also gilt Γ` Fre α` , d.h. Fre α.
X
1.5.23
Vollst¨
andigkeitssatz fu
¨r
Satz 1.58 (Vollst¨
andigkeitssatz f¨
ur
Nat
Nat
Nat
)
ist korrekt und vollst¨andig f¨ur g¨ultige Formeln.
D.h. f¨ur alle Formeln α gilt
Nat
α gdw.
Beweis: folgt aus Lemmas 1.56 und 1.57.
α.
X
1.5.24
Schlussregeln fu
¨r ∧ und ∨
Die Schlussregeln f¨ur ∧ sind recht intuitiv.
α
β
α∧β
α∧β
(∧I )
α∧β
(∧E )
α
(∧E )
β
Die f¨ur ∨ nicht sofort . . .
α
α∨β
(∨I )
β
α∨β
(∨I )
α∨β
[α] [β]
..
..
.
.
ϕ ϕ
(∨E )
ϕ
1.5.25
Nat
α ∨ ¬α
α
1.5.26
Nat
α ∨ ¬α
α
α ∨ ¬α
(∨I )
1.5.26
Nat
α ∨ ¬α
α
α ∨ ¬α
(∨I )
¬(α ∨ ¬α)
⊥
(→ E )
1.5.26
Nat
α ∨ ¬α
[α]1
α ∨ ¬α
(∨I )
¬(α ∨ ¬α)
⊥
¬α
(→ E )
(→ I )1
1.5.26
Nat
α ∨ ¬α
[α]1
α ∨ ¬α
(∨I )
¬(α ∨ ¬α)
⊥
¬α
α ∨ ¬α
(→ E )
(→ I )1
(∨I )
1.5.26
Nat
α ∨ ¬α
[α]1
α ∨ ¬α
(∨I )
¬(α ∨ ¬α)
⊥
¬α
α ∨ ¬α
(→ E )
(→ I )1
(∨I )
¬(α ∨ ¬α)
⊥
(→ E )
1.5.26
Nat
α ∨ ¬α
[α]1
α ∨ ¬α
(∨I )
[¬(α ∨ ¬α)]2
(→ E )
⊥
¬α
α ∨ ¬α
(→ I )1
(∨I )
[¬(α ∨ ¬α)]2
⊥
α ∨ ¬α
(→ E )
(RAA)2
1.5.26
Nat
((α ∧ β) ∨ γ) → (α ∨ γ) ∧ (β ∨ γ)
[α ∧ β]1
α
(∨I )
[(α ∧ β) ∨ γ]3 α ∨ γ
[α ∧ β]2
(∧E )
[γ]1
(∧E )
β
(∨I )
α∨γ
(∨E )1
(∨I )
[(α ∧ β) ∨ γ]3 β ∨ γ
α∨γ
[γ]2
(∨I )
β∨γ
(∨E )2
β∨γ
(∧I )
(α ∨ γ) ∧ (β ∨ γ)
(→ I )3
((α ∧ β) ∨ γ) → ((α ∨ γ) ∧ (β ∨ γ))
1.5.27
Die ∨-Elimination
l¨asst sich auch mit → und ⊥ aufschreiben
[α] [β]
..
..
.
.
¬α → β
ϕ ϕ
(∨E )
ϕ
und als Abk¨urzung f¨ur folgendes ansehen.
[α]1
[β]2
..
..
.
.
ϕ [¬ϕ]3
ϕ [¬ϕ]3
(→ E )
(→ E )
⊥ (→ I )
⊥ (→ I )
1
2
¬α → β
¬α (→ E )
¬β
β
(→ E )
⊥ (RAA)
3
ϕ
1.5.28
Lemma 1.59 (Simulation von Resolutionsschritten in Nat)
Jeder Resolutionsschritt l¨asst sich durch eine konstante Anzahl von
Beweisschritten in Nat simulieren; genauer gesagt: die Herleitung
α ∨ Ai , β ∨ ¬Ai Nat α ∨ β geht mit 6 Schritten.
[Ai ]2
[¬Ai ]1
⊥
(→ E )
(⊥)
β ∨ ¬Ai
[α]2
α ∨ Ai
α∨β
[β]1
β
(∨E )1
β
(∨I )
α∨β
α∨β
(∨I )
(∨E )2
Wenn α oder/und β leer sind, geht es noch einfacher . . .
1.5.29
Vergleich von Beweis-Kalku
¨len
1. Klassische Aussagenlogik
Grundbegriffe
Tableau-Kalk¨
ul
Algorithmen
Frege-Kalk¨
ul
Nat¨
urliches Schließen
Vergleich von Beweis-Kalk¨
ulen
Einerseits lassen sich Beweise in verschiedenen Beweis-Kalk¨
ulen ineinander
u
uhren, andererseits gibt es Formeln, die in einem Kalk¨
ul nur lange Beweise,
¨berf¨
in einem anderen dagegen auch kurze Beweise haben.
Das f¨
uhrt zu einer Hierarchie von Beweis-Kalk¨
ulen.
[Literatur:
Urquhart: The complexity of propositional proofs.]
1.6.1
Was haben wir gemacht?
Wir haben gesehen,
wie man Beweise einer Theorie in Beweise einer anderen Theorie
umwandeln kann.
Das kann man auch abstrakt betrachten.
Definition 1.60 (Polynomielle Simulation zwischen Theorien)
Eine Theorie X l¨asst sich durch eine Theorie Y p-simulieren,
falls es eine polynomiell berechenbare Funktion q gibt,
so dass f¨ur alle Beweise π in X und alle Formeln α gilt:
wenn π ein Beweis von α in X ist,
dann ist q(π) ein Beweis von α in Y .
Eigenschaften von Simulationen
Wir haben zwei p-Simulationen gezeigt.
Lemma 1.61
1. Nat l¨asst sich durch Fre p-simulieren.
2. Fre l¨asst sich durch Nat p-simulieren.
Wir haben Simulationen zum Nachweis von Korrektheit und
Vollst¨andigkeit benutzt.
Lemma 1.62 (informell)
Theorie X lasse sich durch Theorie Y p-simulieren.
1. Wenn X vollst¨andig ist, dann ist Y vollst¨andig.
2. Wenn Y korrekt ist, dann ist X korrekt.
Eine Hierarchie der Beweissysteme
Nat.Schließen
keine bekannten
super-polynomiellen
unteren Schranken f¨ur die
Beweisl¨ange
Frege-Kalk¨ul
=
Cutting planes
keine polynomiellen Beweissysteme
=
Resolution
=
Baum-Resolution
==
=
Tableau
Wahrheitstafeln
1.6.4
2 Modale Aussagenlogik
2. Modale Aussagenlogik
Grundbegriffe
Tableau-Kalk¨ul
Frege-Kalk¨ul
Algorithmen
2.0.1
2 Modale Aussagenlogik
W¨ahrend in der bisher betrachteten klassischen Aussagenlogik nur die Wahrheit von
Aussagen wichtig ist, spielt in der modalen Aussagenlogik die Art und Weise
(modus), in der ein Aussage wahr ist, eine Rolle.
oglicherweise wahr sein,
Eine Aussage kann I notwendigerweise oder m¨
I
heute, gestern oder morgen wahr sein,
I
geglaubt oder gewusst werden,
vor/nach der Ausf¨
uhrung eines Programmschrittes wahr sein.
Wir werden die Grundlagen der Modallogik mit zwei Beweiskalk¨
ulen sowie
Algorithmen betrachten.
I
2.1 Grundbegriffe
2. Modale Aussagenlogik
Grundbegriffe
Tableau-Kalk¨
ul
Frege-Kalk¨
ul
Algorithmen
Literatur: Priest: An introduction to non-classical logic.
Kreuzer, K¨
uhling: Logik f¨
ur Informatiker.
2.1.1
Einfu
¨hrendes Beispiel zur Modallogik
Modallogische Formeln haben zus¨atzliche einstellige Operatoren: und ♦ .
Formelbeispiele: A,
♦(A ∨ ¬B), (♦(A ∧ ♦¬(B ∨ C )) ∧ A)
Semantik: Graph M aus Belegungen (=Kripke-Modell)
Welt s erf¨
ullt ϕ
genau dann, wenn
alle Nachfolger von s erf¨
ullen ϕ
s
A
B, C
C
A
A, B
A, C
M
Einfu
¨hrendes Beispiel zur Modallogik
Modallogische Formeln haben zus¨atzliche einstellige Operatoren: und ♦ .
Formelbeispiele: A,
♦(A ∨ ¬B), (♦(A ∧ ♦¬(B ∨ C )) ∧ A)
Semantik: Graph M aus Belegungen (=Kripke-Modell)
Welt s erf¨
ullt ϕ
genau dann, wenn
alle Nachfolger von s erf¨
ullen ϕ
s
A
B, C
C
A
A, B
A, C
M
M, s
M, s
K
K
C
(B ∨ A)
Einfu
¨hrendes Beispiel zur Modallogik
Modallogische Formeln haben zus¨atzliche einstellige Operatoren: und ♦ .
Formelbeispiele: A,
♦(A ∨ ¬B), (♦(A ∧ ♦¬(B ∨ C )) ∧ A)
Semantik: Graph M aus Belegungen (=Kripke-Modell)
Welt s erf¨
ullt ϕ
genau dann, wenn
alle Nachfolger von s erf¨
ullen ϕ
s
A
B, C
C
A
A, B
A, C
M
M, s K
M, s K
M, s 6 K
M, s K
C
(B ∨ A)
B
¬B
Einfu
¨hrendes Beispiel zur Modallogik
Modallogische Formeln haben zus¨atzliche einstellige Operatoren: und ♦ .
Formelbeispiele: A,
♦(A ∨ ¬B), (♦(A ∧ ♦¬(B ∨ C )) ∧ A)
Semantik: Graph M aus Belegungen (=Kripke-Modell)
Welt s erf¨
ullt ϕ
genau dann, wenn
alle Nachfolger von s erf¨
ullen ϕ
s
A
B, C
C
A
A, B
A, C
M
M, s K
M, s K
M, s 6 K
M, s K
M, s K
M, s K
C
(B ∨ A)
B
¬B
C ∧ ¬B
A
Einfu
¨hrendes Beispiel zur Modallogik
Modallogische Formeln haben zus¨atzliche einstellige Operatoren: und ♦ .
Formelbeispiele: A,
♦(A ∨ ¬B), (♦(A ∧ ♦¬(B ∨ C )) ∧ A)
Semantik: Graph M aus Belegungen (=Kripke-Modell)
Welt s erf¨
ullt ♦ϕ
genau dann, wenn
mind. ein Nachfolger von s erf¨
ullt ϕ
s
A
B, C
C
A
A, B
A, C
M
Einfu
¨hrendes Beispiel zur Modallogik
Modallogische Formeln haben zus¨atzliche einstellige Operatoren: und ♦ .
Formelbeispiele: A,
♦(A ∨ ¬B), (♦(A ∧ ♦¬(B ∨ C )) ∧ A)
Semantik: Graph M aus Belegungen (=Kripke-Modell)
Welt s erf¨
ullt ♦ϕ
genau dann, wenn
mind. ein Nachfolger von s erf¨
ullt ϕ
s
A
B, C
C
A
A, B
A, C
M
M, s
K
♦B
Einfu
¨hrendes Beispiel zur Modallogik
Modallogische Formeln haben zus¨atzliche einstellige Operatoren: und ♦ .
Formelbeispiele: A,
♦(A ∨ ¬B), (♦(A ∧ ♦¬(B ∨ C )) ∧ A)
Semantik: Graph M aus Belegungen (=Kripke-Modell)
Welt s erf¨
ullt ♦ϕ
genau dann, wenn
mind. ein Nachfolger von s erf¨
ullt ϕ
s
A
B, C
C
A
A, B
A, C
M
M, s
M, s
K
K
♦B
♦C
Einfu
¨hrendes Beispiel zur Modallogik
Modallogische Formeln haben zus¨atzliche einstellige Operatoren: und ♦ .
Formelbeispiele: A,
♦(A ∨ ¬B), (♦(A ∧ ♦¬(B ∨ C )) ∧ A)
Semantik: Graph M aus Belegungen (=Kripke-Modell)
Welt s erf¨
ullt ♦ϕ
genau dann, wenn
mind. ein Nachfolger von s erf¨
ullt ϕ
s
A
B, C
C
A
A, B
A, C
M
M, s K
M, s K
M, s 6 K
♦B
♦C
♦A
Einfu
¨hrendes Beispiel zur Modallogik
Modallogische Formeln haben zus¨atzliche einstellige Operatoren: und ♦ .
Formelbeispiele: A,
♦(A ∨ ¬B), (♦(A ∧ ♦¬(B ∨ C )) ∧ A)
Semantik: Graph M aus Belegungen (=Kripke-Modell)
Welt s erf¨
ullt ♦ϕ
genau dann, wenn
mind. ein Nachfolger von s erf¨
ullt ϕ
s
A
B, C
C
A
A, B
A, C
M
M, s K
M, s K
M, s 6 K
M, s K
♦B
♦C
♦A
♦♦(A ∧ ¬B)
Einfu
¨hrendes Beispiel zur Modallogik
Modallogische Formeln haben zus¨atzliche einstellige Operatoren: und ♦ .
Formelbeispiele: A,
♦(A ∨ ¬B), (♦(A ∧ ♦¬(B ∨ C )) ∧ A)
Semantik: Graph M aus Belegungen (=Kripke-Modell)
Welt s erf¨
ullt ♦ϕ
genau dann, wenn
mind. ein Nachfolger von s erf¨
ullt ϕ
s
A
B, C
C
A
A, B
A, C
M
M, s K
M, s K
M, s 6 K
M, s K
M, s K
♦B
♦C
♦A
♦♦(A ∧ ¬B)
¬¬B
Modallogik formal: Formeln
Definition 2.1 (modallogische Formel)
Eine atomare Formel hat die Form Ai f¨ur i = 0, 1, 2, . . .
Modallogische Formeln sind induktiv definiert wie folgt.
1. Alle atomaren Formeln, ⊥ und > sind Formeln.
I F¨
2.
ur jede Formel α ist ¬α eine Formel.
I
I
F¨
ur jede Formel α sind α sowie ♦α Formeln.
F¨
ur alle Formeln α und β sind (α ∧ β) sowie (α ∨ β) ebenfalls
Formeln.
Beispiel:
♦¬♦(A1 ∨ (A3 ∧ (A3 ∧ A5 )))
2.1.3
Modallogik formal: (Kripke-)Semantik
Definition 2.2 (Kripke-Modell)
Ein Kripke-Modell M = (W , R, ξ) besteht aus
I
einem Graph (W , R)
mit Knotenmenge W (Welten), W 6= ∅, und Kantenmenge R, und
I
einer Belegung ξ(w ) ⊆ {A0 , A1 , A2 , . . .} f¨ur jede Welt w .
Konkrete Kripke-Modelle werden in der Regel graphisch angegeben.
Definition 2.3 (Erf¨
ullungsrelation
K
)
Sei M = (W , R, ξ) ein Kripke-Modell, w ∈ W sei eine Welt von M, α
und β seien modale Formeln.
Dei Erf¨ullungsrelation K zwischen Modellen, Welten und Formeln ist
wie folgt definiert.
M, w
M, w
M, w
M, w
M, w
M, w
M, w
K
K
K
K
>
Ai
und
M, w 6 K ⊥
gdw. Ai ∈ ξ(w )
α ∧ β gdw. M, w
α ∨ β gdw. M, w
K
K
α und M, w
α oder M, w
K
K
β
β
¬α
gdw. M, w 6 K α
K
α
gdw. f¨ur alle t ∈ W mit (w , t) ∈ R : M, t
K
♦α
gdw. es gibt ein t ∈ W mit (w , t) ∈ R : M, t
K
K
α
K
α
Formelauswertung
mit Dynamischem Programmieren
f¨
ur alle Teilformeln α in aufsteigender Reihenfolge wiederhole:
markiere jede Welt, die α erf¨
ullt . . .
s
A
teste M, s K ♦A:
1.) markiere mit A
2.) markiere mit ♦A
3.) entscheide M, s K ♦A
A
A
A
2.1.6
Formelauswertung
mit Dynamischem Programmieren
f¨
ur alle Teilformeln α in aufsteigender Reihenfolge wiederhole:
markiere jede Welt, die α erf¨
ullt . . .
s
A A
A
A
teste M, s K ♦A:
1.) markiere mit A
2.) markiere mit ♦A
3.) entscheide M, s K ♦A
A A
A A
A A
2.1.6
Formelauswertung
mit Dynamischem Programmieren
f¨
ur alle Teilformeln α in aufsteigender Reihenfolge wiederhole:
markiere jede Welt, die α erf¨
ullt . . .
s
A
♦A
♦A A
♦A
teste M, s K ♦A:
1.) markiere mit A
2.) markiere mit ♦A
3.) entscheide M, s K ♦A
♦A A A
♦A A A
A
♦A
2.1.6
Formelauswertung
mit Dynamischem Programmieren
f¨
ur alle Teilformeln α in aufsteigender Reihenfolge wiederhole:
markiere jede Welt, die α erf¨
ullt . . .
s
A
♦A ♦A
♦A A
♦A
teste M, s K ♦A:
1.) markiere mit A
2.) markiere mit ♦A
3.) entscheide M, s K ♦A
♦A A A
A A
A
Rechenzeit: Anzahl Teilformeln · Anz.Welten · Anz.Welten
Formelauswertung f¨
ur Modallogik geht in polynomieller Rechenzeit.
2.1.6
Eine modallogische Formel ϕ heißt g¨ultig (Schreibweise K ϕ), falls
f¨ur alle Kripke-Modelle M und alle Welten w in M gilt: M, w K ϕ.
Lemma 2.4 (Wichtige Eigenschaften der modalen Operatoren)
1.
2.
3.
4.
5.
6.
7.
8.
9.
K
(α → β) → (α → β)
K
(α → β) → (♦α → ♦β)
K
♦(α → β) ↔ (α → ♦β)
K
¬α ↔ ♦¬α
K
(α ∧ (α → β)) → β
K
(α ∧ β) ↔ (α ∧ β)
K
(α ∨ β) → (α ∨ β)
K
(♦α ∨ ♦β) ↔ ♦(α ∨ β)
K
♦(α ∧ β) → (♦α ∧ ♦β)
und
K
¬♦α ↔ ¬α
2.1.7
2.2 Der Tableau-Kalku
¨l fu
¨r Modallogik
2. Modale Aussagenlogik
Grundbegriffe
Tableau-Kalk¨
ul
Frege-Kalk¨
ul
Algorithmen
Mit dem Tableau-Kalk¨
ul beweist man die G¨
ultigkeit von Formeln.
[Literatur:
Priest: An introduction to non-classical logic.
Nerode, Shore: Logic for applications.]
2.2.1
Die Konstruktion eines Tableaus . . .
. . . entspricht in der Aussagenlogik einer systematischen Suche
nach einer erf¨ullenden Belegung der Startformel.
Entsprechend soll in der Modallogik nach einem Kripke-Modell
gesucht werden, das die Startformel in einer Welt erf¨ullt.
Grundlegende Beobachtung: es reicht, “Baum-Modelle” zu betrachten.
2.2.2
Tableau fu
¨r A → ♦A
als einf¨
uhrendes Beispiel
s A → ♦A
s ¬A
s ♦A
(s, u)
s ♦¬A
uA
(s, t)
t ¬A
2.2.3
Tableau fu
¨r A → ♦A
als einf¨
uhrendes Beispiel
s A → ♦A
s ¬A
s ♦A
(s, u)
s ♦¬A
uA
(s, t)
t ¬A
Aus den nicht-wid.Pfaden ergeben sich folgende Modelle:
s
t
2.2.3
Tableau fu
¨r A → ♦A
als einf¨
uhrendes Beispiel
s A → ♦A
s ¬A
s ♦A
(s, u)
s ♦¬A
uA
(s, t)
t ¬A
Aus den nicht-wid.Pfaden ergeben sich folgende Modelle:
s
t
s
A
u
2.2.3
Der Tableau-Kalku
¨l fu
¨r Modallogik
Der Tableau-Kalk¨
ul f¨
ur Aussagenlogik wird erweitert.
Beim aussagenlogischen Tableau-Kalk¨
ul geht es darum,
f¨
ur eine Formel einen Pfad durch das Tableau zu finden,
der einer erf¨
ullenden Belegung entspricht.
Beim modallogischen Tableau-Kalk¨
ul soll ein Pfad π durch das Tableau
gefunden werden,
der einem erf¨
ullenden Kripke-Modell (Wπ , Rπ , ξπ ) und
einer Welt s darin entspricht, in der die Formel erf¨
ullt wird.
Dazu werden die Tableaux erweitert.
1. Markierungen der Knoten haben die Form w α mit Welt w und
Formel α. Wπ ist die Menge aller Welten, die auf Pfad π vorkommen.
Der Startknoten des Tableaus f¨
ur α wird mit s α markiert.
2. Die Kanten des Tableaus werden teilweise mit Kanten zwischen Welten
markiert. Rπ ist die Menge aller Kantenmarkierungen auf dem Pfad π.
2.2.4
Zus¨
atzliche Expansionsregeln fu
¨r ♦ und Die Expansionsregel f¨
ur Knoten x mit Markierung v ♦α ist 2-teilig.
1.
v ♦α :
•
(v , w )
w α
wobei w eine Welt ist, die bisher nicht im Tableau vorkommt, und
2. auf jeden Pfad, der durch x l¨auft, und jeden Knoten mit Markierung v β
(f¨
ur beliebiges β) darauf wird die folgende Expansionsregel angewendet.
v β :
•
w β
Achtung: Diese Expansion von v β erfolgt auch, wenn der Knoten mit
dieser Markierung erst in einem sp¨ateren Expansionsschritt erzeugt wird!
2.2.5
. . . mit Negationen . . .
Expansionsregeln f¨ur negierte Modaloperatoren:
v ¬♦α :
•
v ¬α
und
v ¬α :
•
v ♦¬α
2.2.6
Tableau fu
¨r ¬(A → ♦A)
s ¬(A → ♦A)
s A
s ¬♦A
s ¬A
2.2.7
Tableau fu
¨r ¬(A → ♦A)
s ¬(A → ♦A)
s A
s
s ¬♦A
Erf¨ullendes Modell:
s ¬A
2.2.7
Tableau-Beweisbarkeit
Ein Pfad durch ein Tableau heißt widerspr¨uchlich, wenn er Markierungen
t α und t ¬α f¨ur eine Welt t und eine Formel α enth¨alt,
oder wenn er eine Markierung t ⊥ oder t ¬> enth¨alt.
Geschlossene Tableaux und widerspr¨uchliche Tableaux sind wie in der
Aussagenlogik definiert.
Definition 2.5 (Tableau-beweisbar)
Eine modallogische Formel α ist Tableau-beweisbar
(Schreibweise:
falls ¬α ein widerspr¨uchliches Tableau besitzt.
Tab
α),
2.2.8
Tab
(A → B) → (A → B)
s ¬((A → B) → (A → B))
s (A → B)
s ¬(A → B)
s A
s ¬B
s ♦¬B
(s, t)
t ¬B
tA→B
tA
t ¬A
×
tB
×
2.2.9
Zum Beweis des Korrektheitslemmas . . .
. . . gehen wir im Prinzip genauso vor wie bei der Aussagenlogik,
m¨ussen aber die dort verwendeten Ideen anpassen.
In der Aussagenlogik hatten wir:
I
Wenn α von Belegung A erf¨ullt wird, dann gibt es einen Pfad
durch das Tableau, auf dem jede Formel von A erf¨ullt wird.
Das erfordert in der Modallogik mehr Aufwand.
s A → ♦A
s ¬A
s ♦¬A
(s, t)
t ¬A
s ♦A
(s, u)
uA
Modelle aus dem Tableau:
A
ein weiteres erf¨
ullendes Modell:
A
2.2.10
Zum Beweis des Korrektheitslemmas . . .
s A → ♦A
s ¬A
s ♦¬A
(s, t)
t ¬A
s ♦A
(s, u)
uA
Modelle aus dem Tableau:
A
ein weiteres erf¨
ullendes Modell:
A
Definition 2.6 (Treue eines Tableau-Pfades zu einem Modell)
Sei M = (U, S, ξ) ein Kripke-Modell und T ein modales Tableau.
Ein Pfad π durch T heißt M-treu, falls es eine Abbildung f : Wπ → U
gibt, so dass
1. f¨ur jede Knotenmarkierung v α auf π gilt M, f (v )
K
α, und
2. f¨ur jede Kantenmarkierung (a, b) auf π gilt (f (a), f (b)) ∈ S.
2.2.10
Lemma 2.7 (Expansion erh¨
alt M-Treue)
Sei ϕ eine modallogische Formel,
M ein Kripke-Modell mit Welt s und M, s K ϕ.
Sei T ein modales Tableau f¨ur ϕ,
und T 0 entstehe aus T durch Expansion eines Knotens.
Falls T einen M-treuen Pfad besitzt, dann besitzt auch T 0 einen.
Beweis:
Sei T ein modales Tableau f¨ur ϕ, und M = (U, S, ξ).
Sei π ein M-treuer Pfad durch T , und fπ : Wπ → U die zugeh¨orige
Abbildung.
Falls T 0 aus T durch Expansion eines Knotens entsteht, der nicht auf π
liegt, dann bleibt π ein M-treuer Pfad durch T 0 .
2.2.11
Entstehe T 0 also durch Expansion eines Knotens u ψ auf π.
Fall 1: ψ = ¬α, wobei α nicht mit ♦ beginnt,
oder ψ = α ∧ β oder ψ = α ∨ β.
Dann ist Wπ0 = Wπ , und wir definieren fπ0 = fπ .
Es kann wie im aussagenlogischen Fall (Beweis von Lemma 1.18)
argumentiert werden.
Fall 2: ψ = ♦α, d.h. Knoten u ♦α auf Pfad π wird expandiert, d.h.
an π werden u 0 α und u 0 β1 , . . . , u 0 βk angeh¨angt.
Diesen Pfad durch T 0 nennen wir π 0 .
Dann ist Wπ0 = Wπ ∪ {u 0 } und Rπ0 = Rπ ∪ {(u, u 0 )}.
Da π M-treu ist, gilt M, fπ (u) K ♦α.
Gem¨aß der Semantik von ♦
gibt es ein v ∈ U mit (fπ (u), v ) ∈ S und M, v K α.
Definiere fπ0 : Wπ0 → U wie fπ erweitert um fπ0 (u 0 ) := v .
2.2.12
Wir zeigen nun, dass π 0 M-treu mittels fπ0 ist.
1.) F¨ur alle Knoten w γ auf π gilt M, fπ0 (w ) K γ,
da w ∈ Wπ , π M-treu ist und fπ0 auf Wπ wie fπ ist.
F¨ur u 0 α auf π 0 gilt M, fπ0 (u 0 )
K
α, da fπ0 (u 0 ) = v .
F¨ur jeden Knoten u βi auf π 0 gilt M, fπ0 (u) K βi .
Da (fπ0 (u), fπ0 (u 0 )) ∈ S, folgt M, fπ0 (u 0 ) K βi (gem¨aß Semantik von ).
2.) (fπ0 (a), fπ0 (b)) ∈ S f¨ur alle (a, b) ∈ Rπ , und (fπ0 (u), fπ0 (u 0 )) ∈ S.
Also ist der expandierte Pfad π 0 M-treu.
[Ende von Fall 2]
2.2.13
Fall 3: ψ = ¬♦α, d.h. Knoten u ¬♦α auf π wird expandiert, d.h.
an π werden u ¬α und t1 ¬α, . . . , tk ¬α angeh¨angt
f¨ur alle (u, t1 ), . . . , (u, tk ) ∈ Rπ .
0
Diesen Pfad durch T nennen wir π 0 .
Dann ist Wπ0 = Wπ und Rπ0 = Rπ , und wir definieren fπ0 = fπ .
Zum Beweis der M-Treue von π 0 reicht es, M, fπ0 (x) K γ f¨ur alle an π
angeh¨angten Knoten x γ zu zeigen.
1.) Da M, fπ0 (u)
K
¬♦α, folgt M, fπ0 (u)
K
¬α
(wg. ¬♦α ≡ ¬α).
2.) Daraus folgt M, v K ¬α f¨ur alle v ∈ U mit (fπ0 (u), v ) ∈ S.
Da (fπ0 (u), fπ0 (ti )) ∈ S,
folgt M, fπ0 (ti ) K ¬α f¨ur alle i = 1, 2, . . . , k.
Also ist π 0 ebenfalls M-treu.
X
2.2.14
Lemma 2.8 (Korrektheitslemma f¨
ur
Tab
)
Sei α eine modallogische Formel.
Wenn Tab α, dann ist α g¨ultig.
Beweis:
Wir beweisen die Kontraposition.
Sei α nicht g¨ultig, d.h. ¬α ist erf¨ullbar.
Dann gibt es ein Kripke-Modell M0 mit Welt s, so dass M0 , s K ¬α.
Das Tableau aus einen Knoten s ¬α
hat dann einen M0 -treuen Pfad (aus dem einen Knoten).
Jedes Tableau f¨ur ¬α hat einen solchen Knoten als Wurzel.
Nach Lemma 2.7 hat jedes Tableau f¨ur ¬α einen M0 -treuen Pfad.
Also gibt es kein widerspr¨uchliches Tableau f¨ur ¬α, d.h. Tab
6
¬α. X
2.2.15
Lemma 2.9 (Pfad bestimmt Modell)
Sei T ein modales Tableau f¨ur eine Formel ϕ, und π ein nichtwiderspr¨uchlicher Pfad durch T , auf dem jeder Knoten expandiert ist.
Dann gilt f¨ur das Kripke-Modell Mπ = (Wπ , Rπ , ξπ )
mit ξπ (w ) = {Ai | f¨ur ein w ∈ Wπ kommt w Ai auf π vor }:
f¨ur jede Markierung w α auf π gilt Mπ , w K α.
Beweis: sei π ein solcher Pfad mit der Knotenfolge π1 , . . . , π` .
Wir zeigen induktiv, dass die Behauptung f¨ur jedes πi gilt.
IA: i = `. (D.h. wir betrachten den Knoten π` am Ende von π.)
Fall 1: π` hat Markierung w >, w ¬⊥ oder w L f¨
ur ein Literal L.
Es gilt Mπ ,w K >, Mπ ,w K ¬⊥, und Mπ , w K L
aufgrund der Definition von ξπ und der Nicht-Widerspr¨
uchlichkeit von π.
Fall 2: π` ist ein Knoten mit Markierung w β.
Da π` nicht expandiert werden musste, hat w keinen Nachfolger in Rπ .
Also gilt M, w K β.
Eine andere Markierung kann π` nicht haben.
2.2.16
IV: F¨ur πk , πk+1 , . . . , π` gilt die Behauptung.
IS: i = k − 1. πk−1 habe Markierung w α.
Fall 1: α ist >, ¬⊥, ein Literal,
oder α = β und w hat keinen Nachfolger in Rπ .
Dann geht die Argumentation wie im IA.
Fall 2: α ist (β ∧ γ), ¬(β ∧ γ), (β ∨ γ), ¬(β ∨ γ) oder ¬¬β:
Dann wird α “klassisch” aussagenlogisch expandiert und die
Argumentation ist wie im aussagenlogischen Fall (Beweis zu 1.20).
Fall 3: α = ♦β.
Da πk−1 expandiert ist,
gibt es ein πj mit Markierung t β und j > k − 1, und (w , t) ∈ Rπ .
Nach IV gilt Mπ , t K β, und daraus folgt Mπ , w K ♦β.
2.2.17
Fall 4: α = β und w hat mindestens einen Nachfolger.
F¨ur jede Kante (w , t) ∈ Rπ gilt:
Es gibt ein πj mit j > k − 1 und Markierung t β.
Nach IV gilt dann Mπ , t K β.
Also folgt Mπ , w K β.
Fall 5: α = ¬♦β.
Dann gibt es ein πj mit j > k − 1 und Markierung w ¬β.
Nach IV gilt Mπ , w K ¬β, und daraus folgt Mπ , w K ¬♦β.
Fall 6: α = ¬β.
Dann gibt es ein πj mit j > k − 1 und Markierung w ♦¬β.
Nach IV gilt Mπ , w K ♦¬β, und daraus folgt Mπ , w K ¬β.
X
2.2.18
Lemma 2.10 (Vollst¨
andigkeit des modalen Tableau-Kalk¨
uls)
Sei α eine modallogische Formel.
Wenn α g¨ultig ist, dann Tab α.
Beweis:
Wir beweisen die Kontraposition.
Sei Tab
6
α.
Dann besitzt ¬α kein widerspr¨uchliches Tableau.
Da jedes Tableau zu einem endlichen geschlossenen Tableau erweitert
werden kann,
besitzt ¬α ein endliches nicht-widerspr¨uchliches geschlossenes Tableau.
Also enth¨alt das Tableau einen nicht-widerspr¨uchlichen Pfad, auf dem
jeder Knoten expandiert ist.
Nach Lemma 2.9 ist dieser Pfad M-treu f¨ur ein Modell M.
Folglich gibt es in M eine Welt s mit M, s K ¬α.
Also ist α nicht g¨ultig.
X
Zusammenfassung: der Vollst¨
andigkeitssatz
Satz 2.11 (Vollst¨
andigkeitssatz f¨
ur den modalen Tableau-Kalk¨
ul)
F¨ur alle modallogischen Formeln α gilt:
α ist g¨ultig
genau dann, wenn
jedes geschlossene Tableau f¨ur ¬α widerspr¨uchlich ist.
Beweis:
Folgt aus Lemmas 2.8 und 2.10.
X
2.3 Ein Frege-Kalku
¨l fu
¨r Modallogik
2. Modale Aussagenlogik
Grundbegriffe
Tableau-Kalk¨
ul
Frege-Kalk¨
ul
Algorithmen
Mit dem Frege-Kalk¨
ul beweist man die G¨
ultigkeit von Formeln.
[Literatur:
Halpern & Moses: A guide to completeness and complexity of modal logic.]
Ein Frege-Kalku
¨l fu
¨r Modallogik
I
I
Formeln MF: Formeln aus Atomen Ai , ⊥, → und .
¬α wird als abk¨urzende Schreibweise f¨ur α → ⊥ benutzt.
Axiome MAx f¨ur alle α, β, ϕ ∈ MF:
(A1)
(A2)
(A3)
(K)
I
α → (β → α)
(α → (β → ϕ)) → ((α → β) → (α → ϕ))
(¬β → ¬α) → ((¬β → α) → β)
(α → β) → (α → β)
Schlussregeln: modus ponens (MP) und Generalisierung (Gen)
α, α → β
MP(α, α → β, β),
auch beschrieben durch
β
α
Gen(α, α),
auch beschrieben durch
α
Fre
α bedeutet
“α ist Theorem dieses modallogischen Frege-Kalk¨uls”
(“α ist in Fre beweisbar”).
2.3.2
Lemma 2.12
F¨ur alle modallogischen Formeln α gilt
1.
2.
Fre
¬¬α → ¬¬α und
Fre
¬¬α → ¬¬α.
Beweis:
(1)
(2)
(3)
(4)
(5)
(6)
α → ¬¬α
(α → ¬¬α)
(α → ¬¬α) → (α → ¬¬α)
α → ¬¬α
¬¬α → α
¬¬α → ¬¬α
¨
(Teil 2 ist Ubungsaufgabe.)
(Theorem)
Gen (1)
(K)
MP (2), (3)
(Theorem)
TRANS (5), (4)
X
2.3.3
Korrektheit von
Fre
fu
¨r Modallogik
Lemma 2.13 (Korrektheitslemma f¨
ur
Fre
)
Sei α eine modallogische Formel.
Aus Fre α folgt K α.
Beweis:
Wir erweitern den Beweis des Korrektheitslemmas f¨ur Fre (1.34)
von “Belegung A erf¨ullt α” auf “Kripke-Modell M erf¨ullt α in Welt u”.
Die Argumentation im Beweis von Lemma 1.34 geht damit genauso.
Zus¨atzlich muss folgendes gezeigt werden.
1. Im Induktionsanfang muss gezeigt werden, dass (K) g¨ultig ist.
2. Im Induktionsschluss muss die Korrektheit der Regel Gen gezeigt
werden.
2.3.4
zu 1.) Erweiterung des Induktionsanfangs:
Wir zeigen die G¨
ultigkeit von (K).
Sei M = (W , R, ξ) ein Kripke-Modell und u ∈ W .
M, u
K
(α → β) → (α → β)
⇔ M, u 6 K (α → β) oder M, u 6 K α oder M, u
K
β
⇔ ∃v , (u, v ) ∈ R : M, v 6 K α → β oder ∃v , (u, v ) ∈ R : M, v 6 K α
oder M, u
K
β
⇔ ∃v , (u, v ) ∈ R : ((M, v
oder M, u
K
K
α und M, v 6 K β) oder M, v 6 K α)
β
⇔ ∃v , (u, v ) ∈ R : (M, v 6 K β oder M, v 6 K α)
oder M, u
K
β
⇔ ∃v , (u, v ) ∈ R : M, v 6 K α oder M, u 6 K β oder M, u
⇔ M, u
K
β oder M, u 6 K β
(wahre Aussage)
K
β
(X)
2.3.5
zu 2.) Erweiterung des Induktionsschritts f¨ur Gen:
Sei
α
α
die im letzten Beweisschritt benutzte Regel.
Zu zeigen ist: wenn α g¨ultig ist, dann ist auch α g¨ultig.
d.h. M, u
Sei α g¨ultig,
K
α f¨ur alle M und u.
W¨ahle M = (U, R, ξ) und v ∈ U beliebig.
Da M, u
K
α f¨ur alle u mit (v , u) ∈ R,
folgt M, v
K
α.
Da M und v beliebig gew¨ahlt wurden, ist α g¨ultig.
X
2.3.6
Das Deduktionstheorem von
(1)
(2) α
(3) α
Fre
Fre
Fre
α→α
α
α
(geht wie bei
Fre
Fre
geht nicht bei
Fre
)
(Anwendung des DT “von rechts nach links” geht wie bei
(Gen liefert einen nicht-korrekten Sequenten, da α
Man kann bei Beweisen in
Fre
das Deduktionstheorem von
Fre
)
α)
K
Fre
benutzen,
wenn man Gen nur auf Sequenten ohne Hypothesen anwendet.
2.3.7
Verallgemeinerung von (K)
Lemma 2.14
F¨ur jedes k ≥ 1 und alle Formeln α1 , . . . , αk , β gilt
(α1 → (α2 → (α3 → . . . (αk → β) . . .))) →
Fre
(α1 → (α2 → (α3 → . . . (αk → β) . . .)))
Beweis mittels Induktion u¨ber k.
IA k = 1: das ist Axiom (K) X
2.3.8
IS:
(1)
(2)
(3)
Fre
(α1 → (α2 → (α3 → . . . (αk+1 → β) . . .))) →
(α1 → (α2 → (α3 → . . . (αk+1 → β) . . .)))
(α1 → (α2 → (α3 → . . . (αk+1 → β) . . .))), α1 Fre
(α2 → (α3 → . . . (αk+1 → β) . . .))
Fre
(α2 → (α3 → (α4 → . . . (αk+1 → β) . . .))) →
(α2 → (α3 → (α4 → . . . (αk+1 → β) . . .)))
(K)
(DT)
(IV)
(4) (α1 → (α2 → (α3 → . . . (αk+1 → β) . . .))), α1 Fre
α2 → (α3 → . . . (αk+1 → β) . . .) (MP 2,3)
(5)
Fre
(α1 → (α2 → (α3 → . . . (αk+1 → β) . . .))) →
(α1 → (α2 → (α3 → . . . (αk+1 → β) . . .)))
Da Gen nicht benutzt wurde, ist die Anwendung des
Deduktionstheorems korrekt.
(DT)
X
2.3.9
Ein Konsistenzbegriff fu
¨r
Fre
Die N¨utzlichkeit des Konsistenzbegriffs f¨ur Fre beruht auf der
Benutzbarkeit des Deduktionstheorems (siehe z.B. Beweis von Lemma 1.40).
Deshalb brauchen wir f¨ur Fre einen anderen.
Definition 2.15 ( Fre -Konsistenz)
Eine modallogische Formelmenge A heißt Fre -konsistent,
falls f¨ur jede endliche Teilmenge {α1 , . . . , αk } von A gilt:
6
Fre
α1 → (α2 → (. . . → (αk → ⊥) . . .))
Bemerkungen:
(a) α1 → (α2 → (. . . → (αk → ⊥) . . .)) ≡ αi1 → (αi2 → (. . . → (αik → ⊥) . . .))
f¨
ur alle Permutationen der Indizes.
(b) Eine aussagenlog. Menge A ist
Fre -konsistent
gdw. sie
Fre
-konsistent ist.
Lemma 2.16
Wenn Γ Fre
6
α , dann ist Γ ∪ {¬α}
Fre
-konsistent.
Beweis (Kontraposition):
Sei Γ ∪ {¬α} nicht
Fre
-konsistent.
Dann folgt Fre α1 → (α2 → (. . . → (αk → ⊥) . . .))
f¨ur eine Formelmenge {α1 , . . . , αk } ⊆ Γ ∪ {¬α}.
Daraus folgt {α1 , . . . , αk }
Fre
⊥.
Mit ⊥ → α erhalten wir {α1 , . . . , αk }
Damit folgt insgesamt Γ
Fre
α.
Fre
α.
X
2.3.11
Maximal
Fre
-konsistente Mengen
Der Begriff maximal konsistenter Mengen wird aus der Aussagenlogik
u¨bernommen.
Definition 2.17 (maximale Konsistenz)
Eine Formelmenge A heißt maximal Fre -konsistent,
falls jede echte Obermenge von A nicht Fre -konsistent ist.
Sei α eine modallogische Formel.
Eine konsistente Menge Γ ⊆ Tfn(α) heißt α-maximal Fre -konsistent,
wenn keine Menge A mit Γ ( A ⊆ Tfn(α) Fre -konsistent ist.
2.3.12
Eigenschaften maximal
Fre
-konsistenter Mengen
Lemma 2.18
Sei α eine modallogische Formel.
Jede Fre -konsistente Menge Γ ⊆ Tfn (α)
besitzt eine α-maximal Fre -konsistente Obermenge.
Beweis: wie im aussagenlogischen Fall (Lemma 1.44).
X
2.3.13
Max. konsist. Mengen sind wie Welten in Modellen
Lemma 2.19
Sei α eine modallogische Formel und A sei α-maximal Fre -konsistent.
F¨ur jedes ϕ ∈ Tf (α) gilt: entweder ϕ ∈ A oder ¬ϕ ∈ A.
Beweis: Sei A α-maximal Fre -konsistent,
und es gibt ein ϕ ∈ Tf (α) mit ϕ, ¬ϕ 6∈ A oder ϕ, ¬ϕ ∈ A.
Fall (1): ϕ, ¬ϕ 6∈ A.
Dann sind A ∪ {ϕ} und A ∪ {¬ϕ} nicht Fre -konsistent,
und es folgt Fre α1 → (α2 → (. . . → (αk−1 → ¬ϕ) . . .))
und Fre ¬ϕ → (β1 → (β2 → (. . . → (βq−1 → ⊥) . . .))) f¨
ur αi , βj ∈ A.
Mit der Verallgemeinerung von TRANS (1.31) folgt
α1 → (. . . → (αk−1 → (β1 → (. . . → (βq−1 → ⊥) . . .))) . . .).
Fre
Also ist A nicht Fre -konsistent: Widerspruch zur Voraussetzung.
Fall (2): ϕ, ¬ϕ ∈ A.
Wegen Fre ¬ϕ → ¬ϕ (1.24) ist A nicht konsistent: Widerspruch.
X
Lemma 2.20
Sei α eine modallogische Formel und A sei α-maximal Fre -konsistent.
F¨ur jedes β → γ ∈ Tf (α) gilt: β → γ ∈ A gdw. β 6∈ A oder γ ∈ A.
Beweis:
Sei A α-maximal
Fre
-konsistent.
“⇒”:
Sei β → γ ∈ A und β ∈ A. Zu zeigen: γ ∈ A.
Annahme: γ 6∈ A.
Da γ ∈ Tf(α), ist ¬γ ∈ A (Lemma 2.19).
Mit Fre β → (¬γ → ¬(β → γ)) (Satz 1.32(7))
folgt, dass A nicht konsistent ist: Widerspruch zur Annahme.
Also folgt γ ∈ A.
“⇐”:
(1) Sei β 6∈ A. Zu zeigen: β → γ ∈ A.
Ann.: β → γ 6∈ A.
Dann ist ¬β ∈ A und ¬(β → γ) ∈ A (Lemma 2.19).
Aus Fre ¬β → (β → γ) (Satz 1.32(4))
folgt Fre ¬β → ¬¬(β → γ) (mit Satz 1.32(3) und (TRANS)).
Also ist A nicht konsistent: Widerspruch zur Voraussetzung.
Damit folgt β → γ ∈ A.
(2) Sei γ ∈ A. Zu zeigen: β → γ ∈ A.
Ann.: β → γ 6∈ A. Dann ist ¬(β → γ) ∈ A (Lemma 2.19).
Aus Fre γ → (β → γ) (A1)
folgt Fre γ → ¬¬(β → γ) (mit Satz 1.32(3) und (TRANS)).
Also ist A nicht konsistent: Widerspruch zur Voraussetzung.
Damit folgt β → γ ∈ A.
X
2.3.16
Vollst¨
andigkeit von
Fre
fu
¨r Modallogik
Lemma 2.21 (Vollst¨
andigkeitslemma f¨
ur
Fre
)
Sei ϕ eine modallogische Formel. Falls ϕ g¨ultig ist, folgt
Fre
ϕ.
Beweis:
Wir zeigen die Kontraposition:
aus Fre
6
ϕ folgt,
dass es ein Modell Mϕ mit einer Welt uϕ gibt, so dass Mϕ , uϕ 6 K ϕ.
2.3.17
Zuerst konstruieren wir das gesuchte Modell Mϕ = (C , R, ξ) wie folgt.
1. C = die Menge aller ϕ-maximal
-konsistenten Teilmengen
von Tfn(ϕ).
Jede Welt w ist also eine Menge von modallogischen Formeln.
Fre
2. (u, v ) ∈ R genau dann, wenn {α | α ∈ u} ⊆ v
3. ξ(w ) = {Ai | Ai ∈ w }
(f¨
ur alle u, v ∈ C ).
(f¨
ur jedes w ∈ C ).
2.3.18
Beobachtung
F¨ur alle α ∈ Tfn (ϕ) gilt: Mϕ , u
K
α genau dann, wenn α ∈ u.
Beweis mittels Induktion u¨ber Formelaufbau.
IA: α ist Atom oder ⊥: Beobachtung gilt wg. der Definition von ξ.
IS: Fall 1: α = β → γ:
β→γ∈u
gdw. β 6∈ u oder γ ∈ u
gdw. Mϕ , u 6 K β oder Mϕ , u
gdw. Mϕ , u K β → γ
(Lemma 2.20)
K
γ
(IV)
(Semantik von →)
Fall 2: α = β:
(1) β ∈ u
⇒ f¨ur alle v ∈ C , (u, v ) ∈ R : β ∈ v
⇒ f¨ur alle v ∈ C , (u, v ) ∈ R : Mϕ , v
⇒ Mϕ , u K β
(Definition von R)
K
β
(IV)
(Semantik von )
2.3.19
(2) Mϕ , u
K
β
⇒
f¨
ur alle v ∈ C , (u, v ) ∈ R : Mϕ , v
⇒
f¨
ur alle v ∈ C , {α | α ∈ u} ⊆ v : β ∈ v
|
{z
}
K
β
(Semantik von )
(Def. von R, und IV)
=:Au
⇒
jede ϕ-maximal
⇒
Au ∪ {¬β} ist nicht
⇒
Gen
⇒
2.14
⇒
Fre
-konsistent
α1 → (α2 → (. . . → (αk−1 → ¬¬β) . . .)) f¨
ur αi ∈ Au
Fre
(α1 → (α2 → (. . . → (αk−1 → ¬¬β) . . .))) f¨
ur αi ∈ Au
α1 → (α2 → (. . . → (αk−1 → ¬¬β) . . .))
f¨
ur αi ∈ {α | α ∈ u}, d.h. αi ∈ u
Fre
Fre
α1 → (α2 → (. . . → (αk−1 → ¬¬β) . . .)) f¨
ur αi ∈ u
⇒
u ∪ {¬β} ist nicht
2.19
β ∈ u
⇒
-konsistente Erweiterung von Au enth¨alt β
Fre
1.31,2.12
⇒
Fre
Fre
-konsistent, also ¬β 6∈ u
X(Beobachtung)
2.3.20
Abschluss des Beweises des Vollst¨andigkeitslemmas:
Sei
6
Fre
ϕ.
Dann ist {¬ϕ}
Fre
-konsistent (Lemma 2.16) und {¬ϕ} ⊆ Tfn(ϕ).
Folglich gibt es eine
ϕ-maximal Fre -konsistente Obermenge uϕ von {¬ϕ} (Lemma 2.18).
Da ¬ϕ ∈ uφ , folgt Mϕ , uϕ
K
¬ϕ (Beobachtung)
und damit Mϕ , uϕ 6 K ϕ.
Das heißt: ϕ ist nicht g¨ultig.
X
2.3.21
Folgerungen aus dem Beweis
Um zu pr¨ufen, ob ϕ g¨ultig ist,
muss man nur pr¨ufen, ob ϕ in jeder Welt von Mϕ erf¨ullt wird.
Jede Welt von Mϕ ist eine Teilmenge von Tfn(ϕ)
und hat demnach Beschreibungsgr¨oße O(|ϕ|2 ).
Die Gr¨oße des Universums von Mϕ ist 2O(|ϕ|) .
Da Mϕ eindeutig durch ϕ beschrieben ist,
kann man die G¨ultigkeit von ϕ mit polynomiellem Speicherplatz pr¨ufen.
2.3.22
Zusammenfassung: der Vollst¨
andigkeitssatz
Satz 2.22 (Vollst¨
andigkeitssatz f¨
ur
Fre
)
Sei α eine modallogische Formel.
α ist g¨ultig genau dann, wenn Fre α.
Beweis:
Folgt aus Lemmas 2.13 und 2.21.
X
2.4 Algorithmen fu
¨r Modallogik
2. Modale Aussagenlogik
Grundbegriffe
Tableau-Kalk¨ul
Frege-Kalk¨ul
Algorithmen
Wir werden den Algorithmus, den wir f¨ur die Aussagenlogik
aus dem Tableau-Kalk¨ul entwickelt haben,
f¨ur die Modallogik erweitern.
2.4.1
Was passiert beim Aufbau eines Tableaus?
Wir wiederholen nochmal den aussagenlogischen Fall
Mit (fast) jedem Knoten ist eine Menge aus zerlegbaren Formeln und Literalen
verbunden.
¬[((A → C ) ∨ (B → C )) → ((A ∨ B) → C )]
(A → C ) ∨ (B → C )
¬((A ∨ B) → C )
A→C
B→C
A∨B
A∨B
¬C
¬C
¬A
A
×
¬B
C
×
B
A
C
×
B
×
2.4.2
Was passiert beim Aufbau eines Tableaus?
Wir wiederholen nochmal den aussagenlogischen Fall
Mit (fast) jedem Knoten ist eine Menge aus zerlegbaren Formeln und Literalen
verbunden.
{¬[((A → C ) ∨ (B → C )) → ((A ∨ B) → C )]}
(A → C ) ∨ (B → C )
¬((A ∨ B) → C )
A→C
B→C
A∨B
A∨B
¬C
¬C
¬A
A
×
¬B
C
×
B
A
C
×
B
×
2.4.2
Was passiert beim Aufbau eines Tableaus?
Wir wiederholen nochmal den aussagenlogischen Fall
Mit (fast) jedem Knoten ist eine Menge aus zerlegbaren Formeln und Literalen
verbunden.
{¬[((A → C ) ∨ (B → C )) → ((A ∨ B) → C )]}
{(A → C ) ∨ (B → C ), ¬((A ∨ B) → C )}
A→C
B→C
A∨B
A∨B
¬C
¬C
¬A
A
×
¬B
C
×
B
A
C
×
B
×
2.4.2
Was passiert beim Aufbau eines Tableaus?
Wir wiederholen nochmal den aussagenlogischen Fall
Mit (fast) jedem Knoten ist eine Menge aus zerlegbaren Formeln und Literalen
verbunden.
{¬[((A → C ) ∨ (B → C )) → ((A ∨ B) → C )]}
{(A → C ) ∨ (B → C ), ¬((A ∨ B) → C )}
{A → C , ¬((A ∨ B) → C )}
B→C
A∨B
A∨B
¬C
¬C
¬A
A
×
¬B
C
×
B
A
C
×
B
×
2.4.2
Was passiert beim Aufbau eines Tableaus?
Wir wiederholen nochmal den aussagenlogischen Fall
Mit (fast) jedem Knoten ist eine Menge aus zerlegbaren Formeln und Literalen
verbunden.
{¬[((A → C ) ∨ (B → C )) → ((A ∨ B) → C )]}
{(A → C ) ∨ (B → C ), ¬((A ∨ B) → C )}
{A → C , ¬((A ∨ B) → C )}
B→C
A∨B
{A → C , A ∨ B, ¬C }
¬A
A
×
¬C
¬B
C
×
B
A
C
×
B
×
2.4.2
Was passiert beim Aufbau eines Tableaus?
Wir wiederholen nochmal den aussagenlogischen Fall
Mit (fast) jedem Knoten ist eine Menge aus zerlegbaren Formeln und Literalen
verbunden.
{¬[((A → C ) ∨ (B → C )) → ((A ∨ B) → C )]}
{(A → C ) ∨ (B → C ), ¬((A ∨ B) → C )}
{A → C , ¬((A ∨ B) → C )}
B→C
A∨B
{A → C , A ∨ B, ¬C }
{¬A, A ∨ B, ¬C }
A
×
B
¬C
¬B
C
×
A
C
×
B
×
2.4.2
Was passiert beim Aufbau eines Tableaus?
Wir wiederholen nochmal den aussagenlogischen Fall
Mit (fast) jedem Knoten ist eine Menge aus zerlegbaren Formeln und Literalen
verbunden.
{¬[((A → C ) ∨ (B → C )) → ((A ∨ B) → C )]}
{(A → C ) ∨ (B → C ), ¬((A ∨ B) → C )}
{A → C , ¬((A ∨ B) → C )}
B→C
A∨B
{A → C , A ∨ B, ¬C }
{¬A, A ∨ B, ¬C }
{¬A, A, ¬C }
×
B
¬C
¬B
C
×
A
C
×
B
×
2.4.2
Was passiert beim Aufbau eines Tableaus?
Wir wiederholen nochmal den aussagenlogischen Fall
Mit (fast) jedem Knoten ist eine Menge aus zerlegbaren Formeln und Literalen
verbunden.
{¬[((A → C ) ∨ (B → C )) → ((A ∨ B) → C )]}
{(A → C ) ∨ (B → C ), ¬((A ∨ B) → C )}
{A → C , ¬((A ∨ B) → C )}
B→C
A∨B
{A → C , A ∨ B, ¬C }
{¬A, A ∨ B, ¬C }
{¬A, A, ¬C } {¬A, B, ¬C }
×
¬C
¬B
C
×
A
C
×
B
×
2.4.2
Was passiert beim Aufbau eines Tableaus?
Wir wiederholen nochmal den aussagenlogischen Fall
Mit (fast) jedem Knoten ist eine Menge aus zerlegbaren Formeln und Literalen
verbunden.
{¬[((A → C ) ∨ (B → C )) → ((A ∨ B) → C )]}
{(A → C ) ∨ (B → C ), ¬((A ∨ B) → C )}
{A → C , ¬((A ∨ B) → C )}
B→C
A∨B
{A → C , A ∨ B, ¬C }
{C , A ∨ B, ¬C }
×
{¬A, A, ¬C } {¬A, B, ¬C }
×
¬C
{¬A, A ∨ B, ¬C }
¬B
A
C
×
B
×
2.4.2
Was passiert beim Aufbau eines Tableaus?
Wir wiederholen nochmal den aussagenlogischen Fall
Mit (fast) jedem Knoten ist eine Menge aus zerlegbaren Formeln und Literalen
verbunden.
{¬[((A → C ) ∨ (B → C )) → ((A ∨ B) → C )]}
{(A → C ) ∨ (B → C ), ¬((A ∨ B) → C )}
{A → C , ¬((A ∨ B) → C )}
{B → C , ¬((A ∨ B) → C )}
A∨B
{A → C , A ∨ B, ¬C }
{C , A ∨ B, ¬C }
×
{¬A, A, ¬C } {¬A, B, ¬C }
×
¬C
{¬A, A ∨ B, ¬C }
¬B
A
C
×
B
×
2.4.2
Was passiert beim Aufbau eines Tableaus?
Wir wiederholen nochmal den aussagenlogischen Fall
Mit (fast) jedem Knoten ist eine Menge aus zerlegbaren Formeln und Literalen
verbunden.
{¬[((A → C ) ∨ (B → C )) → ((A ∨ B) → C )]}
{(A → C ) ∨ (B → C ), ¬((A ∨ B) → C )}
{A → C , ¬((A ∨ B) → C )}
{B → C , ¬((A ∨ B) → C )}
{A → C , A ∨ B, ¬C }
{B → C , A ∨ B, ¬C }
{¬A, A ∨ B, ¬C }
{C , A ∨ B, ¬C }
×
{¬A, A, ¬C } {¬A, B, ¬C }
×
¬B
A
C
×
B
×
2.4.2
Was passiert beim Aufbau eines Tableaus?
Wir wiederholen nochmal den aussagenlogischen Fall
Mit (fast) jedem Knoten ist eine Menge aus zerlegbaren Formeln und Literalen
verbunden.
{¬[((A → C ) ∨ (B → C )) → ((A ∨ B) → C )]}
{(A → C ) ∨ (B → C ), ¬((A ∨ B) → C )}
{A → C , ¬((A ∨ B) → C )}
{B → C , ¬((A ∨ B) → C )}
{A → C , A ∨ B, ¬C }
{B → C , A ∨ B, ¬C }
{¬A, A ∨ B, ¬C }
{C , A ∨ B, ¬C }
×
{¬A, A, ¬C } {¬A, B, ¬C }
×
{¬B, A ∨ B, ¬C }
A
B
×
C
×
2.4.2
Was passiert beim Aufbau eines Tableaus?
Wir wiederholen nochmal den aussagenlogischen Fall
Mit (fast) jedem Knoten ist eine Menge aus zerlegbaren Formeln und Literalen
verbunden.
{¬[((A → C ) ∨ (B → C )) → ((A ∨ B) → C )]}
{(A → C ) ∨ (B → C ), ¬((A ∨ B) → C )}
{A → C , ¬((A ∨ B) → C )}
{B → C , ¬((A ∨ B) → C )}
{A → C , A ∨ B, ¬C }
{B → C , A ∨ B, ¬C }
{¬A, A ∨ B, ¬C }
{C , A ∨ B, ¬C } {¬B, A ∨ B, ¬C }
×
{¬A, A, ¬C } {¬A, B, ¬C }
{¬B, A, ¬C }
B
×
×
C
×
2.4.2
Was passiert beim Aufbau eines Tableaus?
Wir wiederholen nochmal den aussagenlogischen Fall
Mit (fast) jedem Knoten ist eine Menge aus zerlegbaren Formeln und Literalen
verbunden.
{¬[((A → C ) ∨ (B → C )) → ((A ∨ B) → C )]}
{(A → C ) ∨ (B → C ), ¬((A ∨ B) → C )}
{A → C , ¬((A ∨ B) → C )}
{B → C , ¬((A ∨ B) → C )}
{A → C , A ∨ B, ¬C }
{B → C , A ∨ B, ¬C }
{¬A, A ∨ B, ¬C }
{C , A ∨ B, ¬C } {¬B, A ∨ B, ¬C }
×
{¬A, A, ¬C } {¬A, B, ¬C }
{¬B, A, ¬C } {¬B, B, ¬C }
×
×
C
×
2.4.2
Was passiert beim Aufbau eines Tableaus?
Wir wiederholen nochmal den aussagenlogischen Fall
Mit (fast) jedem Knoten ist eine Menge aus zerlegbaren Formeln und Literalen
verbunden.
{¬[((A → C ) ∨ (B → C )) → ((A ∨ B) → C )]}
{(A → C ) ∨ (B → C ), ¬((A ∨ B) → C )}
{A → C , ¬((A ∨ B) → C )}
{B → C , ¬((A ∨ B) → C )}
{A → C , A ∨ B, ¬C }
{B → C , A ∨ B, ¬C }
{¬A, A ∨ B, ¬C }
{C , A ∨ B, ¬C } {¬B, A ∨ B, ¬C } {C , A ∨ B, ¬C }
×
×
{¬A, A, ¬C } {¬A, B, ¬C }
{¬B, A, ¬C } {¬B, B, ¬C }
×
×
2.4.2
Was kommt bei Modallogik dazu?
s ¬((A → B) → (A → B))
s ¬((A → B) → (A → B))
s (A → B)
s (A → B)
s ¬(A → B)
s ¬(A → B)
s A
s A
s ¬B
s ¬B
s ♦¬B
(s, t)
t ¬B
s ♦¬B
(s, t) ∈ R
t ¬B
t ¬A
×
tA→B
tA→B
tA
tA
tB
×
t ¬A
×
tB
×
Was kommt bei Modallogik dazu?
s ¬((A → B) → (A → B))
{¬((A → B) → (A → B))}
s (A → B)
s (A → B)
s ¬(A → B)
s ¬(A → B)
s A
s A
s ¬B
s ¬B
s ♦¬B
(s, t)
t ¬B
s ♦¬B
(s, t) ∈ R
t ¬B
t ¬A
×
tA→B
tA→B
tA
tA
tB
×
t ¬A
×
tB
×
Was kommt bei Modallogik dazu?
s ¬((A → B) → (A → B))
{¬((A → B) → (A → B))}
s (A → B)
t ¬A
×
s ¬(A → B)
{(A → B), ¬(A → B)}
s A
s A
s ¬B
s ¬B
s ♦¬B
(s, t)
t ¬B
s ♦¬B
(s, t) ∈ R
t ¬B
tA→B
tA→B
tA
tA
tB
×
t ¬A
×
tB
×
Was kommt bei Modallogik dazu?
s ¬((A → B) → (A → B))
{¬((A → B) → (A → B))}
s (A → B)
{(A → B), ¬(A → B)}
s ¬(A → B)
s A
{(A → B), A, ¬B}
s ¬B
s ♦¬B
(s, t) ∈ R
t ¬B
s ♦¬B
(s, t)
t ¬B
t ¬A
×
tA→B
tA→B
tA
tA
tB
×
t ¬A
×
tB
×
Was kommt bei Modallogik dazu?
s ¬((A → B) → (A → B))
{¬((A → B) → (A → B))}
s (A → B)
{(A → B), ¬(A → B)}
s ¬(A → B)
s A
t ¬A
×
s ¬B
{(A → B), A, ¬B}
s ♦¬B
(s, t)
t ¬B
{(A → B), A, ♦¬B}
(s, t) ∈ R
t ¬B
tA→B
tA→B
tA
tA
tB
×
t ¬A
×
tB
×
Was kommt bei Modallogik dazu?
s ¬((A → B) → (A → B))
{¬((A → B) → (A → B))}
s (A → B)
{(A → B), ¬(A → B)}
s ¬(A → B)
s A
s ¬B
{(A → B), A, ¬B}
s ♦¬B
(s, t)
t ¬B
{(A → B), A, ♦¬B}
(s, t) ∈ R
tA→B
{A → B, A, ¬B}
tA
t ¬A
×
tB
×
t ¬A
×
tB
×
Was kommt bei Modallogik dazu?
s ¬((A → B) → (A → B))
{¬((A → B) → (A → B))}
s (A → B)
{(A → B), ¬(A → B)}
s ¬(A → B)
s A
s ¬B
{(A → B), A, ¬B}
s ♦¬B
(s, t)
t ¬B
{(A → B), A, ♦¬B}
(s, t) ∈ R
tA→B
{A → B, A, ¬B}
tA
t ¬A
×
tB
×
{¬A, A, ¬B}
×
{B, A, ¬B}
×
Was kommt bei Modallogik dazu?
s C ∧ ♦A ∧ ♦B ∧ ¬B
{C ∧ ♦A ∧ ♦B ∧ ¬B}
sC
s ♦A
s ♦B
s ¬B
(s, t) ∈ R
tA
{C , ♦A, ♦B, ¬B}
t ¬B
(s, u) ∈ R
uB
{A, ¬B}
u ¬B
×
{B, ¬B}
×
Was kommt bei Modallogik dazu?
s C ∧ ♦A ∧ ♦B ∧ ¬B
{C ∧ ♦A ∧ ♦B ∧ ¬B}
sC
s ♦A
s ♦B
s ¬B
(s, t) ∈ R
tA
{C , ♦A, ♦B, ¬B}
t ¬B
(s, u) ∈ R
uB
{A, ¬B}
u ¬B
×
{B, ¬B}
×
min
Erweiterung der Typen fu
¨r Tableau-Knoten
f¨
ur modale Aussagenlogik
Typ 1 (keine Verzweigung)
wird erweitert um Knoten mit Markierungen ¬α und ¬♦α
Typ 2 (Verzweigung)
bleibt wie im aussagenlogischen Fall
Typ 3: Markierung t ♦α . . .
es werden Knoten angeh¨angt, die f¨
ur eine neue Welt u stehen
und die mit u α und jeweils einem u β markiert sind, f¨
ur
das ein Knoten mit Markierung t β auf dem Pfad liegt
Wenn man mit Mengen zu zerlegender Formeln arbeitet, ergibt sich:
I
Umgang mit Formeln vom Typ 1 und 2 wie gehabt
I
Umgang mit Formeln vom Typ 3:
f¨
ur jedes ♦α ersetze S durch
S♦α := {α} ∪ {ψ | ψ ∈ S}
und u
ufe, ob alle diese Mengen unabh¨angig voneinander erf¨
ullbar sind.
¨berp¨
2.4.5
Methode zum Bestimmen der
Zerlegungsformeln
f¨
ur modale aussagenlogische Formeln
Methodenaufruf mzerlege(ϕ,i) ergibt die i-te Zerlegungsformel von ϕ.
Methode mzerlege (Formel ϕ, Index i)
falls i = 1 dann
(∗ bestimme die erste Zerlegungsformel ∗)
falls ϕ ∈ {α ∧ β, α ∨ β, ¬(α → β), ¬¬α} dann return α
falls ϕ ∈ {¬(α ∧ β), ¬(α ∨ β), α → β} dann return ¬α
falls ϕ = ¬♦α dann return ¬α
falls ϕ = ¬α dann return ♦¬α
sonst
(∗ bestimme die zweite Zerlegungsformel ∗)
falls ϕ ∈ {α ∧ β, α ∨ β, α → β} dann return β
falls ϕ ∈ {¬(α ∧ β), ¬(α ∨ β), ¬(α → β)} dann return ¬β
Erfu
aß Tableau-Kalku
¨llbarkeitstest gem¨
¨l
f¨
ur modale aussagenlogische Formeln als rekursive Methode
Als Folgerung des Vollst¨andigkeitssatzes f¨
ur den Tableau-Kalk¨
ul der modalen
Aussagenlogik gilt:
Ein Aufruf merf¨
ullbar(S) liefert Ergebnis 1 gdw. es ein Kripke-Modell gibt, das alle
Formeln in S erf¨
ullt.
Methode merf¨
ullbar(Formelmenge S) {
falls S widerspr¨
uchlich ist dann return 0
falls S eine Formel ψ vom Typ 1 besitzt dann
return merf¨
ullbar((S − ψ) ∪ {mzerlege(ψ, 1), mzerlege(ψ, 2)})
sonst: falls S eine Formel ψ vom Typ 2 besitzt dann
return max merf¨
ullbar((S − ψ) ∪ {mzerlege(ψ, b)})
b∈{1,2}
sonst: falls S eine Formel vom Typ 3 enth¨
alt dann
return min merf¨
ullbar({β | β ∈ S} ∪ {α})
♦α∈S
sonst: (∗ S ist nicht widerspr¨uchlich und besteht aus Literalen ∗)
return 1
}
2.4.7
Struktur der rekursiven Aufrufe
f¨
ur merf¨
ullbar({♦A ∧ ♦¬A ∧ (A → A ∧ ¬A → ¬A ∧ ♦B ∧ ♦¬B)})
Wir schreiben abk¨
urzend me[X , Y , Z ] f¨
ur merf¨
ullbar({X , Y , Z }).
Rekursive Aufrufe f¨
ur Formeln vom Typ 1 sind nicht aufgef¨
uhrt.
me[♦A, ♦¬A, (A → A ∧ ¬A → ¬A ∧ ♦B ∧ ♦¬B)]
Struktur der rekursiven Aufrufe
f¨
ur merf¨
ullbar({♦A ∧ ♦¬A ∧ (A → A ∧ ¬A → ¬A ∧ ♦B ∧ ♦¬B)})
Wir schreiben abk¨
urzend me[X , Y , Z ] f¨
ur merf¨
ullbar({X , Y , Z }).
Rekursive Aufrufe f¨
ur Formeln vom Typ 1 sind nicht aufgef¨
uhrt.
me[♦A, ♦¬A, (A → A ∧ ¬A → ¬A ∧ ♦B ∧ ♦¬B)]
min
♦A
♦¬A
me[A, A → A, ¬A → ¬A, ♦B, ♦¬B]
me[¬A, A → A, ¬A → ¬A, ♦B, ♦¬B]
Struktur der rekursiven Aufrufe
f¨
ur merf¨
ullbar({♦A ∧ ♦¬A ∧ (A → A ∧ ¬A → ¬A ∧ ♦B ∧ ♦¬B)})
Wir schreiben abk¨
urzend me[X , Y , Z ] f¨
ur merf¨
ullbar({X , Y , Z }).
Rekursive Aufrufe f¨
ur Formeln vom Typ 1 sind nicht aufgef¨
uhrt.
me[♦A, ♦¬A, (A → A ∧ ¬A → ¬A ∧ ♦B ∧ ♦¬B)]
min
♦A
♦¬A
me[A, A → A, ¬A → ¬A, ♦B, ♦¬B]
max
¬A
A → A A
me[A, ¬A, . . .]
=0
me[¬A, A → A, ¬A → ¬A, ♦B, ♦¬B]
me[A, A, ¬A → ¬A, ♦B, ♦¬B]
Struktur der rekursiven Aufrufe
f¨
ur merf¨
ullbar({♦A ∧ ♦¬A ∧ (A → A ∧ ¬A → ¬A ∧ ♦B ∧ ♦¬B)})
Wir schreiben abk¨
urzend me[X , Y , Z ] f¨
ur merf¨
ullbar({X , Y , Z }).
Rekursive Aufrufe f¨
ur Formeln vom Typ 1 sind nicht aufgef¨
uhrt.
me[♦A, ♦¬A, (A → A ∧ ¬A → ¬A ∧ ♦B ∧ ♦¬B)]
min
♦A
♦¬A
me[A, A → A, ¬A → ¬A, ♦B, ♦¬B]
max
¬A
A → A A
me[A, ¬A, . . .]
=0
me[¬A, A → A, ¬A → ¬A, ♦B, ♦¬B]
me[A, A, ¬A → ¬A, ♦B, ♦¬B]
max
¬¬A ¬A → ¬A ¬A
me[A, A, ♦B, ♦¬B]
me[A, A, ¬A, ♦B, ♦¬B]
Struktur der rekursiven Aufrufe
f¨
ur merf¨
ullbar({♦A ∧ ♦¬A ∧ (A → A ∧ ¬A → ¬A ∧ ♦B ∧ ♦¬B)})
Wir schreiben abk¨
urzend me[X , Y , Z ] f¨
ur merf¨
ullbar({X , Y , Z }).
Rekursive Aufrufe f¨
ur Formeln vom Typ 1 sind nicht aufgef¨
uhrt.
me[♦A, ♦¬A, (A → A ∧ ¬A → ¬A ∧ ♦B ∧ ♦¬B)]
min
♦A
♦¬A
me[A, A → A, ¬A → ¬A, ♦B, ♦¬B]
max
¬A
A → A A
me[A, ¬A, . . .]
=0
me[¬A, A → A, ¬A → ¬A, ♦B, ♦¬B]
me[A, A, ¬A → ¬A, ♦B, ♦¬B]
max
¬¬A ¬A → ¬A ¬A
me[A, A, ♦B, ♦¬B]
min
♦B
♦¬B
me[A, B]
=1
me[A, ¬B]
=1
me[A, A, ¬A, ♦B, ♦¬B]
Struktur der rekursiven Aufrufe
f¨
ur merf¨
ullbar({♦A ∧ ♦¬A ∧ (A → A ∧ ¬A → ¬A ∧ ♦B ∧ ♦¬B)})
Wir schreiben abk¨
urzend me[X , Y , Z ] f¨
ur merf¨
ullbar({X , Y , Z }).
Rekursive Aufrufe f¨
ur Formeln vom Typ 1 sind nicht aufgef¨
uhrt.
me[♦A, ♦¬A, (A → A ∧ ¬A → ¬A ∧ ♦B ∧ ♦¬B)]
min
♦A
♦¬A
me[A, A → A, ¬A → ¬A, ♦B, ♦¬B]
max
¬A
A → A A
me[A, ¬A, . . .]
=0
me[¬A, A → A, ¬A → ¬A, ♦B, ♦¬B]
me[A, A, ¬A → ¬A, ♦B, ♦¬B]
max
¬¬A ¬A → ¬A ¬A
me[A, A, ♦B, ♦¬B]
min
♦B
♦¬B
me[A, B]
=1
me[A, A, ¬A, ♦B, ♦¬B]
min
♦B
♦¬B
me[A, ¬B] me[A, ¬A, B] me[A, ¬A, ¬B]
=1
=0
=0
Struktur der rekursiven Aufrufe
f¨
ur merf¨
ullbar({♦A ∧ ♦¬A ∧ (A → A ∧ ¬A → ¬A ∧ ♦B ∧ ♦¬B)})
Wir schreiben abk¨
urzend me[X , Y , Z ] f¨
ur merf¨
ullbar({X , Y , Z }).
Rekursive Aufrufe f¨
ur Formeln vom Typ 1 sind nicht aufgef¨
uhrt.
me[♦A, ♦¬A, (A → A ∧ ¬A → ¬A ∧ ♦B ∧ ♦¬B)]
min
♦A
♦¬A
me[A, A → A, ¬A → ¬A, ♦B, ♦¬B]
.
..
=1
me[¬A, A → A, ¬A → ¬A, ♦B, ♦¬B]
Struktur der rekursiven Aufrufe
f¨
ur merf¨
ullbar({♦A ∧ ♦¬A ∧ (A → A ∧ ¬A → ¬A ∧ ♦B ∧ ♦¬B)})
Wir schreiben abk¨
urzend me[X , Y , Z ] f¨
ur merf¨
ullbar({X , Y , Z }).
Rekursive Aufrufe f¨
ur Formeln vom Typ 1 sind nicht aufgef¨
uhrt.
me[♦A, ♦¬A, (A → A ∧ ¬A → ¬A ∧ ♦B ∧ ♦¬B)]
min
♦A
♦¬A
me[A, A → A, ¬A → ¬A, ♦B, ♦¬B]
.
..
=1
me[¬A, A → A, ¬A → ¬A, ♦B, ♦¬B]
max
¬A
A → A A
me[¬A, ¬A → ¬A, ♦B, ♦¬B]
me[¬A, A, ¬A → ¬A, ♦B, ♦¬B]
Struktur der rekursiven Aufrufe
f¨
ur merf¨
ullbar({♦A ∧ ♦¬A ∧ (A → A ∧ ¬A → ¬A ∧ ♦B ∧ ♦¬B)})
Wir schreiben abk¨
urzend me[X , Y , Z ] f¨
ur merf¨
ullbar({X , Y , Z }).
Rekursive Aufrufe f¨
ur Formeln vom Typ 1 sind nicht aufgef¨
uhrt.
me[♦A, ♦¬A, (A → A ∧ ¬A → ¬A ∧ ♦B ∧ ♦¬B)]
min
♦A
♦¬A
me[A, A → A, ¬A → ¬A, ♦B, ♦¬B]
.
..
=1
me[¬A, A → A, ¬A → ¬A, ♦B, ♦¬B]
max
¬A
A → A A
me[¬A, ¬A → ¬A, ♦B, ♦¬B]
max
¬¬A
¬A → ¬A ¬A
me[¬A, A, ♦B, ♦¬B]
=0
me[¬A, A, ¬A → ¬A, ♦B, ♦¬B]
me[¬A, ¬A, ♦B, ♦¬B]
Struktur der rekursiven Aufrufe
f¨
ur merf¨
ullbar({♦A ∧ ♦¬A ∧ (A → A ∧ ¬A → ¬A ∧ ♦B ∧ ♦¬B)})
Wir schreiben abk¨
urzend me[X , Y , Z ] f¨
ur merf¨
ullbar({X , Y , Z }).
Rekursive Aufrufe f¨
ur Formeln vom Typ 1 sind nicht aufgef¨
uhrt.
me[♦A, ♦¬A, (A → A ∧ ¬A → ¬A ∧ ♦B ∧ ♦¬B)]
min
♦A
♦¬A
me[A, A → A, ¬A → ¬A, ♦B, ♦¬B]
.
..
=1
me[¬A, A → A, ¬A → ¬A, ♦B, ♦¬B]
max
¬A
A → A A
me[¬A, ¬A → ¬A, ♦B, ♦¬B]
max
¬¬A
¬A → ¬A ¬A
me[¬A, A, ♦B, ♦¬B]
=0
me[¬A, A, ¬A → ¬A, ♦B, ♦¬B]
me[¬A, ¬A, ♦B, ♦¬B]
min
♦B
♦¬B
me[¬A, B]
=1
me[¬A, ¬B]
=1
Struktur der rekursiven Aufrufe
f¨
ur merf¨
ullbar({♦A ∧ ♦¬A ∧ (A → A ∧ ¬A → ¬A ∧ ♦B ∧ ♦¬B)})
Wir schreiben abk¨
urzend me[X , Y , Z ] f¨
ur merf¨
ullbar({X , Y , Z }).
Rekursive Aufrufe f¨
ur Formeln vom Typ 1 sind nicht aufgef¨
uhrt.
me[♦A, ♦¬A, (A → A ∧ ¬A → ¬A ∧ ♦B ∧ ♦¬B)]
min
♦A
♦¬A
me[A, A → A, ¬A → ¬A, ♦B, ♦¬B]
.
..
=1
me[¬A, A → A, ¬A → ¬A, ♦B, ♦¬B]
max
¬A
A → A A
me[¬A, ¬A → ¬A, ♦B, ♦¬B]
..
.
=1
me[¬A, A, ¬A → ¬A, ♦B, ♦¬B]
Struktur der rekursiven Aufrufe
f¨
ur merf¨
ullbar({♦A ∧ ♦¬A ∧ (A → A ∧ ¬A → ¬A ∧ ♦B ∧ ♦¬B)})
Wir schreiben abk¨
urzend me[X , Y , Z ] f¨
ur merf¨
ullbar({X , Y , Z }).
Rekursive Aufrufe f¨
ur Formeln vom Typ 1 sind nicht aufgef¨
uhrt.
me[♦A, ♦¬A, (A → A ∧ ¬A → ¬A ∧ ♦B ∧ ♦¬B)]
min
♦A
♦¬A
me[A, A → A, ¬A → ¬A, ♦B, ♦¬B]
.
..
=1
me[¬A, A → A, ¬A → ¬A, ♦B, ♦¬B]
max
¬A
A → A A
me[¬A, ¬A → ¬A, ♦B, ♦¬B]
me[¬A, A, ¬A → ¬A, ♦B, ♦¬B]
..
max
.
¬¬A
¬A → ¬A ¬A
=1
me[¬A, A, A, ♦B, ♦¬B]
=0
me[¬A, A, ¬A, ♦B, ♦¬B]
Struktur der rekursiven Aufrufe
f¨
ur merf¨
ullbar({♦A ∧ ♦¬A ∧ (A → A ∧ ¬A → ¬A ∧ ♦B ∧ ♦¬B)})
Wir schreiben abk¨
urzend me[X , Y , Z ] f¨
ur merf¨
ullbar({X , Y , Z }).
Rekursive Aufrufe f¨
ur Formeln vom Typ 1 sind nicht aufgef¨
uhrt.
me[♦A, ♦¬A, (A → A ∧ ¬A → ¬A ∧ ♦B ∧ ♦¬B)]
min
♦A
♦¬A
me[A, A → A, ¬A → ¬A, ♦B, ♦¬B]
.
..
=1
me[¬A, A → A, ¬A → ¬A, ♦B, ♦¬B]
max
¬A
A → A A
me[¬A, ¬A → ¬A, ♦B, ♦¬B]
me[¬A, A, ¬A → ¬A, ♦B, ♦¬B]
..
max
.
¬¬A
¬A → ¬A ¬A
=1
me[¬A, A, A, ♦B, ♦¬B]
=0
me[¬A, A, ¬A, ♦B, ♦¬B]
min
♦B
♦¬B
me[A, ¬A, B]
=0
me[A, ¬A, B]
=0
(Grobe) Analyse
Es gilt: ϕ ist erf¨ullbar genau dann, wenn merf¨ullbar({ϕ}) = 1.
Bei Aufruf von merf¨ullbar({ϕ}) wird ein Baum durchsucht,
I
dessen Tiefe durch die Anzahl der Verkn¨upfungszeichen in ϕ
beschr¨ankt ist
I
bei dem der Ausgangsgrad jedes Knotens durch die Anzahl der
modalen Operatoren in ϕ beschr¨ankt ist
I
in dem jeder Knoten mit einer Formelmenge markiert ist, deren
Gr¨oße durch die Gr¨oße von ϕ beschr¨ankt ist.
Der Speicherverbrauch ist also O(|ϕ|2 ) f¨ur den Rekursionsstapel.
Satz 2.23
Das Erf¨ullbarkeitsproblem f¨ur modale Aussagenlogik ist in PSPACE.
Komplexit¨
at
Die Tabelle zeigt komplexit¨atstheoretische Vollst¨andigkeitsresultate.
Aussagenlogik
(AL)
Intuitionistische AL
Modale AL
Erf¨
ullbarkeit
G¨
ultigkeit
Formelauswertung
NP
coNP
NC1
[Cook 71]
[Cook 71]
[Buss 87]
NP
PSPACE
P
[Cook 71]
[Statman 79]
[MuWe 10]
PSPACE
PSPACE
P
[Ladner 77]
[Ladner 77]
[Folklore]
NP
NC1
P
PSPACE
coNP
polynomielle Zeit
parallel
superschnell
polynomieller Platz
deterministisch nicht-determ.
schnell
langsam
2.4.10
3 Temporale Aussagenlogik
3. Temporale Logik
Grundbegriffe linearer Zeitlogik LTL
B¨uchi-Automaten
Ein Algorithmus f¨ur das G¨ultigkeitsproblem f¨ur LTL
Formelauswertung von LTL-Formeln
Weitere temporale Logiken
3.0.1
Temporale Logik
Temporale Logik benutzt man z.B. zur Untersuchung von Prozessen,
die schrittweise ihren Zustand ver¨andern.
I jetzt, oder
Eine Aussage
kann z.B.
I irgendwann in der Zukunft, oder
I
solange, bis eine andere Aussage wahr ist,
wahr sein.
3.0.2
3.1 Grundbegriffe linearer Zeitlogik LTL
3. Temporale Logik
Grundbegriffe linearer Zeitlogik LTL
B¨uchi-Automaten
Ein Algorithmus f¨ur das G¨ultigkeitsproblem f¨ur LTL
Formelauswertung von LTL-Formeln
Weitere temporale Logiken
Literatur: Kreuzer, K¨
uhling: Logik f¨
ur Informatiker.
Eike Best: Modelchecking (Vorlesungsskript 2010, im Web).
3.1.3
Einfu
¨hrendes Beispiel
Modelliere: Prozesse d¨
urfen nicht gleichzeitig die selbe Ressource benutzen . . .
I
n – Ressource wird weder angefordert noch benutzt
I
a – Ressource wird angefordert (es wird auf Zugriff gewartet)
I
b – Ressource wird benutzt
s0
n1 n2
s1
Modell f¨
ur erlaubte Zustands¨
uberg¨ange:
a1 n2
n1 a2
s2
(bi . . . Prozess i benutzt die Ressource . . . )
(wir schreiben Atome hier mit kleinen Buchst.)
a1 a2
s4
b1 n2
s3
b1 a2 s6
n1 b2
s5
s7 a1 b2
Garantiert dieses Modell, dass
jeder Prozess die angeforderte Ressource auch irgendwann benutzen kann?
3.1.4
Temporale Operatoren
s0
n1 n2
s1
a1 n2
n 1 a2
s2
a1 a2
s4
b1 n2
s3
b1 a2 s6
n1 b2
s5
s 7 a1 b 2
Ein (unendlicher) Pfad π = s0 , s1 , s4 , . . . durch das Modell:
n1 n2
a1 n2
a1 a2
a1 b2
s0
s1
s4
...
a1 n2
b1 n2
b1 a2
n1 a2
n1 b2
...
Eigenschaften von Pfad π:
π
G . . . globally
p
n1 ∧ n2
“die Startwelt von π erf¨
ullt n1 ∧ n2 ”
3.1.5
Temporale Operatoren
s0
n1 n2
s1
a1 n2
n 1 a2
s2
a1 a2
s4
b1 n2
s3
b1 a2 s6
n1 b2
s5
s 7 a1 b 2
Ein (unendlicher) Pfad π = s0 , s1 , s4 , . . . durch das Modell:
n1 n2
a1 n2
a1 a2
a1 b2
s0
s1
s4
...
a1 n2
b1 n2
b1 a2
n1 a2
n1 b2
Eigenschaften von Pfad π:
π
p
F b2
“es gibt einen Suffix ρ von π = π 0 ρ mit ρ
G . . . globally, F . . . future
p
b2 ”
...
Temporale Operatoren
s0
n1 n2
s1
a1 n2
n 1 a2
s2
a1 a2
s4
b1 n2
s3
b1 a2 s6
n1 b2
s5
s 7 a1 b 2
Ein (unendlicher) Pfad π = s0 , s1 , s4 , . . . durch das Modell:
n1 n2
a1 n2
a1 a2
a1 b2
s0
s1
s4
...
a1 n2
b1 n2
b1 a2
n1 a2
n1 b2
...
Eigenschaften von Pfad π:
π
p
G ¬(b1 ∧ b2 )
G . . . globally, F . . . future
“f¨
ur alle Suffixe ρ von π gilt ρ
p
¬(b1 ∧ b2 )”
3.1.5
Temporale Operatoren
s0
n1 n2
s1
a1 n2
n 1 a2
s2
a1 a2
s4
b1 n2
s3
b1 a2 s6
n1 b2
s5
s 7 a1 b 2
Ein (unendlicher) Pfad π = s0 , s1 , s4 , . . . durch das Modell:
n1 n2
a1 n2
a1 a2
a1 b2
s0
s1
s4
...
a1 n2
b1 n2
b1 a2
n1 a2
n1 b2
...
Eigenschaften von Pfad π:
π
p
G . . . globally, F . . . future, X . . . next
G(a2 → F b2 )
3.1.5
Temporale Operatoren
s0
n1 n2
s1
a1 n2
n 1 a2
s2
a1 a2
s4
b1 n2
s3
b1 a2 s6
n1 b2
s5
s 7 a1 b 2
Ein (unendlicher) Pfad π = s0 , s1 , s4 , . . . durch das Modell:
n1 n2
a1 n2
a1 a2
a1 b2
s0
s1
s4
...
a1 n2
b1 n2
b1 a2
n1 a2
n1 b2
...
Eigenschaften von Pfad π:
π
p
X n2
“f¨
ur ρ mit π = s0 , ρ gilt ρ
G . . . globally, F . . . future, X . . . next
p
n2 ”
3.1.5
Temporale Operatoren
s0
n1 n2
s1
a1 n2
n 1 a2
s2
a1 a2
s4
b1 n2
s3
b1 a2 s6
n1 b2
s5
s 7 a1 b 2
Ein (unendlicher) Pfad π = s0 , s1 , s4 , . . . durch das Modell:
n1 n2
a1 n2
a1 a2
a1 b2
s0
s1
s4
...
a1 n2
b1 n2
b1 a2
n1 a2
n1 b2
...
Eigenschaften von Pfad π:
π
p
n1 ∧ X n2 ∧ X X a2
G . . . globally, F . . . future, X . . . next
π
p
n1 ∧ X(n2 ∧ X a2 )
3.1.5
Temporale Operatoren
s0
n1 n2
s1
a1 n2
n 1 a2
s2
a1 a2
s4
b1 n2
s3
b1 a2 s6
n1 b2
s5
s 7 a1 b 2
Ein (unendlicher) Pfad π = s0 , s1 , s4 , . . . durch das Modell:
n1 n2
a1 n2
a1 a2
a1 b2
s0
s1
s4
...
a1 n2
b1 n2
b1 a2
n1 a2
n1 b2
...
Eigenschaften von Pfad π:
π 6 p G((a1 ∧ ¬b2 ) → X b1 )
G . . . globally, F . . . future, X . . . next
3.1.5
Temporale Operatoren
s0
n1 n2
s1
a1 n2
n 1 a2
s2
a1 a2
s4
b1 n2
s3
b1 a2 s6
n1 b2
s5
s 7 a1 b 2
Ein (unendlicher) Pfad π = s0 , s1 , s4 , . . . durch das Modell:
n1 n2
a1 n2
a1 a2
a1 b2
s0
s1
s4
...
a1 n2
b1 n2
b1 a2
n1 a2
n1 b2
...
Eigenschaften von Pfad π:
π 6 p G((a1 ∧ ¬b2 ) → X b1 )
G . . . globally, F . . . future, X . . . next
π
p
¬ G((a1 ∧ ¬b2 ) → X b1 )
3.1.5
Temporale Operatoren
s0
n1 n2
s1
a1 n2
n 1 a2
s2
a1 a2
s4
b1 n2
s3
b1 a2 s6
n1 b2
s5
s 7 a1 b 2
Ein (unendlicher) Pfad π = s0 , s1 , s4 , . . . durch das Modell:
n1 n2
a1 n2
a1 a2
a1 b2
s0
s1
s4
...
a1 n2
b1 n2
b1 a2
n1 a2
n1 b2
...
Eigenschaften von Pfad π:
π
p
F ¬((a1 ∧ ¬b2 ) → X b1 )
G . . . globally, F . . . future, X . . . next
π
p
¬ G((a1 ∧ ¬b2 ) → X b1 )
3.1.5
Temporale Operatoren
s0
n1 n2
s1
a1 n2
n 1 a2
s2
a1 a2
s4
b1 n2
s3
b1 a2 s6
n1 b2
s5
s 7 a1 b 2
Ein (unendlicher) Pfad π = s0 , s1 , s4 , . . . durch das Modell:
n1 n2
a1 n2
a1 a2
a1 b2
s0
s1
s4
...
a1 n2
b1 n2
b1 a2
n1 a2
n1 b2
...
Eigenschaften von Pfad π:
π
p
F ¬((a1 ∧ ¬b2 ) → X b1 )
G . . . globally, F . . . future, X . . . next
π
p
F((a1 ∧ ¬b2 ) ∧ ¬ X b1 )
3.1.5
Temporale Operatoren
s0
n1 n2
s1
a1 n2
n 1 a2
s2
a1 a2
s4
b1 n2
s3
b1 a2 s6
n1 b2
s5
s 7 a1 b 2
Ein (unendlicher) Pfad π = s0 , s1 , s4 , . . . durch das Modell:
n1 n2
a1 n2
a1 a2
a1 b2
s0
s1
s4
...
a1 n2
b1 n2
b1 a2
n1 a2
n1 b2
...
Eigenschaften von Pfad π:
π
p
F((a1 ∧ ¬b2 ) ∧ X ¬b1 )
π
p
F((a1 ∧ ¬b2 ) ∧ ¬ X b1 )
G . . . globally, F . . . future, X . . . next , U . . . until
3.1.5
Temporale Operatoren
s0
n1 n2
s1
a1 n2
n 1 a2
s2
a1 a2
s4
b1 n2
s3
b1 a2 s6
n1 b2
s5
s 7 a1 b 2
Ein (unendlicher) Pfad π = s0 , s1 , s4 , . . . durch das Modell:
n1 n2
a1 n2
a1 a2
a1 b2
s0
s1
s4
...
a1 n2
b1 n2
b1 a2
n1 a2
n1 b2
...
Eigenschaften von Pfad π:
π
p
(a1 ∨ n2 ) U b1
“von s0 aus auf π gilt a1 ∨ n2 bis b1 erf¨
ullt ist”
G . . . globally, F . . . future, X . . . next , U . . . until
3.1.5
Syntax von LTL
LTL . . . linear-time temporal logic
Definition 3.1 (die Sprache: LTL-Formeln)
(Aussagenlogische) LTL-Formeln sind induktiv definiert wie folgt.
1. Die Konstante ⊥ und alle Atome Ai sind LTL-Formeln.
2. F¨ur alle LTL-Formeln α und β sind
α → β,
Xα
(next),
Fα
(future),
Gα
(globally),
αUβ
(until)
ebenfalls LTL-Formeln.
Wir benutzen Abk¨urzungen >, ¬α, α ∧ β, α ∨ β, α ↔ β wie u¨blich.
Semantik von LTL
Definition 3.2 ((Pfad-)Erf¨
ullungsrelation
p
f¨
ur LTL)
Sei π = π0 π1 π2 . . . eine unendliche Folge von Belegungen
πi ⊆ {A0 , A1 , . . .}, und π j = πj πj+1 . . . Suffix von π (f¨ur j ≥ 0). Die
Relation p zwischen Belegungsfolgen und LTL-Formeln ist wie folgt
definiert.
π6p ⊥
π
π
Ai gdw. Ai ∈ π0
α → β gdw. π 6 p α oder π
p
β
p
π
p
X α gdw. π 1
π
p
F α gdw. es gibt ein i ≥ 0 : π i
π
π
p
p
p
p
α
G α gdw. f¨ur alle i ≥ 0 : π
i
p
p
α
α
α U β gdw. es gibt ein i ≥ 0 : π i p β
und f¨ur alle j = 0, 1, . . . , i − 1 : π j
p
α
Definition 3.3 (¨
aquivalente LTL-Formeln)
LTL-Formeln α und β heißen ¨aquivalent (α ≡ β),
falls f¨ur jede Belegungsfolge π gilt: π p α genau dann, wenn π
p
β.
¨
Lemma 3.4 (wichtige Aquivalenzen
in LTL)
1. ¬ X α ≡ X ¬α
2. ¬ G α ≡ F ¬α
3.
Fα ≡ >Uα
4.
X α ≡ X(⊥ U α)
5.
F α ≡ α ∨ X(> U α)
6. α U β ≡ β ∨ (α ∧ X(α U β))
3.1.8
Lemma 3.5
F¨ur jede LTL-Formel α gibt es eine ¨aquivalente Formel α0 ,
die nur aus ⊥, Atomen, →, X und U besteht.
Wir benutzen >, ∧, ∨, ↔, F und G weiterhin als abk¨urzende
Schreibweisen.
Definition 3.6 (Erf¨
ullbarkeit, G¨
ultigkeit)
Sei ϕ eine LTL-Formel.
ϕ heißt erf¨ullbar (bezgl. p ),
falls es eine Belegungsfolge π mit π
p
ϕ gibt.
ϕ heißt g¨ultig (bezgl. p ),
falls π p ϕ f¨ur alle Belegungsfolgen π gilt.
Wir werden einen Algorithmus zum Test der G¨ultigkeit von
LTL-Formeln betrachten.
Der Algorithmus muss mit unendlichen Belegungsfolgen umgehen
k¨onnen.
Soetwas kennt man in der Theoretischen Informatik von
B¨uchi-Automaten.
Im n¨achsten Abschnitt werden sie vorgestellt.
3.1.10
Tableau- und Frege-Systeme fu
¨r LTL
Siehe z.B.
Orna Lichtenstein, Amir Pnueli:
Propositional temporal logics: decidability and completeness
Logic Journal of the IGPL 8(1), pp.55-85, 2000.
Mark Reynolds:
A traditional tree-style tableau for LTL
http://www.csse.uwa.edu.au/∼mark/research/Online/ltlsattabLONG.pdf, 2014
3.1.11
3.2 Bu
¨chi-Automaten
3. Temporale Logik
Grundbegriffe linearer Zeitlogik LTL
B¨uchi-Automaten
Ein Algorithmus f¨ur das G¨ultigkeitsproblem f¨ur LTL
Formelauswertung von LTL-Formeln
Weitere temporale Logiken
B¨uchi-Automaten sind endliche Automaten, die unendliche W¨orter
entscheiden.
Wir wiederholen zuerst kurz das Grundwissen u¨ber
endliche Automaten (f¨ur endliche W¨orter)
und lernen dann etwas u¨ber
endliche Automaten f¨ur unendliche W¨orter.
3.2.12
Endliche Automaten fu
orter
¨r endliche W¨
Ein endlicher Automat A = (Q, Σ, ∆, q0 , F ) besteht aus
I einer endlichen Menge Q
(Zust¨ande)
I einem endlichen Alphabet Σ
I einer Relation ∆ ⊆ Q × Σ × Q (Zustands¨
uberg¨ange)
I einem Startzustand q0 ∈ Q
I einer Menge von Endzust¨
anden F ⊆ Q
a
start
Q = {A, B, C , D}
A
a
b
B
a
b
D
b
Σ = {a, b}
∆ = {(A, a, B), (A, b, C ), . . .}
q0 = A
F = {A, D}
C
a
b
3.2.13
Von einem EA akzeptierte W¨
orter
Ein Wort w = a1 · · · an (ai ∈ Σ) wird vom endlichen Automaten A
akzeptiert,
wenn es eine Zustandsfolge ρ0 ρ1 ρ2 · · · ρn gibt (ρi ∈ Q), so dass
I ρ0 = q0 (die Folge beginnt mit dem Startzustand),
I (ρi−1 , ai , ρi ) ∈ ∆ f¨
ur 1 ≤ i ≤ n
(die Zustands¨uberg¨ange entsprechen dem Wort w ), und
I ρn ∈ F (die Folge endet in einem Endzustand).
a
a
start
A
B
D
b
b
a
b
C
b
a
3.2.14
Regul¨
are Sprache
Ein EA A = (Q, Σ, ∆, q0 , F ) akzeptiert die Sprache
L(A) = {w ∈ Σ∗ | A akzeptiert w } .
Eine Sprache heißt regul¨ar, wenn sie von einem EA akzeptiert wird.
Ein EA heißt deterministisch, wenn ∆ eine Funktion Q × Σ → Q ist.
Satz 3.7
Die Klasse der regul¨aren Sprachen ist abgeschlossen unter
Nichtdeterminismus, Komplement und Vereinigung.
3.2.15
Zwei ¨
aquivalente Entscheidungsprobleme
Definition 3.8 (Leerheitsproblem f¨
ur endliche Automaten)
Das Leerheitsproblem f¨ur endliche Automaten ist das folgende
Entscheidungsproblem.
gegeben:
gefragt:
ein endlicher Automat A
ist L(A) = ∅ ?
Definition 3.9 (Graph-Erreichbarkeitsproblem)
Das Erreichbarkeitsproblem f¨ur gerichtete Graphen ist das folgende
Entscheidungsproblem.
gegeben:
gefragt:
gerichteter Graph G , Knoten s und t
hat G einen Pfad von s nach t ?
3.2.16
Algorithmus fu
¨r das Nicht-Leerheitsproblem
f¨
ur endliche Automaten
Eingabe: endlicher Automat B = (Q, Σ, ∆, q0 , F )
w¨ahle nichtdeterministisch q ∈ F
s := q0
wiederhole |Q| − 1-mal {
(∗ finde einen Weg von q0 nach q ∗)
w¨ahle nichtdeterministisch v ∈ Q
falls (s, a, v ) ∈ ∆ f¨
ur ein a ∈ Σ
dann s := v
}
falls s = q
dann akzeptiere
sonst verwirf
Analyse des Algorithmus
1. Der Algorithmus h¨alt bei jeder Eingabe und ist korrekt.
2. Der Wert jeder Variable kann mit log |Q| Bit gespeichert werden.
3. Der Algorithmus ist nichtdeterministisch.
Das Nicht-Leerheitsproblem f¨
ur endliche Automaten
ist in NL (nondeterministic logspace).
Da NL Komplement-abgeschlossen ist,
ist auch das Leerheitsproblem f¨
ur endliche Automaten in NL.
NP
NC1
L
NL
P
PSPACE
coNP
polynomielle Zeit
logarithmischer Platz
polynomieller Platz
3.2.18
Unendliche W¨
orter
Sei Σ ein Alphabet (also eine endliche Menge und nicht leer).
Σ∗ ist die Menge aller endlichen W¨orter u¨ber Σ.
Σ∗ ist abz¨ahlbar unendlich.
Σω ist die Menge aller unendlichen W¨orter u¨ber Σ.
(“ω-W¨orter”)
Σω ist u¨berabz¨ahlbar unendlich.
Noch allgemeiner: sei S eine Menge.
S ∗ = {w1 w2 · · · wm | m ≥ 0 und wi ∈ S f¨ur alle i = 1, 2, . . . , m}
S ω = {w1 w2 · · · | wi ∈ S f¨ur alle i ≥ 1}
Bu
¨chi-Automaten
Endliche Automaten f¨
ur unendliche W¨
orter
Ein B¨uchi-Automat ist ein endlicher Automat A = (Q, Σ, ∆, q0 , F ).
Ein ω-Wort w = a1 a2 · · · (ai ∈ Σ) wird vom B¨uchi-Automaten A
akzeptiert,
wenn es eine unendliche Zustandsfolge ρ0 ρ1 ρ2 · · · gibt (ρi ∈ Q), so
dass
I
ρ0 = q0 (die Folge beginnt mit dem Startzustand),
I
(ρi−1 , ai , ρi ) ∈ ∆ f¨ur i ≥ 1
(die Zustands¨uberg¨ange entsprechen dem Wort w ), und
I
es gibt unendlich viele i mit ρi ∈ F
(die Folge durchl¨auft unendlich oft einen Endzustand).
Lω (A) = {w ∈ Σω | A akzeptiert w }
ist die vom B¨uchi-Automat A akzeptierte Sprache.
3.2.20
Beispiel 1
Σ = {a, b, c}
a, c
b, c
a
A1 :
start
A
B
b
Beispiel 1
Σ = {a, b, c}
a, c
b, c
a
A1 :
start
A
B
b
Lω (A1 ) = {w ∈ Σω | in w kommt nach jedem a irgendwann ein b}
3.2.21
Beispiel 2
Σ = {a, b, c}
b, c
a, b, c
A2 :
start
A
a
B
3.2.22
Beispiel 2
Σ = {a, b, c}
b, c
a, b, c
A2 :
start
A
a
Lω (A2 ) = {w ∈ Σω | in w gibt es ein letztes a}
B
Beispiel 3
Σ = {a, b, c}
b, c
c
a
A3 :
start
A
B
b
3.2.23
Beispiel 3
Σ = {a, b, c}
b, c
c
a
A3 :
start
A
B
b
Lω (A3 ) = {w ∈ Σω | zwischen zwei a in w kommt stets ein b vor}
3.2.23
Beispiele 4 und 5
Σ = {a, b}
a, b
A4 :
start
A
a
a
B
3.2.24
Beispiele 4 und 5
Σ = {a, b}
a, b
A4 :
start
A
a
a
B
Lω (A4 ) = {w ∈ Σω | in w gibt es nur endlich viele b}
3.2.24
Beispiele 4 und 5
Σ = {a, b}
a, b
A4 :
start
A
a
a
B
Lω (A4 ) = {w ∈ Σω | in w gibt es nur endlich viele b}
a
A5 :
start
b
b
A
B
a
3.2.24
Beispiele 4 und 5
Σ = {a, b}
a, b
A4 :
start
A
a
a
B
Lω (A4 ) = {w ∈ Σω | in w gibt es nur endlich viele b}
a
A5 :
start
b
b
A
B
a
Lω (A5 ) = {w ∈ Σω | in w kommen unendlich viele b vor}
Beispiele 4 und 5
Σ = {a, b}
a, b
A4 :
start
A
a
a
B
Lω (A4 ) = {w ∈ Σω | in w gibt es nur endlich viele b}
a
A5 :
start
b
b
A
B
a
Lω (A5 ) = {w ∈ Σω | in w kommen unendlich viele b vor} = Lω (A4 )
Determinismus vs. Nichtdeterminismus
Lemma 3.10
Es gibt keinen deterministischen B¨uchi-Automaten f¨ur
Lω (A4 ) = {w ∈ {a, b}ω | in w gibt es nur endlich viele b}.
Beweis: Sei B ein det. B¨
uchi-Automat mit z Zust¨anden und Lω (B) ⊇ Lω (A4 ).
Da baaa · · · ∈ Lω (A4 ), gibt es ein r1 ,
so dass B bei Eingabe bar1 in einem Endzustand ist.
Entsprechend gibt es ein Wort bar1 bar2 bar3 . . . barz+1 , so dass B bei Eingabe von
bar1 . . . bari in einem Endzustand ist (f¨
ur i = 1, 2, . . . , z + 1).
Da B nur z Zust¨ande hat, muss einer dieser Zust¨ande
bei Eingabe von bar1 . . . barx und auch bei Eingabe von bar1 . . . bary (x < y )
erreicht sein.
Dann ist bar1 . . . barx (barx+1 . . . bary )ω ein ω-Wort mit unendlich vielen b,
das von B akzeptiert wird.
Also gilt Lω (B) ) Lω (A4 ).
Folglich gibt es keinen deterministischen B¨
uchi-Automaten f¨
ur Lω (A4 ).
X
3.2.25
ω-regul¨
are Sprachen
Sei Σ ein Alphabet.
Eine Teilmenge A ⊆ Σω heißt ω-regul¨ar,
falls es einen B¨uchi-Automaten B mit A = Lω (B) gibt.
(Mit B¨
uchi-Automat ist ein nichtdeterministischer B¨
uchi-Automat gemeint.)
Lemma 3.11 (Abschlusseigenschaften ω-regul¨
arer Sprachen)
1. Wenn A regul¨ar ist, dann ist Aω ω-regul¨ar.
2. Wenn A regul¨ar und B ω-regul¨ar ist, dann ist A B ω-regul¨ar.
3. Die Klasse der ω-regul¨aren Sprachen ist abgeschlossen unter
Durchschnitt und Komplement.
3.2.26
Abschlusseig. ω-regul¨
arer Sprachen
Der Beweis der Komplementabgeschlossenheit der Klasse der ω-regul¨arer
Sprachen ist schwierig.
Wichtig ist, dass der Komplement-Automat exponentiell wachsen kann.
Zum Abschluss unter Durchschnitt:
Bezeichne w [i] den Pr¨afix der L¨ange i von w .
Das ω-Wort w wird von A und B akzeptiert genau dann, wenn es eine
unendliche Folge i1 < i2 < i3 < . . . von nat¨
urlichen Zahlen gibt, so dass
I f¨
ur jedes ungerade ` gilt: A erreicht mit w [i` ] einen Endzustand, und
I f¨
ur jedes gerade ` gilt: B erreicht mit w [i` ] einen Endzustand.
Aus A = (QA , Σ, ∆A , zA , FA ) und B = (QB , Σ, ∆B , zB , FB ) ergibt sich damit
C = (QA × QB × {1, 2}, Σ, ∆C , (zA , zB , 1), FA × QB × {1} ∪ QA × FB × {2})
mit ∆C = {((a, b, i), x, (a0 , b 0 , j)) | (a, x, a0 ) ∈ ∆A und (b, x, b 0 ) ∈ ∆B und
(1) i = 1 und a ∈ FA und j = 2, oder
(2) i = 2 und b ∈ FB und j = 1, oder (3) i = j }
Das Leerheitsproblem fu
¨r Bu
¨chi-Automaten
Definition 3.12 (Leerheitsproblem f¨
ur B¨
uchi-Automaten)
Das Leerheitsproblem f¨ur B¨uchi-Automaten ist folgendes
Entscheidungsproblem.
gegeben:
gefragt:
ein B¨uchi-Automat B
ist Lω (B) = ∅ ?
Idee zur L¨osung des Nicht-Leerheitsproblems:
wenn B ein Wort w akzeptiert,
dann gibt es einen Endzustand, der bei w unendlich oft durchlaufen wird.
Algorithmus dazu:
(1) rate einen Endzustand q, der vom Startzustand erreichbar ist
(2) falls q auf einem Kreis liegt,
dann ist Lω (B) nicht leer
Algorithmus fu
¨r das Nicht-Leerheitsproblem
f¨
ur B¨
uchi-Automaten
Eingabe B¨
uchi-Automat B = (Q, Σ, ∆, q0 , F )
w¨ahle nichtdeterministisch q ∈ F
s := q0
wiederhole |Q| − 1-mal {
(∗ finde einen Weg von q0 nach q ∗)
w¨ahle nichtdeterministisch v ∈ Q
falls (s, a, v ) ∈ ∆ f¨
ur ein a ∈ Σ, dann s := v
}
falls s 6= q dann verwirf (und halte)
w¨ahle nichtdeterministisch v ∈ Q
(∗ finde einen Weg von q nach q, ∗)
falls (s, a, v ) ∈ ∆ f¨
ur ein a ∈ Σ, dann s := v
(∗ der mindestens eine Kante enth¨
alt. ∗)
sonst verwirf (und halte)
wiederhole |Q| − 2-mal
w¨ahle nichtdeterministisch v ∈ Q
falls (s, a, v ) ∈ ∆ f¨
ur ein a ∈ Σ, dann s := v
}
falls s = q
dann akzeptiere
sonst verwirf
Analyse des Algorithmus
1. Der Algorithmus h¨alt bei jeder Eingabe und ist korrekt.
2. Der Wert jeder Variable kann mit log |Q| Bit gespeichert werden.
3. Der Algorithmus ist nichtdeterministisch.
Das Nicht-Leerheitsproblem f¨ur B¨uchi-Automaten
ist in NL (nondeterministic logspace).
Da NL Komplement-abgeschlossen ist,
ist auch das Leerheitsproblem f¨ur B¨uchi-Automaten in NL.
Die beiden Probleme sind auch NL-vollst¨andig.
Verallgemeinerte Bu
¨chi-Automaten
Ein verallgemeinerter B¨uchi-Automat B = (Q, Σ, ∆, q0 , F) besteht aus
I
einer endlichen Menge Q (Zust¨ande)
I
einem endlichen Alphabet Σ
I
einer Relation ∆ ⊆ Q × Σ × Q
I
einem Startzustand q0 ∈ Q
I
einer Menge F ⊆ P(Q) aus Teilmengen von Q
Ein ω-Wort w ∈ Σω wird von B akzeptiert,
falls es eine Zustandsfolge s0 , s1 , s2 , . . . gibt, die von B bei Eingabe w
durchlaufen wird,
in der f¨ur jedes F ∈ F unendlich viele i mit si ∈ F vorkommen.
Beispiele fu
¨r verallg. Bu
¨chi-Automaten
b
a
a
b
B1 :
start
A
b
b
B2 :
B
start
A
a
B
a
ω
Lω (B1 ) = {w ∈ {a, b} | in w kommen unendlich viele b vor}
Lω (B2 ) = {w ∈ {a, b}ω | in w kommen unendlich viele a vor}
b
a
b
B3 :
start
A
B
a
Lω (B3 ) = {w ∈ {a, b}ω | in w kommen unendl. viele a und unendl. viele b vor}
B3 ist ein verallgemeinerter B¨
uchi-Automat mit F = {A}, {B}}.
3.2.32
Lemma 3.13
Jede ω-Sprache, die von einem verallgemeinerten B¨uchi-Automaten
akzeptiert wird, wird auch von einem (normalen) B¨uchi-Automaten
akzeptiert.
Beweisidee:
Sei B = (Q, Σ, ∆, q0 , {F0 , F1 , . . . , F`−1 }) ein verallgemeinerter
B¨
uchi-Automat.
ˆ = (Q × {0, 1, . . . , ` − 1}, Σ, ∆0 , (q0 , 0), F ) mit
Definiere B
((b, k), x, (b 0 , k 0 )) ∈ ∆0 genau dann, wenn
¨
(b, x, b 0 ) ∈ ∆ (Ubergang
gem¨aß B) und
0
I wenn b ∈ Fk , dann k = (k + 1) mod `; sonst ist k = k 0 .
(Wenn ein Endzustand in Fk erreicht wurde,
dann wird auf einen Endzustand in Fk+1 gewartet.)
S
Schließlich ist F =
Fi × {i}.
I
i=0,1,...,`−1
ˆ
Es ist nicht zu schwer zu sehen, dass Lω (B) = Lω (B).
X
3.2.33
Definition 3.14 (G¨
ultigkeitsproblem f¨
ur LTL)
Das G¨
ultigkeitsproblem f¨
ur LTL ist folgendes Entscheidungsproblem.
gegeben:
gefragt:
LTL-Formel ϕ
gilt π ϕ f¨
ur jede Belegungsfolge π ?
1. Wir konstruieren einen B¨
uchi-Automat B¬ϕ aus der Formel ¬ϕ,
der alle Belegungsfolgen akzeptiert, die ¬ϕ erf¨
ullen.
2. Nun gilt: ϕ is g¨
ultig genau dann, wenn Lω (B¬ϕ ) = ∅.
Also kann man das G¨
ultigkeitsproblem f¨
ur LTL-Formeln mit dem
Leerheitsproblem f¨
ur B¨
uchi-Automaten l¨
osen.
Achtung: hier ist noch unklar,
wie groß B¬ϕ wird.
Diese Gr¨oße bestimmt den Aufwand des Algorithmus . . .
Der B¨uchi-Automat f¨ur die LTL-Formel
¬ F(A ∧ G(¬C → X ¬B))
[≡ G(A → F(¬C ∧ X B))]
I
soll z.B. folgende Belegungsfolgen akzeptieren:
{A, B, C }{A, B}{B, C }{A, B, C }{B}{B} · · ·
{A}( {B, C }{C }{A, B}{A, C } )ω
I
soll z.B. folgende Belegungsfolgen verwerfen:
{A, B}{B}{A}{A, B, C }{B}{B}∅ω · · ·
{A}{A}{A}{A}{A} · · ·
Da er mindestens eine Belegungsfolge akzeptiert,
ist F(A ∧ G(¬C → X ¬B)) keine g¨ultige Formel.
3.3.35
Hintikka-Mengen
Definition 3.15 (Hintikka-Mengen)
Eine Menge Z ⊆ Tf(ϕ) heißt Hintikka-Menge f¨ur die LTL-Formel ϕ,
falls gilt:
1. ⊥ 6∈ Z und
2. f¨ur alle α → β ∈ Tf(ϕ):
α → β ∈ Z gdw. α 6∈ Z oder β ∈ Z .
Beispiel: f¨
ur ϕ = A → ¬ X(¬B U A) mit
Tf(ϕ) = {A → ¬ X(¬B U A), A, ¬ X(¬B U A), X(¬B U A), ⊥, ¬B U A, ¬B, B}
sind die folgenden Mengen Hintikka-Mengen.
I
C1 = {A → ¬ X(¬B U A), X(¬B U A), ¬B}
I
C2 = {A → ¬ X(¬B U A), A, ¬ X(¬B U A), ¬B}
I
C3 = {A → ¬ X(¬B U A), A, X(¬B U A), ¬B U A, ¬B}
C4 = {A, X(¬B U A), B}
I
Hintikka-Mengen Z f¨ur ϕ sind wie ϕ-maximal-konsistente Mengen.
Es gilt f¨ur ¬α ∈ Tf(ϕ): ¬α ∈ Z gdw. α 6∈ Z !
Beobachtung
Sei ρ eine Belegungsfolge mit ρ
Dann ist {α | α ∈ Tf (ϕ) und ρ
p
p
ϕ.
α} eine Hintikka-Menge f¨ur ϕ.
Belegungsfolgen lassen sich entsprechend zu Folgen von
Hintikka-Mengen erweitern.
Definition 3.16 (durch ρ bestimmte Hintikka-Folge f¨
ur ϕ)
Sei ρ = ρ0 ρ1 . . . eine Belegungsfolge und ϕ eine LTL-Formel.
Die Folge von Hintikka-Mengen Z ρ,ϕ = Z0ρ,ϕ , Z1ρ,ϕ , . . . f¨ur ϕ mit
Ziρ,ϕ = {α ∈ Tf(ϕ) | ρi p α} heißt durch ρ bestimmte Hintikka-Folge
f¨ur ϕ.
3.3.37
Beispiel:
Sei ϕ = A → X(¬A U ¬B) und ρ = {A, B} {B} {B} {A} ({A, B})ω .
| {z } |{z} |{z} |{z} | {z }
ρ0
ρ1
ρ2
ρ3
ρ4+n
Dann ist
I
Z0ρ,ϕ = {A, B, X(¬A U ¬B), A → X(¬A U ¬B)}}
I
Z1ρ,ϕ = {¬A, B, ¬A U ¬B, X(¬A U ¬B), A → X(¬A U ¬B)}
I
Z2ρ,ϕ = Z1ρ,ϕ
I
Z3ρ,ϕ = {A, ¬B, ¬A U ¬B, ¬ X(¬A U ¬B)}
I
Z4ρ,ϕ = {A, B}
Welche Eigenschaften hat die Folge Z0 , Z1 , Z2 , . . . ?
I
ρ,ϕ
X α ∈ Ziρ,ϕ gdw. α ∈ Zi+1
I
ρ,ϕ
α U β ∈ Ziρ,ϕ gdw. β ∈ Ziρ,ϕ oder pα ∈ Ziρ,ϕ und α U β ∈ Zi+1
q
I
wenn α U β ∈ Ziρ,ϕ , dann gibt es ein j ≥ i mit β ∈ Zjρ,ϕ
Von Belegungsfolgen zu Hintikka-Folgen
Lemma 3.17
Sei ρ eine Belegungsfolge, ϕ eine LTL-Formel und Z ρ,ϕ die durch ρ
bestimmte Hintikka-Folge f¨ur ϕ. Dann gilt f¨ur alle i ≥ 0 und f¨ur alle
X α, α U β ∈ Tf (ϕ):
(L1) X α ∈ Zi gdw. α ∈ Zi+1 ,
(L2) α U β ∈ Zi gdw. β ∈ Zi oder pα ∈ Zi und α U β ∈ Zi+1 q,
und
(L3) wenn α U β ∈ Zi , dann gibt es ein j ≥ i mit β ∈ Zj .
Beweis ist ziemlich offensichtlich.
3.3.39
Von Hintikka-Folgen zu Belegungsfolgen
Lemma 3.18
Sei Z0 , Z1 , Z2 , . . . eine unendliche Folge von Hintikka-Mengen f¨ur ϕ mit
folgenden Eigenschaften f¨ur alle i ≥ 0.
(L1) X α ∈ Zi gdw. α ∈ Zi+1 ,
(L2) α U β ∈ Zi gdw. β ∈ Zi oder pα ∈ Zi und α U β ∈ Zi+1 q,
und
(L3) wenn α U β ∈ Zi , dann gibt es ein j ≥ i mit β ∈ Zj .
Dann gilt f¨ur die Belegungsfolge ρ = ρ0 ρ1 ρ2 · · · mit ρi = Zi ∩ At(ϕ),
alle α ∈ Tf (ϕ) und alle i ≥ 0:
ρi p α gdw. α ∈ Zi .
Beweis:
IA: f¨ur ⊥ und Atome gilt die Behauptung offensichtlich.
IS:
α = β → γ: folgt direkt aus der Semantik von →, der IV und der
Hintikka-Eigenschaft von Zi .
α = X β: folgt direkt aus der Semantik von →, der IV und Eigenschaft
(L1) von Zi und Zi+1 .
α = β U γ:
ρi
p
β U γ ⇔ ∃k ≥ i : ρk p γ & ∀j = 0, 1, . . . , k − 1 : ρj p β
⇔ ∃k ≥ i : γ ∈ Zk & ∀j = 0, 1, . . . , k − 1 : β ∈ Zj
⇔ ∃k ≥ i : γ ∈ Zk & β U γ ∈ Zk &
∀j = 0, 1, . . . , k − 1 : β ∈ Zj & β U γ ∈ Zj
⇔ β U γ ∈ Zi
X
3.3.41
Ein verallgemeinerter B¨uchi-Automat
I
die Hintikka-Mengen f¨ur ϕ als Zust¨ande hat,
I
vom Startzustand in alle Zust¨ande mit ϕ geht,
I
die Menge aller Belegungen f¨ur At(ϕ) als Alphabet benutzt,
I
die Zustands¨uberg¨ange gem¨aß (3.16), (L1) und (L2) macht und
I
die Endzust¨ande gem¨aß (L3),
(plus Extra-Startzustand)
akzeptiert alle ϕ erf¨ullenden Belegungsfolgen ρ
auf Pfaden, die durch ρ bestimmten Hintikka-Folgen mit (L1)–(L3)
entsprechen.
Beispiel 1: BAi
ϕ = Ai
∅
{Ai }
{Ai }
q0
start
{Ai }
{Ai }
{ }
∅
I
I
I
I
I
I
Zust¨ande {q0 } ∪ {Z | Z ⊆ Tf(Ai ) ist Hintikka-Menge}
Alphabet P(At(Ai )) = P({Ai })
der Startzustand hat alle Zust¨ande q mit ϕ ∈ q als Nachfolger
alle Zustands¨uberg¨ange benutzen die Belegung des Zielzustandes
Endzust¨ande (?)
Lω (BAi ) = {ρ ∈ (P(At(Ai )))ω | ρ p Ai }
3.3.43
Beispiel 2: B¬(> U ¬(> U A))
ϕ = ¬(> U ¬(> U A)) ≡ G F A
Jeder Zustand Z ⊆ Tf(ϕ) muss folgende Eigenschaften erf¨
ullen.
1. > ∈ Z , da ⊥ 6∈ Z und > ∈ Tf(¬(> U ¬(> U A)))
2. entweder > U A ∈ Z oder ¬(> U A) ∈ Z
3. entweder > U ¬(> U A) ∈ Z oder ¬(> U ¬(> U A)) ∈ Z
4. wenn A ∈ Z , dann > U A ∈ Z und damit ¬(> U A) 6∈ Z
5. wenn ¬(> U A) ∈ Z , dann > U ¬(> U A) ∈ Z und ¬(> U ¬(> U A)) 6∈ Z
Damit ergeben sich folgende 5 Hintikka-Mengen:
>
>
>
>
>
>
>
>
>
A
A
A
A
A
[¬](> U A)
>UA
>UA
¬(> U A)
¬(> U A)
>UA
>UA
¬(> U A)
¬(> U A)
[¬](> U ¬(> U A))
> U ¬(> U A)
¬(> U ¬(> U A))
¬(> U ¬(> U A))
> U ¬(> U A)
> U ¬(> U A)
¬(> U ¬(> U A))
¬(> U ¬(> U A))
> U ¬(> U A)
X
X
geht nicht
X
X
X
geht nicht
geht nicht
3.3.44
Beispiel 2: B¬(> U ¬(> U A))
ϕ = ¬(> U ¬(> U A)) ≡ G F A
Die Zust¨ande von Bϕ sind die 5 Hintikka-Mengen und der Startzustand q0 .
Das Alphabet {∅, {A}} ist die Menge aller Belegungen f¨
ur das Atom A.
Die Zustands¨
uberg¨ange m¨
ussen folgende Bedingungen erf¨
ullen.
1. wenn (q0 , B, Z 0 ) ∈ ∆, dann ¬(> U ¬(> U A)) ∈ Z 0
2. wenn (Z , {A}, Z 0 ) ∈ ∆, dann A ∈ Z 0
3. wenn (Z , ∅, Z 0 ) ∈ ∆, dann A 6∈ Z 0
4. wenn (Z , B, Z 0 ) ∈ ∆ und > U A ∈ Z und A 6∈ Z , dann > U A ∈ Z 0
5. wenn (Z , B, Z 0 ) ∈ ∆ und > U ¬(T U A) ∈ Z und ¬(> U A) 6∈ Z , dann
> U ¬(> U A) ∈ Z 0
F¨
ur jede Teilformel α U β von ϕ gibt es eine Menge von Endzust¨anden.
1. F> U A = {Z | wenn > U A ∈ Z , dann A ∈ Z }
2. F> U ¬(> U A) = {Z | wenn > U ¬(> U A) ∈ Z , dann ¬(> U A) ∈ Z }
B¬(> U ¬(> U A))
>
> U ¬(> U A)
>UA
ϕ = ¬(> U ¬(> U A)) ≡ G F A
A >
¬(>U¬(>UA))
>UA
{A}
start
A
> U ¬(> U A)
>UA
>
>UA
¬(>U¬(>UA))
>
∅
q0
¬(> U A)
> U ¬(> U A)
>
3.3.46
Definition 3.19 (durch ϕ bestimmter B¨
uchi-Automat Bϕ )
Sei ϕ eine LTL-Formel.
Dann ist Bϕ = (Q, Σ, ∆, q0 , F) der verallgemeinerte B¨
uchi-Automat mit
Q = q0 ∪ Z ⊆ Tf(ϕ) | Z ist eine Hintikka-Menge f¨
ur ϕ ,
= P(At(ϕ)),
F = Fα U β | α U β ∈ Tf(ϕ) ∪ Q mit
Fα U β = q ∈ Q − {q0 } | wenn α U β 6∈ q, dann β ∈ q und
∆ = (q0 , B, R) | ϕ ∈ R und B = R ∩ At(ϕ)
∪ (L, B, R) | L 6= q0 und R 6= q0 und B = R ∩ At(ϕ) und
f¨
ur alle X α ∈ Tf(ϕ) : X α ∈ L gdw. α ∈ R, und
f¨
ur alle α U β ∈ Tf(ϕ) : α U β ∈ L gdw.
(1) β ∈ L oder (2) α ∈ L und α U β ∈ R
.
Σ
Lemma 3.20
Bϕ akzeptiert genau die Belegungsfolgen ρ ∈ (P(At(ϕ)))ω mit ρ
p
ϕ.
Beweis:
“⇒”: Die Belegungsfolge ρ = ρ0 ρ1 . . . werde von Bϕ mit dem
Berechnungspfad q0 , Z0 , Z1 , . . . akzeptiert.
Behauptung 2
F¨
ur alle α ∈ Tf (ϕ) und alle i ≥ 0 gilt: ρi
Da ϕ ∈ Z0 , folgt ρ
p
p
α gdw. α ∈ Zi .
ϕ.
“⇐”: Wenn ρ p ϕ, dann kann Bϕ bei Eingabe ρ den Berechnungspfad
q0 , Z0ρ,ϕ , Z1ρ,ϕ , . . . entsprechend der durch ρ bestimmten Hintikka-Folge f¨
ur ϕ
durchlaufen.
Behauptung 3
q0 , Z0ρ,ϕ , Z1ρ,ϕ , . . . ist ein akzeptierender Berechnungspfad von Bϕ bei
Eingabe ρ.
Folglich wird ρ von Bϕ akzeptiert.
X
Beweis der Behauptung 3
Behauptung 3, formaler
ρ,ϕ
(1) (q0 , ρ0 , Z0ρ,ϕ ) ∈ ∆ und (Ziρ,ϕ , ρi+1 , Zi+1
) ∈ ∆ f¨ur alle i ≥ 0.
(2) Sei F = {F1 , . . . , Fk } die Menge der Endzustandsmengen von Bϕ .
F¨ur jedes j = 1, 2, . . . , k und jedes i ≥ 0 gilt: es gibt ein p ≥ i mit
Zpρ,ϕ ∈ Fj .
Alle Ziρ,ϕ sind Hintikka-Mengen.
Außerdem erf¨ullen sie “β ∈ Ziρ,ϕ ⇒ α U β ∈ Ziρ,ϕ ” f¨ur alle
α U β ∈ Tf(ϕ). da β ∈ Ziρ,ϕ ⇒ ρi p β ⇒ ρi p α U β ⇒ α U β ∈ Ziρ,ϕ .
zu (1): (q0 , ρ0 , Z0ρ,ϕ ) ∈ ∆, da Z0ρ,ϕ eine Hintikka-Menge ist und
ρ0 = Z0ρ,ϕ ∩ At(ϕ) ist.
ρ,ϕ
ρ,ϕ
(Ziρ,ϕ , ρi+1 , Zi+1
) ∈ ∆, da Ziρ,ϕ und Zi+1
Hintikka-Mengen sind und
nach Lemma 3.17 die Eigenschaften (L1) und (L2) erf¨ullen.
3.3.49
zu (2): Sei Fj die Endzustandsmenge f¨ur α U β ∈ Tf(ϕ).
Wenn α U β 6∈ Ziρ,ϕ , dann ist Ziρ,ϕ ∈ Fj .
Sei α U β ∈ Ziρ,ϕ .
Dann folgt ρi p α U β (da Z ρ,ϕ durch ρ bestimmt wird)
und folglich gibt es ein p ≥ i mit ρp p β (Semantik von U).
Dann ist β ∈ Zpρ,ϕ und damit ist Zpρ,ϕ ∈ Fj .
X
3.3.50
Beweis der Behauptung 2
Behauptung 2
F¨ur alle α ∈ Tf(ϕ) und alle i ≥ 0 gilt: ρi
p
α gdw. α ∈ Zi .
Wir beweisen die Behauptung induktiv u¨ber den Formelaufbau.
IA: F¨
ur α = ⊥ gilt ρi 6 p ⊥ und ⊥ 6∈ Zi , da Zi Hintikka-Menge ist.
F¨
ur α = A gilt
ρi p A gdw. A ∈ ρi (Semantik der Erf¨ullung von Atomen)
gdw. A ∈ Zi (wenn (L, ρi , R) ∈ ∆, dann ρi = R ∩ At(ϕ))
IV: die Behauptung gilt f¨
ur Formeln β und γ in Tf(ϕ).
IS: zu zeigen: die Behauptung gilt auch f¨
ur β → γ, X β und β U γ.
(1) ρi
p
β→γ
gdw.
gdw.
gdw.
ρi 6 p β oder ρi p γ
β 6∈ Zi oder γ ∈ Zi
β → γ ∈ Zi
(Semantik von →)
(IV)
(Zi ist Hintikka-Menge)
3.3.51
(2) ρi
p
Xβ
gdw.
gdw.
gdw.
ρi+1 p β
β ∈ Zi+1
X β ∈ Zi
(Semantik von X)
(IV)
(f¨
ur alle (L, ρi , R) ∈ ∆ gilt
(3) ρi p β U γ
gdw. ∃j ≥ i : ρj p γ
und f¨
ur l = i, i + 1, . . . , j − 1: ρl
X β ∈ L gdw. β ∈ R)
(Semantik von U)
p
β
gdw.
∃j ≥ i : γ ∈ Zj
und f¨
ur l = i, i + 1, . . . , j − 1: β ∈ Zl
(IV)
gdw.
∃j ≥ i : γ ∈ Zj und β U γ ∈ Zj
und f¨
ur l = i, i + 1, . . . , j − 1: β ∈ Zl
(γ ∈ Zj ⇒ β U γ ∈ Zj )
gdw.
(∗) ∃j ≥ i : γ ∈ Zj und β U γ ∈ Zj
(γ ∈ Zj ⇒ β U γ ∈ Zj )
und f¨
ur l = i, i + 1, . . . , j − 1: β ∈ Zl und β U γ ∈ Zl
(β ∈ Zl & β U γ ∈ Zl+1 ⇒ β U γ ∈ Zl )
Offensichtlich folgt β U γ ∈ Zi aus (∗).
Damit ist ρi p β U γ ⇒ β U γ ∈ Zi gezeigt.
3.3.52
Es bleibt noch zu zeigen: β U γ ∈ Zi ⇒ (∗).
Sei β U γ ∈ Zi .
Da ρ von Bϕ akzeptiert wird,
gibt es unendlich viele r mit Zr ∈ Fβ U γ .
Sei j das kleinste solche r mit r ≥ i.
Da f¨
ur (L, B, R) ∈ ∆ gilt,
dass “β U γ ∈ L ⇔ γ ∈ L oder pβ ∈ L und β U γ ∈ R q”,
sind β und β U γ in Zi , . . . , Zq−1
und β U γ, γ ∈ Zj .
Also folgt (∗) aus β U γ ∈ Zi .
Insgesamt ist damit β U γ ∈ Zi ⇒ ρi
p
α gezeigt.
X
3.3.53
LTL-Gu
¨ltigkeit und das Leerheitsproblem
fu
¨r Bu
¨chi-Automaten
Aus Lemma 3.20 folgt direkt
Satz 3.21
Sei ϕ eine LTL-Formel.
Dann ist ϕ g¨ultig genau dann, wenn Lω (B¬ϕ ) = ∅.
Damit ergibt sich der folgende Algorithmus f¨ur das G¨ultigkeitsproblem
f¨ur LTL.
3.3.54
Algorithmus f¨
ur das G¨
ultigkeitsproblem f¨
ur LTL
Eingabe: LTL-Formel ϕ
ˆ ¬ϕ = (Q, Σ, ∆, q0 , F ) gem¨aß Lemmas 3.20 und 3.13
sei B
w¨ahle nichtdeterministisch q ∈ F
x := q0
wiederhole |Q| − 1-mal
(∗ finde einen Weg von q0 nach q ∗)
w¨ahle nichtdeterministisch v ∈ Q
falls (x, a, v ) ∈ ∆ f¨
ur ein a ∈ Σ, dann x := v
falls x 6= q dann verwirf (und halte)
w¨ahle nichtdeterministisch v ∈ Q
(∗ finde einen Weg von q nach q, ∗)
falls (x, a, v ) ∈ ∆ f¨
ur ein a ∈ Σ, dann x := v (∗ der mindestens eine Kante enth¨alt. ∗)
sonst verwirf (und halte)
wiederhole |Q| − 2-mal
w¨ahle nichtdeterministisch v ∈ Q
falls (x, a, v ) ∈ ∆ f¨
ur ein a ∈ Σ, dann x := v
falls x = q
dann akzeptiere
sonst verwirf
Analyse des Algorithmus
Der Algorithmus ist fast genauso wie f¨
ur das Leerheitsproblem f¨
ur
B¨
uchi-Automaten und entscheidet deshalb das Komplement des
G¨
ultigkeitsproblems f¨
ur LTL.
ABER:
I Die Menge Q hat Gr¨
oße |Q| ∈ O(|W | · 2|ϕ| ),
deshalb ben¨
otigt die Variable x Speicherplatz O(log |W | + |ϕ|).
I Der Algorithmus ist also ein nichtdeterministischer Algorithmus,
der polynomiellen Speicherplatz ben¨
otigt.
I
Damit haben wir:
das Komplement des G¨
ultigkeitsproblems f¨
ur LTL ist in NPSPACE.
PSPACE = NPSPACE (nichtdet. Algorithmen kann man in det. Algorithmen umformen,
wobei sich der Speicherverbrauch quadriert (Satz von Savitch))
und PSPACE ist unter Komplement abgeschlossen.
Damit ergibt sich schließlich
Satz 3.22
Das G¨
ultigkeitsproblem f¨
ur LTL ist in PSPACE.
3.4 Das Formelauswertungsproblem von
LTL
3. Temporale Logik
Grundbegriffe linearer Zeitlogik LTL
B¨uchi-Automaten
Ein Algorithmus f¨ur das G¨ultigkeitsproblem f¨ur LTL
Formelauswertung von LTL-Formeln
Weitere temporale Logiken
Um Formeln f¨ur einen Belegungspfad auswerten zu k¨onnen, muss man
sich auf eine Darstellung von Pfadeb festlegen.
Dazu geht man von Pfaden zu Graphen und definiert eine Semantik f¨ur
LTL auf Kripke-Modellen.
Kripke-Semantik fu
¨r LTL-Formeln
Definition 3.23 (Erf¨
ullungsrelation
K
f¨
ur LTL-Formeln)
Sei M = (W , R, ξ) ein Kripke-Modell, w ∈ W und ϕ eine LTL-Formel.
M, w K ϕ, falls f¨
ur jeden unendlichen Pfad P = w , w1 , w2 , . . . durch
(W , R), der in w beginnt, gilt, dass ξ(w )ξ(w1 )ξ(w2 ) . . . p ϕ.
Definition 3.24 (Erf¨
ullbarkeit, G¨
ultigkeit)
Sei ϕ eine LTL-Formel.
ϕ heißt erf¨
ullbar, falls es ein Kripke-Modell M mit Welt w gibt, so dass
M, w K ϕ.
ϕ heißt g¨
ultig ( K ϕ), falls M, w
Welt w in M gilt.
K
ϕ f¨
ur jedes Kripke-Modell M und jede
Die unter Pfad-Semantik g¨
ultigen LTL-Formeln sind genau die unter
Kripke-Semantik g¨
ultigen LTL-Formeln.
Beispiel
s0
n1 n2
s1
M, s0 K ¬(b1 ∧ b2 )
(Sicherheit)
M, s0 6 K a1 → F b1
a1 n2
n 1 a2
a1 a2
s4
b1 n2
s3
b1 a2 s6
s2
n1 b2
s5
s 7 a1 b 2
3.4.59
Beispiel
s0
n1 n2
M, s0 K a1 → F b1
(Lebendigkeit)
M, s0
K
M, s0
K
a1 n 2
a1 → (a1 U b1 )
(a1 ∧ b2 )
→ X(¬b2 U b1 )
n1 a2
a1 a2
b1 n2
b 1 a2
a1 a2
n1 b2
a1 b2
3.4.60
Das Formelauswertungsproblem fu
¨r LTL
Definition 3.25 (Formelauswertungsproblem f¨
ur LTL)
gegeben: Kripke-Modell M = (W , R, ξ), Welt s ∈ W , LTL-Formel ϕ
gefragt:
gilt M, s K ϕ
Das Problem l¨asst sich mit einer Erweiterung unserer L¨osung f¨
ur das
G¨
ultigkeitsproblem l¨osen.
1. Wir konstruieren einen B¨
uchi-Automat BM,s aus dem Kripke-Modell M,
ξ
der alle ω-Belegungen π akzeptiert, die Pfaden π aus s entsprechen.
2. Wir konstruieren einen B¨
uchi-Automat B¬ϕ aus der Formel ¬ϕ,
der alle ω-Belegungen akzeptiert, die ¬ϕ erf¨
ullen (wie gehabt).
3. Nun gilt M, s K ϕ genau dann, wenn Lω (BM,s ) ∩ Lω (B¬ϕ ) = ∅.
Also kann man das Formelauswertungsproblem f¨
ur LTL-Formeln mit
dem Leerheitsproblem f¨
ur B¨
uchi-Automaten l¨
osen.
Hier ist noch unklar, wie groß BM,s , B¬ϕ und der Durchschnittsaut. werden.
Diese Gr¨oßen bestimmen den Aufwand des Algorithmus . . .
Belegungsfolgen aus Kripke-Modellen
Beispiel
Der B¨uchi-Automat f¨ur das Kripke-Modell M mit Welt s
s
A
soll folgende Belegungsfolgen
A
A, B
I
akzeptieren:
{A}{C }{A}{A, C }{B, C }{A} · · ·
{A}( {B, C }{C }{A, B}{A, C } )ω
I
verwerfen:
{A}{C }{B}{A, C }{B, C } · · ·
B, C
C
A, C
3.4.62
Belegungsfolgen aus LTL-Formeln
Beispiel
Der B¨uchi-Automat f¨ur die LTL-Formel
¬ F(A ∧ G(¬C → X ¬B))
[≡ G(A → F(¬C ∧ X B))]
I
soll folgende Belegungsfolgen akzeptieren:
{A, B, C }{A, B}{B, C }{A, B, C }{B}{B} · · ·
{A}( {B, C }{C }{A, B}{A, C } )ω
I
soll folgende Belegungsfolgen verwerfen:
{A, B}{B}{A}{A, B, C }{B}{B}∅ω · · ·
{A}{A}{A}{A}{A} · · ·
3.4.63
Formelauswert. mit den beiden Automaten
Beispiel
Der B¨uchi-Automat f¨ur
s
A
B, C
C
und der B¨uchi-Automat f¨ur
¬ F(A ∧ G(¬C → X ¬B)) akzeptiert
{A}( {B, C }{C }{A, B}{A, C } )ω .
A
A, B
akzeptiert also
{A}( {B, C }{C }{A, B}{A, C } )ω
A, C
Also gilt M, s 6 K F(A ∧ G(¬C → X ¬B)),
weil {A}( {B, C }{C }{A, B}{A, C } )ω 6 p F(A ∧ G(¬C → X ¬B)).
Bu
¨chi-Automaten aus Kripke-Modellen
Beispiel f¨
ur M, s und BM,s
s
s
start
A
{A}
B, C
C
{C }
{A, C }
{A}
A, C
Kripke-Modell M mit Welt
s
{A}
{B, C }
{C }
A
A, B
{B, C }
{A}
{A, B}
B¨uchi-Automat BM,s
mit Lω (BM,s ) =
ξ
{π | π ist Pfad durch M aus s}
3.4.65
Bu
¨chi-Automaten aus Kripke-Modellen
formal
Sei ϕ eine LTL-Formel.
Sei M = (W , R, ξ) eine Kripke-Modell mit Welt s ∈ W ,
und ξ : W → P(At(ϕ)).
(ξ(w ) ist eine Belegung.)
Definiere BM,s = (Q, Σ, ∆, s0 , F ) ein B¨
uchi-Automat mit
Q
Σ
∆
s0
F
=
=
=
=
=
W
P(At(ϕ))
{(w , ξ(w ), w 0 ) | (w , w 0 ) ∈ R}
s
Q
Lemma 3.26
Lω (BM,s ) = {π ξ | π ist unendlicher Pfad durch M mit Startpunkt s}.
Der Algorithmus
Satz 3.27
Sei M = (W , R, ξ) ein Kripke-Modell, s ∈ W , und ϕ eine LTL-Formel.
Dann gilt M, s K ϕ genau dann, wenn Lω (BM,s ) ∩ Lω (B¬ϕ ) = ∅.
Um Lω (BM,s ) ∩ Lω (B¬ϕ ) = ∅ zu entscheiden,
baut man sich einen B¨
uchi-Automaten BM,s,ϕ mit
Lω (BM,s,ϕ ) = Lω (BM,s ) ∩ Lω (B¬ϕ ) und entscheidet daf¨
ur das Leerheitsproblem.
Sei B¬ϕ = (Q, Σ, ∆, q0 , {F0 , . . . , F`−1 }).
Dann ist BM,s,ϕ = (W × Q × {1, 2, . . . , k}, Σ, ∆0 , (s, q0 , 1), F ) mit
((a, b, k), x, (a0 , b 0 , k 0 )) ∈ ∆0 genau dann, wenn
¨
I (a, a0 ) ∈ R und x = ξ(a) (Ubergang
gem¨aß BM,s )
0
¨
I (b, x, b ) ∈ ∆ (Ubergang gem¨
aß B¬ϕ )
I wenn b ∈ Fk , dann k 0 = (k + 1) mod `; sonst ist k = k 0
(Wenn ein Endzustand in Fk erreicht wurde,
dann wird auf einen Endzustand in Fk+1 gewartet.
Da alle Zust¨ande in BM,s Endzust¨ande sind,
braucht man sie nicht weiter zu ber¨
ucksichtigen.)
S
Schließlich ist F =
W × Fi × {i}.
i=0,1,...,`−1
Algorithmus fu
¨r das
Formelauswertungsproblem fu
¨r LTL
Eingabe Kripke-Modell M = (W , R, ξ), Welt s ∈ W , LTL-Formel ϕ
sei BM,s,ϕ = (Q, Σ, ∆, q0 , F ) wie oben beschrieben
w¨ahle nichtdeterministisch q ∈ F
x := q0
wiederhole |Q| − 1-mal
(∗ finde einen Weg von q0 nach q ∗)
w¨ahle nichtdeterministisch v ∈ Q
falls (x, a, v ) ∈ ∆ f¨
ur ein a ∈ Σ, dann x := v
falls x 6= q dann verwirf (und halte)
w¨ahle nichtdeterministisch v ∈ Q
(∗ finde einen Weg von q nach q, ∗)
falls (x, a, v ) ∈ ∆ f¨
ur ein a ∈ Σ, dann x := v (∗ der mindestens eine Kante enth¨alt. ∗)
sonst verwirf (und halte)
wiederhole |Q| − 2-mal
w¨ahle nichtdeterministisch v ∈ Q
falls (x, a, v ) ∈ ∆ f¨
ur ein a ∈ Σ, dann x := v
falls x = q
dann akzeptiere
sonst verwirf
Analyse des Algorithmus
Der Algorithmus ist fast genauso wie f¨
ur das Leerheitsproblem f¨
ur
B¨
uchi-Automaten und entscheidet deshalb das Komplement des
Formelauswertungsproblems f¨
ur LTL.
ABER:
I Die Menge Q hat Gr¨
oße |Q| ∈ O(|W | · 2|ϕ| ), deshalb ben¨otigt die Variable x
Speicherplatz O(log |W | + |ϕ|).
I Der Algorithmus ist also ein nichtdeterministischer Algorithmus, der
polynomiellen Speicherplatz ben¨
otigt.
I
Damit haben wir:
das Komplement des Formelauswertungsproblems f¨
ur LTL ist in NPSPACE.
PSPACE = NPSPACE (nichtdet. Algorithmen kann man in det. Algorithmen umformen,
wobei sich der Speicherverbrauch quadriert (Satz von Savitch))
und PSPACE ist unter Komplement abgeschlossen.
Damit ergibt sich schließlich
Satz 3.28
Das Formelauswertungsproblem f¨
ur LTL ist in PSPACE.
3.5 Weitere Zeitlogiken
Erweiterung von LTL um Pfadquantoren
3. Temporale Logik
Grundbegriffe linearer Zeitlogik LTL
B¨uchi-Automaten
Ein Algorithmus f¨ur das G¨ultigkeitsproblem f¨ur LTL
Formelauswertung von LTL-Formeln
Weitere temporale Logiken
Computation tree logic (CTL) kennt nur noch Kripke-Semantik (keine
Pfad-Semantik auf Belegungsfolgen mehr) und erlaubt Quantifizierung
von Pfaden durch Kripke-Modelle mit den Pfad-Quantoren E und A.
Wir geben nur einen kurzen informellen Einblick.
3.5.70
Beispiel
E . . . es gibt einen Pfad mit der aktuellen Welt als Startpunkt
A . . . f¨ur alle Pfade mit der aktuellen Welt als Startpunkt
M, s0
E(G ¬b2 )
M, s0
E(G(¬b2 ∧ E(F b2 )))
M, s0
¬ E(F(b1 ∧ b2 ))
M, s0
A(G(¬b1 ∨ ¬b2 ))
s0
n1 n2
s1
a1 n2
n 1 a2
a1 a2
s4
b1 n2
s3
b1 a2 s6
s2
n1 b2
s5
s 7 a1 b 2
3.5.71
Pfad-Quantoren
s0
n1 n2
s1
a1 n2
n 1 a2
a1 a2
s4
b1 n2
s3
b1 a2 s6
s2
n1 b2
s5
s 7 a1 b 2
I
Sicherheit: AG ¬(b1 ∧ b2 )
I
Lebendigkeit: AG(a1 → AFb1 )
I
kein Blockieren: AG(n1 → EXa1 )
I
Flexibilit¨at: EF(b1 ∧ E[b1 U(¬b1 ∧ E[¬b2 U b1 ])])
3.5.72
Pfad-Quantoren
s0
n1 n2
s1
a1 n2
n 1 a2
a1 a2
s4
b1 n2
s3
b1 a2 s6
s2
n1 b2
s5
s 7 a1 b 2
I
Sicherheit: AG ¬(b1 ∧ b2 )
I
Lebendigkeit: AG(a1 → AFb1 )
I
kein Blockieren: AG(n1 → EXa1 )
I
Flexibilit¨at: EF(b1 ∧ E[b1 U(¬b1 ∧ E[¬b2 U b1 ])])
3.5.72
Pfad-Quantoren
s0
n1 n2
s1
a1 n2
n 1 a2
a1 a2
s4
b1 n2
s3
b1 a2 s6
s2
n1 b2
s5
s 7 a1 b 2
I
Sicherheit: AG ¬(b1 ∧ b2 )
I
Lebendigkeit: AG(a1 → AFb1 )
I
kein Blockieren: AG(n1 → EXa1 )
I
Flexibilit¨at: EF(b1 ∧ E[b1 U(¬b1 ∧ E[¬b2 U b1 ])])
3.5.72
Pfad-Quantoren
s0
n1 n2
s1
a1 n2
n 1 a2
a1 a2
s4
b1 n2
s3
b1 a2 s6
s2
n1 b2
s5
s 7 a1 b 2
I
Sicherheit: AG ¬(b1 ∧ b2 )
I
Lebendigkeit: AG(a1 → AFb1 )
I
kein Blockieren: AG(n1 → EXa1 )
I
Flexibilit¨at: EF(b1 ∧ E[b1 U(¬b1 ∧ E[¬b2 U b1 ])])
Temporale Logiken
LTL: linear-time temporal logic
I Formeln mit temporalen Operatoren, ohne Pfad-Quantoren
F(G x → y U z)
I g¨
ultige Formel wird in jedem Modell auf jedem Pfad erf¨
ullt
I Modell erf¨
ullt Formel,
wenn sie auf jedem Pfad aus s durchs Modell erf¨
ullt wird
CTL: computation tree logic, branching-time temporal logic
I Formeln mit kombinierten Pfad-Quantoren und temporalen
Operatoren
AF(EGx → A(y U z))
CTL+ :
I
Formeln mit alternierenden Pfad-Quantoren und temporalen
Operatoren
E(G x → (y U(A(x ∧ F z))))
CTL? :
I
Formeln mit Pfad-Quantoren und temporalen Operatoren
A(F x ∧ E(G F x → (y U z)))
Komplexit¨
atsresultate
Erf¨
ullbarkeit /
G¨
ultigkeit
LTL
CTL
CTL+
CTL?
PSPACE
EXPTIME
EEXPTIME
EEXPTIME
[SC85]
[FL79]
[JL03]
[VS85]
[Pr80]
Formelauswertung
PSPACE
P
∆p2
PSPACE
[SC85]
[CES86]
[LMS01]
[CES86]
[Sc02]
NP
∆p2
P
PSPACE
EXPTIME
EEXPTIME
coNP
S
k
O(nk )
Zeit
S
O(nk )
Platz
k
S
k
k
O(2n )
Zeit
S
nk
k
O(22 )
Zeit
3.5.74
Komplexit¨
atsresultate
Erf¨
ullbarkeit /
G¨
ultigkeit
LTL
CTL
CTL+
CTL?
PSPACE
EXPTIME
EEXPTIME
EEXPTIME
[SC85]
[FL79]
[JL03]
[VS85]
[Pr80]
Formelauswertung
PSPACE
P
∆p2
PSPACE
[SC85]
[CES86]
[LMS01]
[CES86]
[Sc02]
Literatur:
[FL79]
[Pr80]
[VS85]
[SC85]
[CES86]
[Sc02]
[LMS01]
[JL03]
Fischer, Ladner 1979
Pratt 1980
Vardi, Stockmeyer 1985
Sistla, Clarke 1985
Clarke, Emerson, Sistla 1986
Schnoebelen 2002
Laroussinie, Markey, Schnoebelen 2001
Johannsen, Lange 2003
3.5.74

DRK und Feuerwehr Brackenheim DRK und Feuerwehr

Theoretische Informatik II

Gm Pythagoras - Aufgaben - B.S

Übungsblatt 2

Was bisher geschah: klassische Aussagenlogik

Theoretische Informatik II

Blatt 3 - Technische Universität München

Kfz-Mechatroniker (w/m) in der Automobilproduktion

Kfz-Mechatroniker Entwicklungswerkstatt (w/m)

Lösung - Technische Universität München