modallogik (aussagenlogisch) · ki, ss 06, folien modal, seite 11, 22. juni2006. beispiel: wise man...

Modallogik (aussagenlogisch)

Zur Formulierung und Reprasentation von Aussagen,

die uber die Aussagenlogik hinausgehen.

Meist”modale“ Einschrankung

”Bald wird es regnen“

”Moglicherweise ist die Erde eine Kugel“ .

”Ich weiß, dass es niemand gibt, der alles weiß “ .

”Es ist verboten, bei roter Ampel uber die Kreuzung zu fahren “

”Togo wird nie Weltmeister“

”Brasilien wird immer wieder Weltmeister“

KI, SS 06, Folien Modal, Seite 1, 22. Juni2006

Modallogik (aussagenlogisch)

Einfachste Variante: 3, 2 als Modaloperatoren und Formeln

2 3

”∀ “

”∃ “

Immer gilt: Irgendwann gilt:Es ist bekannt: Es ist moglich:Es ist geboten: Es ist erlaubt:

I.a.: Simultan mehrere (auch parametrisierte) Operatoren2A, 2B, 3C: A glaubt . . . , B glaubt . . . , C halt fur moglich . . .


Logikformalismen: Beispiele und Motivation

philosophische Logik

untersucht u.a. Modallogik und Varianten

Fragestellung der philosophischen Logik:

Welche Ableitungsverfahren sind immer richtig

bzw. unter bestimmten Umstanden richtig?


Logikformalismen: Modellierung der Zeit

Diskrete Zeit

Operatoren:”vorher“,

”nachher“,

”immer“,

”manchmal“ usw.

2F : F gilt immer in der Zukunft3F : F gilt irgendwann in der Zukunft.

In dieser Modellierung sollte gelten: 22F ⇔ 2F

lineare Zeit: deterministische Prozesse

(32F ) ⇒ (23F )

”verzweigende“Zeit: nicht-deterministische Prozesse

Andere Modaloperatoren erforderlich


Bemerkungen zu CTL∗, CTL, LTL

Logik CTL∗ (computation tree logic):

ist Verallgemeinerung einer Modallogik zu verzweigender Zeit

mit Anwendung in Hardwareverifikation.

Spezialisierung: LTL: linear time logic

Modallogik CTLWelten Welten (Zustande)Erreichbarkeit (nachste Welt) Erreichbarkeits-Pfade

Es gibt keine Endwelt


Logik des Erlaubten und Verbotenen

(Normative Logik, Deontic Logic)

2F : F ist geboten; F muss gelten; bzw. F ist obligatorisch.3F : F ist erlaubt.

In dieser Logik sollte gelten, dass obligatorisches auch erlaubt sein

sollte. D.h.

2F ⇒ 3F


Logik des Wissens (epistemische Logik)

2F : F ist bekannt.3F : F ist glaubhaft.

bekannte Fakten sind richtig sind: D.h. 2F ⇒ F

Dieses Axiom ist falsch in einer Zeitlogik mit

2 ≡”

im nachsten Zustand gilt“


Variante einer Logik des Wissens

(autoepistemische Logik)

Glauben an gewisse Fakten.

2F : F wird geglaubt.3F : F ist moglich (¬F wird nicht geglaubt).

Die Axiome dazu:

2(F ⇒ G) ⇒ (2F ⇒ 2G)2F ⇒ 22F positive Introspektion¬2F ⇒ 2(¬2F ) negative Introspektion

Modellierungsmoglichkeit:”nichtmonotone“ Logik


Logik des Beweisens

2F : F ist beweisbar3F : F ist nicht widerlegbar

In dieser Logik sollte gelten, dass beweisbare Fakten richtig sind: D.h.

2F ⇒ F

Man kann z.B. formulieren:

”F gilt, aber ist nicht beweisbar: F ∧ ¬2F .


parametrisierte Modaloperatoren

parametrisierte Modaloperatoren in einer Logik des Wissens mit

mehreren Akteuren:

A F A weiß, dass F giltA (¬ B F ) A weiß, dass B nicht weiß, dass F wahr ist.

Extremfall: dynamische Logik zur Programmverifikation.

z.B. P F : nach (jeder) Ausfuhrung des Programms P gilt,

falls das Programm terminiert, die Formel F .


Beispiel: Wise man puzzle

Drei Weise sitzen sich gegenuber, so dass jeder den anderen von vorne

sieht.

Jedem wird ein roter oder blauer Punkt auf die Stirn gemalt. Minde-

stens einer der Punkte ist rot, was den Weisen bekannt ist. Jeder sieht

die Stirn der anderen aber nicht seine eigene.

Nach einer Zeit des Uberlegens sagt der erste Weise:

”Ich weiß nicht, welche Farbe der Punkt auf meiner Stirn hat.“

Nach weiterem Uberlegen sagt der zweite Weise:

”Ich weiß auch nicht, welche Farbe der Punkt auf meiner Stirn hat.“

Kurz danach sagt der dritte Weise:

”Jetzt weiß ich, welche Farbe der Punkt auf meiner Stirn hat“.

Welche?


Beispiel: Wise man puzzle

Der Punkt ist rot!: Argumentation:

Seien 1,2,3 die Weisen.

1 kann nur RR oder RB sehen, sonst wusste er seine Farbe.

2 kann nur RR oder RB sehen, sonst wusste er seine Farbe.

3 kann jetzt alle Wissenstande nutzen:

Wenn er BB sieht, dann weiß er dass er R hat.

Wenn er RB sieht, dann kann er nicht B haben, da 1,2 ihre Farbe

nicht kennen.

Wenn er RR sieht, und hat B: Dann wusste 2, dass er R hat.

Also hat 3 die Farbe R auf der Stirn.


Wise Man Puzzle

Die Axiome dazu in einer Modallogik mit mehreren ModaloperatorenA F bedeutet: A weiß, dass F gilt.

einfache Annahme: die Aussagen unten sind in allen Welten gultig.

(RA ∨RB ∨RC)RA ⇒ B (RA) ∧ C (RA)RB ⇒ A (RB) ∧ C (RB)RC ⇒ A (RC) ∧ B (RC)¬RA ⇒ B (¬RA) ∧ C (¬RA)¬RB ⇒ A (¬RB) ∧ C (¬RB)¬RC ⇒ A (¬RC) ∧ B (¬RC)

¬( A RA)) ∧ ¬( A ¬RA))¬( B RB) ∧ ¬( B ¬RB))

|= C RC ? (in der Anfangswelt)


Aussagenlogische Modallogik

Syntax

Wie Aussagenlogik

Zusatz: zwei Modal-Operatoren 2 und 3:

Neue Grammatikregeln:

F ::= 2F | 3F (auch geschachtelt)

Beispiele 2X ∨3X2(X ∧ Y ) ⇔ 2X ∧ 2Y2((3X) ∨ 2¬(2Y ))


Semantik

Analog zur Aussagenlogik

Nur fur 2 und 3 ist eine neues Konzept notwendig

Achtung: 2 und 3 sind nicht wahrheitsfunktional

D.h. es gibt keine Wahrheitstafel fur 2 und 3.


Kripke-Semantik

Modallogische Semantik:benotigt strukturierte Menge von aussagenlogischen Interpretationen.

moglichen Welten Menge WErreichbarkeitsrelation R binare Relation auf W

w4

w1w2

w3


Kripke-Semantik

Kripke-Rahmen

(Kripke-Frame)

Paar (W, R)

Kripke-Struktur Tripel (W, R, I)fur w ∈ W ist I(w) eineaussagenlogische Interpretationmit I(w1) = I(w2) ⇔ w1 = w2


Beispiel

Sei K die Kripkestruktur:

A,− Bw2

w1A,B

Dannn gilt die Formel 3A in K,

aber nicht 3B.


Beispiel

Sei K die Kripkestruktur:

−A,B

w1w2

w3

w4

A,B

A,−B

A,−B

Dannn gilt die Formel 2(A ∨B) in K,

aber nicht 3B.


Gultigkeit einer Formel

F gultig in K = (W, R, I), falls fur alle w ∈ W : w |= F .Notation: K |= F .

F Tautologie, falls fur alle K = (W, R, I): K |= F .

F erfullbar, falls es ein K = (W, R, I) gibt mit: K |= F .

F gultig in (W, R), falls fur alle I gilt: (W, R, I) |= F .


Semantische Folgerung, Deduktionstheorem

F ist semantische Folgerung (logische Konsequenz) von {F1, . . . , Fn},falls fur alle Kripke-Strukturen K gilt:

Wenn K |= {F1, . . . , Fn}, dann auch K |= F .

Notation: {F1, . . . , Fn} |= F .


Deduktionstheorem gilt in der Modallogik

Aussage F1 ∧ . . . ∧ Fn ⇒ F ist Tautologie

ist aquivalent zu {F1, . . . , Fn} |= F

Verwendung der Semantik.

”⇒“: Es gelte F1, . . . , Fn |= F und sei K eine Kripke-Struktur.

Wenn ein Fi, i = 1, . . . , n nicht gilt in K, dann ist F1 ∧ . . . ∧ Fn falsch in

K,

also gilt K |= F1 ∧ . . . ∧ Fn ⇒ F .

Wenn alle Fi in K gelten, dann auch F1 ∧ . . .∧Fn, nach Voraussetzung

auch F , also auch K |= F1 ∧ . . . ∧ Fn ⇒ F .

”⇐“:


Einige einfache Eigenschaften

• Wenn F eine Tautologie ist, dann ist auch 2F eine

Tautologie.

• w |= 20 bedeutet, dass w eine Sackgasse ist:von w aus ist keine Welt mehr erreichbar, denn in

keiner Interpretation ist 0 wahr.

• w |= 2220 impliziert, dass man von w aus hochstens

2 R-Schritte machen kann.

• 21 ist immer eine Tautologie


Aquivalenzen und Nichtaquivalenzen

alle aussagenlogischen Tautologien geltenund:

2(F ∧G) ⇔ 2F ∧ 2G3(F ∨G) ⇔ 3F ∨3G3(F ∧G) 6⇔ 3F ∧3G2(F ∨G) 6⇔ 2F ∨ 2G¬(2F ) ⇔ 3(¬F )¬(3F ) ⇔ 2(¬F )2(F ⇒ G) ⇒ (2F ⇒ 2G)


Die einfachste Modallogik: K

Diese entspricht der angegebenen Kripke-Semantik.

Folgende Herleitungsregeln fur K-Tautologien sind ausreichend:

1. Alle klassischen Tautologien

2. 2(A ⇒ B) ⇒ (2A ⇒ 2B)

3.A ⇒ B A

B

4.A

2A


Tableaukalkul fur die Logik K

Ein Tableau ist ein Baum mit zwei Arten von Knoten:

w;F w ist ein Name fur eine Welt.R(w1, w2) Erreichbarkeitsrelation zwischen w1, w2.

Ein Pfad P ist geschlossen,

wenn w; 0 auf dem Pfad P

oder w, A und w;¬A ist auf dem Pfad P (mit gleichem w)

Ein Tableau ist geschlossen, wenn alle Pfade geschlossen sind.


Tableaukalkul fur K

Expansionsregeln:• aussagenlogische Tableauregeln; w bleibt erhalten

•w;3F

R(w, w′) und w′;Fwerden an allen Pfaden durch w;3F angehangt (w′ ist neue Welt)

•w;2F

w′;Fwird an allen Pfaden durch w;2F angehangt, dieR(w, w′) enthalten, aber noch nicht w′;F .

• w;¬2F wird wie w;3(¬F ) behandelt.und w;¬3F wird wie w;2(¬F ) behandelt.


Tableau-Kalkul Beispiel

0;¬(2(F ∧G) ⇒ (2F ∧ 2G))

0;2(F ∧G)

0;¬(2F ∧ 2G)

fffffffffffffffffffffffff

XXXXXXXXXXXXXXXXXXXXXXXXX

0;¬2F 0;¬2G

R(0,1) R(0,2)

1;¬F 2;¬G

1;F ∧G 2;F ∧G

1;F 2;G


Kalkul Beispiel0;¬(2(F ⇒ G) ⇒ (2F ⇒ 2G))

0;2(F ⇒ G)

0;¬(2F ⇒ 2G)

0;2F

0;¬2G

R(0,1)

1;¬G

1;F

1;F ⇒ G

ffffffffffffffffffffffffffff

XXXXXXXXXXXXXXXXXXXXXXXXXXXX

1;¬F 1;G


Tableaukalkul fur K: Eigenschaften

Der Tableaukalkul fur K terminiert, ist korrekt und vollstandig

D.h. Das vervollstandigte Tableau ist geschlossen genau dann

wenn man einen K-Widerspruch eingibt.

Begrundung: neu eingefuhrte Formeln sind kleiner als bereits vorhandeneDie Lange der R-Ketten is beschrankt.

Wenn das vollstandige Tableau nicht geschlossen ist:

nicht-geschlossene Pfade reprasentieren Modelle der Formel

bzw. Gegenbeispiele (der Formel vor der Negation)


Tableau liefert Modell

Betrachte A ⇒ 2A:

0;¬(A ⇒ 2A)

0;A

0;¬(2A)

R(0,1)

1;¬A

Das Modell kann man direkt ablesen.


Modallogik: Rahmen-Axiome

Korrespondenztheorie:

Charakterisierung einer (Modal-Logik) durch Rahmenaxiome

Man definiert Modallogikvarianten

mittels Eigenschaften der zulassigen Rahmen.

Meist: Eigenschaften der Erreichbarkeitsrelation


Modallogik: Rahmen-Axiome

Name der Modallogik Eigenschaft der Relation(des Axioms) im Rahmen (W, R)K R ist beliebigT R ist reflexivK4 R ist transitivS4 R ist reflexiv und transitivB R ist symmetrischS5 R ist reflexiv, transitiv und symmetrisch5 R ist euklidischD R ist seriell (unbeschrankt)D4 R ist seriell und transitivS4.2 R ist reflexiv, transitiv und konfluentGrz R: jede unendliche R-Kette w1 R w2 . . . hat

nur endliche viele wi.Aussagenlogik es gibt genau eine Welt w0, und w0 R w0

gilt


Relations-Eigenschaften

reflexiv ∀w : R(w, w)transitiv ∀w1, w2, w3 : w1 R w2 ∧ w2 R w3 ⇒ w1 R w3symmetrisch ∀w1, w2 : w1 R w2 ⇒ w2 R w1seriell ∀w∃w′ : w R w′

euklidisch ∀w1, w2, w3 : w1 R w2 ∧ w1 R w3 ⇒ (w2 R w3)konfluent (falls R reflexiv und transitiv)

∀w1, w2, w3 : (w1 R w2 ∧ w1 R w3)⇒ (∃w4 : w2 R w4) ∧ w3 R w4


Tautologien einer Logik

Beispiel

Die Tautologien der Logik K4 sind

genau die modallogischen Formeln F , so dass

∀k : k |= F fur alle Interpretationen k gilt,

die einen K4-Rahmen haben,

d.h. deren Erreichbarkeitsrelation transitiv ist.


Abhangigkeiten zwischen den Logiken

K

T

K4D

S4

D4

B

DB

S5

Aussagenlogik


Axiomenschemata

Name (alt. N) Formel AnwendungK 2(F ⇒ G) ⇒ (2F ⇒ 2G)T (M) 2F ⇒ F epistemischD 2F ⇒ 3F deontisch4 2F ⇒ 22F Zeit; WissenB F ⇒ 23F5 (E) 3F ⇒ 23F WissenM (G) 23F ⇒ 32FL (H, Lem0) 2((A ∧ 2A) ⇒ B) ∨ 2((B ∧ 2B) ⇒ A)

3 (H, H+0 , Lem) 2(2A ⇒ B) ∨ 2(2B ⇒ A)

2 (G) 32F ⇒ 23F ZeitG (W) 2(2F ⇒ F ) ⇒ 2FDum 2(2(F ⇒ 2F ) ⇒ F ) ⇒ (32F ⇒ 2F )Grz 2(2(F ⇒ 2F ) ⇒ F ) ⇒ F )


Axiomenschemata: Erlauterungen

epistemische und deontische Logiken

Name Formel ErklarungT 2F ⇒ F Was ich weiß, das giltD 2F ⇒ 3F

2F ⇒ ¬2¬F Wenn ich F glaube, dann glaube ich das Ge-

genteil nicht4 2F ⇒ 22F Wenn ich F weiß, dann weiß ich dass ich F

weiß(Positive Introspektion)

5 3F ⇒ 23F¬2F ⇒ 2¬2F wenn ich F nicht weiß, dann weiß ich dass ich

F nicht weiß.(Negative Introspektion)

(Axiome sind teilweise umgeformt)


Allgemeiner Tableau-Kalkul fur L mit

Hornklauseltheorie fur R• aussagenlogische Tableauregeln; w bleibt erhalten

•w;3F

R(w, w′) und w′;Fwerden an allen Pfaden durch w;3F angehangt(w′ ist neue oder bereits im Pfad vorkommende Welt)

•w;2F

w′;Fwird an allen Pfaden durch w;2F angehangt, dieR(w, w′) enthalten, aber noch nicht w′;F .

• R(w1, w2) wird am Pfad P angehangt,wenn es aus den R-Axiomen und den R-Relationen im Pfad folgt.

• w;¬2F wird wie w;3(¬F ) behandelt.und w;¬3F wird wie w;2(¬F ) behandelt.


Generischer Tableau-Kalkul TKL

Optimierungsversuch: Fallunterscheidungen vermeiden

Eine Logik L wird festgehalten.

Pro Logik ist ein spezieller Algorithmus erforderlich, der geschlossene

Pfade erkennt.

Ein Tableau ist ein Baum mit Knoten p;F

p: R-Sequenz: Folge von Termen (mit Variablen), die die Er-

reichbarkeit reprasentierenTerme reprasentieren Interpretationen (Welten)

F Formel ist gultig in der Endwelt von p.


Generischer Tableau-Kalkul

R-Sequenzen

Anmerkungen:

Beispiel fur R-Sequenzen: 0 oder 0 · x · g(x)

Achtung: die R-Sequenz 0 · . . . · x sagt noch nicht aus,

dass eine Instanz fur x existiert

Die Eigenschaften der Erreichbarkeitsrelation

durfen benutzt werden.


Kalkul Beispiel

0;¬(2(F ∧G) ⇒ (2F ∧ 2G))

0;2(F ∧G)

0;¬(2F ∧ 2G)

0 · x;F ∧G

0 · x;F

0 · x;G

ffffffffffffffffffffffffffff

XXXXXXXXXXXXXXXXXXXXXXXXXXXXX

0;¬2F 0;¬2G

0 · a;¬F 0 · b;¬G


Kalkul Beispiel (2)

Das Tableau im Beispiel ist geschlossen; (Definition folgt)

Disjunktion nur bei geschlossenen R-Sequenzen erlaubrt.


Invarianten von R-Sequenzen

Fur R-Sequenzen p gilt (aufgrund der Erzeugung):

Wenn p = t1 . . . tk · x · . . ., dann gilt:

• In jeder R-Sequenz q = s1 . . . sj · x, . . . des Tableaus istj = k und s1 . . . sj = t1 . . . tk

• x kommt nicht in t1 . . . tk vor.


Zur Definition geschlossener Pfade

Fixiere Logik L

P Tableaupfad:RS(P ): Menge der R-Sequenzen p in Tableaupfad P .

Erzeugung von Erreichbarkeitsrelationen Q(P ) im Pfad P :

• Falls t1 · . . . · tn ∈ RS(P ), tn keine Variable,σ Grundsubstitution,und 0 R σ(t1), . . . , σ(tn−2) R σ(tn−1) ∈ Q(P );dann auch σ(tn−1) R σ(tn) ∈ Q(P ).

• Wenn Q(P ) |=L s R t fur Grundterme s, tdann auch s R t ∈ Q(P )

Q(P ) besteht aus allen herleitbaren Grund-Relationen


Test von Eigenschaften von R-Sequenzen

Gegeben: L, P und Q(P ):

1. σ(p) ist L-Instanz von p = t1 · . . . · tn,wenn σ Grundsubstitution ist,

wenn 0 R σ(t1) in Q(P ), und

σ(ti) R σ(ti+1) ∈ Q(P ) fur i = 1, . . . , n− 1,

2. p ist L-erfullbar, wenn es eine L-Instanz von p gibt.

3. p und q sind L-kompatibel,wenn es Grundinstanzen p′ und q′ von p und q bzgl Q(P )

gibt, so dass p′ und q′ die gleiche End-Welt haben.

Notwendig: Algorithmen fur diese Eigenschaft in jeder Logik L.


geschlossene Pfade und Tableaus

Gegeben: Logik L

Definition Ein Pfad P ist L-geschlossen, gdw.

es gibt zwei markierte Formeln p, F und q, G auf P , so dass

p, q L-kompatibel bzgl P

und F, G sind L-komplementare Literale (Formeln).

Oder p; 0 ist auf dem Pfad, und p ist L-erfullbar.

Ein Tableau ist L-geschlossen,

gdw alle Pfade L-geschlossen sind


Tableau-Expansionregeln fur TKL

p;¬¬F

p;F

p;α

p;α1p;α2

p;β

p;β1 | p;β2p enthalt keine Variablen

p;β

p′;βp′ ist L-Instanz von p im Pfad

p;3F

p · f(x1, . . . , xn);Ff ist neu und xi sind die Variablen in p

p;2F

p · x;Fx ist neue Variable


Optimierte Algorithmen fur Logiken K, D, B, T,

S4, S4.2, S5

Logik K: Keine Bedingungen an die Relation.

Kompatibel-Test: Unifikation der R-Sequenzen als n-Tupel+ K-Erfullbarkeitstest

Der Test auf geschlossenes P kann polynomiell implementiert werden.


Beispiele fur K mit Test

Distributivitat von 2 uber ∧.

0;¬(2(F ∧G) ⇒ (2F ∧ 2G))

0;2(F ∧G)

0;¬(2F ∧ 2G)

0 · x;F ∧G

0 · x;F

0 · x;G

fffffffffffffffffffffffffffff

XXXXXXXXXXXXXXXXXXXXXXXXXXXXX

0;¬2F 0;¬2G

0 · a;¬F 0 · b;¬G


Beispiele fur K

Distributivitat von 2 uber ∧ (andere Richtung)

0;¬((2F ∧ 2G) ⇒ 2(F ∧G)) 0;2G

0; (2F ∧ 2G) 0 · x;F

0;¬2(F ∧G) 0 · y;G

0;2F

66lllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllll

0 · a;¬(F ∧G)

jjjjjjjjjjjjjjj

TTTTTTTTTTTTTTT

0 · a;¬F 0 · a;¬G


Beispiele fur KDistributivitat von 2 uber ∨ gilt nur in einer Richtung.

0;¬(2(F ∨G) ⇒ (2F ∨ 2G)) 0 · a;¬F

0;2(F ∨G) 0 · b;¬G

0;¬(2F ∨ 2G) 0 · a;F ∨G

0 · x;F ∨G 0 · b;F ∨G

jjjjjjjjjjjjjjj

QQQQQQQQQQQQQ

0;¬2F 0 · a;F 0 · a;G

mmmmmmmmmmmmm

RRRRRRRRRRRRR

0;¬2G

::uuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuu

geschlossen 0 · b;F 0 · b;G

Modell? geschlossen


Beispiele in K

Die andere Richtung der Distributivitat 2 uber ∨ gilt:

0;¬((2F ∨ 2G) ⇒ 2(F ∨G)) 0 · a;¬F

0; (2F ∨ 2G) 0 · a;¬G

nnnnnnnnnnnnn

PPPPPPPPPPPPP

0;¬2(F ∨G) 0;2F 0;2G

0 · a;¬(F ∨G)

77nnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnn

0 · x;F 0 · y;G


Lob’s Axiom impliziert Transitivitat

Lobs Axiom ist 2(2F ⇒ F ) ⇒ 2F .

Instanz F = (P ∧ 2P )


Lob’s Axiom impliziert Transitivitat: Tableau

0;¬((2(2(P ∧ 2P ) ⇒ (P ∧ 2P )) ⇒ 2(P ∧ 2P )) ⇒ (2P ⇒ 22P ))0; (2(2(P ∧ 2P ) ⇒ (P ∧ 2P )) ⇒ 2(P ∧ 2P ))

0;¬(2P ⇒ 22P )0;2P

0;¬22P0 · x;P

0 · a;¬2P0 · a · b;¬P

0;¬2(2(P ∧ 2P ) ⇒ (P ∧ 2P ))0 · c;¬(2(P ∧ 2P ) ⇒ (P ∧ 2P ))

0 · c;2(P ∧ 2P )0 · c;¬(P ∧ 2P )

0 · c;¬Pgeschlossen mit x 7→ c

0;2(P ∧ 2P )0 · y;P ∧ 2P

0 · y;P0 · y;2P0 · y · z;P

geschlossen mit y 7→ a, z 7→ b


Algorithmen fur Logik D

D: Von jeder Welt aus gibt es stets eine erreichbare Welt(R terminiert nicht).

• alle R-Sequenzen sind D-erfullbar• p1 und p2 sind D-kompatibel, wenn sie unifizierbar sind.• Berechenbar in O(n)

Hullenberechnung Q(P ) analog zur K

Zusatz: Man darf Skolemisieren im Fall t R x (siehe Skript)


Beispiele fur Logik D

Das Axiom 2F ⇒ 3F gilt in D:

0;¬(2F ⇒ 3F )0;2F0;¬3F0 · x;¬F0 · y;F

Das Tableau ist geschlossen,

da 0 · x und 0 · y mit x 7→ y gleichgemacht werden konnen,

und da es in D von jeder Welt aus, insbesondere von der initialen Welt

0 aus, eine weitere gibt.



¬20 ist eine D-Tautologie:

0;¬¬200;200 · x; 0

Ist geschlossen, da in D alle R-Sequenzen erfullbar sind.



A ⇒ 3A ist keine D-Tautologie:

0;¬(A ⇒ 3A)

0;A

0;¬3A

0 · x;¬A

Ist nicht geschlossen.


Logik T

T : Die Relation R ist reflexiv.

Es gilt :• Alle R-Sequenzen sind T -erfullbar.• der T -kompatibel-Test von p1 und p2 ist

analog zu Unifikation unter Ausnutzung der Reflexivitat von R:Unifiziere die R-Sequenzen von links nach rechts;Als Rateschritt ist eine Einfugung t R t erlaubt.

Z.B. wurde 0 · x · y mit 0 · a unifizieren durch x = y = a.


Logik B

R ist symmetrisch.

Q(P ) endlich, wenn Entferung 0 – w nicht großer als maximale R-

Sequenzlange.

Kompatibilitatstest: Nutze Symmetrie aus und benutze Q(P ) zum Test

der Erfullbarkeit.

zB 0 · x · g(x) · y und 0 · a sind kompatibel.


Logik S4

Die Relation R ist reflexiv und transitiv.

Alle Pfade sind S4-erfullbar.

Q(P ) kann unendlich sein


Beispiel in S4

In S4 ist nicht beweisbar: 23F ⇒ 32F (das M-Axiom)

0;¬(23F ⇒ 32F )0;23F0;¬32F dies entspricht 23¬F0 · x, 3F0 · y, 3¬F0 · x · a(x), F0 · x · b(x),¬F

Die letzten beiden Welten a(x), b(x) lassen sich nicht gleichmachen,

sind also nicht S4-kompatibel.


Beispiel in S4

In S4 gilt: 32F ⇒ 323F :

0;¬(32F ⇒ 323F )0;32F

0;¬323F0 · a;2F0 · a · x;F

0 · y;¬23F0 · y · b(y);¬3F0 · y · b(y) · z;¬F

Dieses Tableau lasst sich schließen:

a · x;F und y · b(y) · z,¬F werden dann widerspruchlich.

S4-Instanziierung : y 7→ a, x 7→ b(a), z 7→ b(a).


Beispiel in S4

Zeige, dass in S4 323F ⇒ 3F gilt.

0;¬(323F ⇒ 3F )0;323F0;¬3F0 · x,¬F0 · a, 23F0 · a · y, 3F

0 · a · y · b(y), F

Ist geschlossen, da b() von 0 aus erreichbar, bzw. 0 · x und 0 · a · y · b(y)S4-kompatibel sind.


Beispiel in S4

32F ⇒ 2F ist nicht in S4 beweisbar:

0;¬(32F ⇒ 2F )0;32F0;¬2F0 · a;¬F0 · b;2F0 · b · x;F

Ist nicht geschlossen, da die R-Sequenzen 0 · a und 0 · b · x nicht kom-

patibel in diesem Pfad sind.

Instanziierung x 7→ a nicht erlaubt, da b R a nicht gelten muss (nicht

in Q(P )).


Tableaukalkul terminiert nicht fur S4

0;¬(2(2(F ⇒ 2F ) ⇒ F ) ⇒ F )0;2(2(F ⇒ 2F ) ⇒ F )

0;¬F0x; (2(F ⇒ 2F ) ⇒ F )00; (2(F ⇒ 2F ) ⇒ F )

00;¬2(F ⇒ 2F ) 00;F00a;¬(F ⇒ 2F ) geschlossen

00a;F00a;¬2F00ab;¬F

(Transitivitat und Instanz)0b;¬2(F ⇒ 2F ) 0b;F0bc;¬(F ⇒ 2F ) geschlossen

0bc;F0bc;¬2F0bcd;¬F

. . .


Logik S5: Algorithmen

Die Relation ist reflexiv, symmetrisch und transitiv (Aquivalenzrelati-

on).

Alle Pfade sind S5-erfullbar.

Kompatibilitatstest: Betrachte Paare der Endwelten der R-Sequenzen.

R-Sequenzen sind S5-kompatibel in folgenden Fallen:

(r, s), (r, x), (x, y), oder (x, r) und x 6∈ FV (r),

r, s unifizierbar.

(r, s) kann nur vorkommen, wenn vorher instanziiert wurde


Beispiele

In S5 (auch in S4) gilt: 3(F ∨3G) ⇒ 3F ∨3G:


0;¬(3(F ∨3G) ⇒ 3F ∨3G)

0;3(F ∨3G)

0;¬(3F ∨3G)

0 · a;F ∨3G

0;¬3F

0;¬3G

0 · x;¬F

0 · y;¬G

ffffffffffffffffffffffffffffffff

ZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZ

0 · a;F 0 · a;3G

geschlossen 0 · a · b, G

geschlossen, da R transitiv

Beispiel in S5

In S5 ist ebenfalls nicht beweisbar: 23F ⇒ 32F (das M-Axiom)

(Tableau wie bzgl S4):

0;¬(23F ⇒ 32F )0;23F0;¬32F dies entspricht 23¬F0 · x, 3F0 · y, 3¬F0 · x · a(x), F0 · x · b(x),¬F

Die letzten beiden Welten a(x), b(x) lassen sich nicht gleichmachen,sind also nicht S5-kompatibel.

Beachte: In S5 schrumpft das M-Axiom zu 3F ⇒ 2F


Beispiel in S5

In S5 gilt: 3(F ∨ 2G) ⇒ 3F ∨ 2G

Beachte: In S4 gilt diese Formel nicht.


0;¬(3(F ∨ 2G) ⇒ 3F ∨ 2G)

0;3(F ∨ 2G)

0;¬(3F ∨ 2G)

0 · a;F ∨ 2G

0;¬3F

0;¬2G

0 · x;¬F

0 · b;¬G

eeeeeeeeeeeeeeeeeeeeeeeeeeeeeeee

YYYYYYYYYYYYYYYYYYYYYYYYYYYYYY

0 · a;F 0 · a;2G

geschlossen 0 · a · y;G

geschlossen

Normalformen in der Logik S5

In der Logik S5 gilt:

Alle Formeln lassen sich in eine Normalform bringen,

mit folgenden Eigenschaften: Negationszeichen sind direkt vor aussa-

genlogischen Variablen

Es gibt UND-ODER-Verknupfung oberhalb und unterhalb der Modal-

operatoren

Modaloperatoren kommen nicht mehr unter anderen Modaloperatoren

vor.


Normalform-Transformationen in der Logik S5

1. Negation nach innen:

¬¬F → F¬2F → 3¬F¬3F → 2¬F¬(F ∨G) → ¬F ∧ ¬G¬(F ∧G) → ¬F ∨ ¬G

2. Weitere Transformationen (Symmetrie beachten).

(a)

22F → 2F32F → 2F23F → 3F33F → 3F


(b)

3(F ∨G) → 3F ∨3G3(F ∧3G) → 3F ∧3G3(F ∧ 2G) → 3F ∧ 2G

(c)

2(F ∧G) → 2F ∧ 2G2(F ∨3G) → 2F ∨3G2(F ∨ 2G) → 2F ∨ 2G

Modalitaten in S4

In S4 gibt es nur folgende 7 Modalitaten: andere sind aquivalent dazu:

22F ⇔ 2F33F ⇔ 3F3232F ⇔ 32F2323F ⇔ 23F

und folgende Implikationen gelten:

F

F

F

F

F

F

F


Anwendungen in der Zeitlogik (temporale

Logik)

1. in deterministischer (linearer) Zeit: Logik S4.3.1.

2F von jetzt ab gilt stets F .3F irgendwann gilt F

2. verzweigende Zeit (nichtdeterministische Prozesse)2F von jetzt ab gilt stets F3F es ist moglich, dass F in der Zukunft gilt.

(bzw. Es gibt einen moglichen Ablauf des Prozesses, so

dass irgendwann in der Zukunft F gilt.


lineare, diskrete, deterministische Zeit

S4-Kalkul ist anwendbar.

In linearer Zeit gilt z.B. folgendes (euklidische) Axiom:

(3F ∧3G) ⇒ (3(F ∧3G) ∨3(F ∧G) ∨3(3F ∧G)

D.h. Zwei Ereignisse E1, E2 entweder gleichzeitig, oder E1 vor E2 oder

E2 nach E1.


Weitere Modaloperatoren

Vergangenheitsoperatoren: Diese sind dual 2, 3

2 = G gilt ab jetzt immer3 = F gilt irgendwann in der Zukunft2P = H galt immer in der Vergangenheit3P = P galt irgendwann in der Vergangenheit


Weitere Modaloperatoren: Zusammenhange

(die”K-Axiome der Zeit“):

2(F ⇒ G) ⇒ (2F ⇒ 2G)2P (F ⇒ G) ⇒ (2PF ⇒ 2PG)F ⇒ 22PFF ⇒ 2P2F

Fur lineare Zeit braucht man dann auch das duale Axiom:

(3PF ∧3PG) ⇒ (3P (F ∧3PG) ∨3P (F ∧G) ∨3P (3PF ∧G)


Beispiel in einer linearen, diskreten Zeit

Wenn Brasilien Fußballweltmeister ist, und immer wenn Brasilien Fuß-

ballweltmeister ist, ist irgendwann Deutschland wieder Fußballweltmei-

ster ist immer wenn Deutschland Fußballweltmeister ist, ist irgendwann

Brasilien wieder Fußballweltmeister,

dann gilt zu jedem zukuftigen Zeitpunkt, dass danach irgendwann

Deutschland wieder Fußballweltmeister ist.

Axiome:

B,

2(¬B ∨ ¬D)

2(B ⇒ 3D)

2(D ⇒ 3B)

Behauptung: 23D



0;B

0;2(¬B ∨ ¬D)

0;2(B ⇒ 3D)

0;2(D ⇒ 3B)

0;32¬D

0 · a;2¬D a als minimaler Zeitpunkt

0 · a · x;¬D



0 · y;B ⇒ 3D

jjjjjjjjjjjjjjjj

0 · 0;¬B 0 · 0;3D Instanz y 7→ 0

0 · b;D 0 < b mit Teiltableau

0 · z;D ⇒ 3B

jjjjjjjjjjjjjjj

0 · b;¬D 0 · b;3B Instanz z 7→ b

0 · b · c;B b < c

0 · c;B ⇒ 3D

jjjjjjjjjjjjjjjjInstanz y 7→ c

0 · c;¬B 0 · c;3D

0 · c · d;D c < d


Beispiel WM

Jetzt muss man Fallunterscheidung machen nach a < d, a = d, a > d.

Wenn a ≤ d, dann sind 0 · c · d;D und 0 · a · x;¬D widerspruchlich.

Wenn a > d, dann kann man mit der Minimalitat von a argumentieren.

Dazu mussen die Formeln 2 – 4 verschiebbar in der Zeit sein.


Beispiel: Tautologie bei linearer Zeit

(32F ∧32G) ⇒ 32(F ∧G)

Intuitiv: Wenn ab einem Zeitpunkt stets F gilt,

und ab einem Zeitpunkt stets G gilt,

dann gibt es auch einen Zeitpunkt,

ab dem stets beides, namlich F ∧G gilt.

(Dies gilt nicht fur verzweigende Zeit)


Beispiel: Tableau

0;¬((32F ∧32G) ⇒ 32(F ∧G))0;32F0;32G0;¬32(F ∧G)0 · a;2F0 · b;2G0 · a · x;F0 · b · y;G0 · u;¬2(F ∧G)0 · u · c;¬(F ∧G)

a = b a < b b < a0 · a · c;¬F 0 · a · c,¬G 0 · b · c,¬F 0 · b · c,¬G 0 · a · c,¬F 0 · a · c,¬G

geschl. geschl. geschl. geschl. geschl. geschl.


Axiome fur dichte Zeit

3F ⇒ 33F

zwischen zwei Zeitpunkten gibt es immer noch einen weiteren.


Axiome fur diskrete Zeit

F ∧ 2PF ⇒ 32PFF ∧ 2F ⇒ 3P2F


modallogik (aussagenlogisch) · ki, ss 06, folien modal, seite 11, 22. juni2006. beispiel: wise man...

Documents