Prof. Dr. M. Kreuzer ohne Abgabe

Logik für Informatiker

Übungsblatt 15

Aufgabe 35 Sei F eine modallogische Formel, α = (W, R, ξ) eine zu F passende Struktur, wobei R eine Äquivalenzrelation auf W sei, das heißt für alle x, y, z ∈ W gilt

(x, x) ∈ R
(x, y) ∈ R ⇒ (y, x) ∈ R
((x, y) ∈ R und (y, z) ∈ R) ⇒ (x, z) ∈ R.

Sei w ∈ W und sei [w] die Äquivalenzklasse von w. Weiter sei α′ = ([w], R ∩ ([w] × [w]), ξ). Man zeige, dass gilt

α(F, w) = α′(F, w)

Aufgabe 36 Es mögen die Bezeichnungen der Vorlesung für die prädikatenlogische Übersetzung modallogischer Formeln gelten. Für zwei modallogische Formeln F, G seien die Operatoren UNLESS, WHILE, BE-FORE und ATNEXT wie folgt definiert:

F UNLESS G := \begin{matrix}∃y : (P (x, y) ∧ G^{∗}|_{x↦y} ∧ ∀z : ((P (x, z) ∧ P (z, y)) ⇒ F^{∗}|_{x↦z}))∨ \\ ∀y : (P (x, y) ⇒ F^{∗}|_{x↦y}) \end{matrix}

F WHILE G := \begin{matrix}∃y : (P (x, y) ∧ ¬G^{∗}|_{x↦y} ∧ ∀z : ((P (x, z) ∧ P (z, y)) ⇒ (F ∧ G)^{∗}|_{x↦z}))∨ \\ ∀y : (P (x, y) ⇒ F^{∗}|_{x↦y}) \end{matrix}

F BEFORE G := ∀y : ((P (x, y) ∧ G^{∗}|_{x↦y}) ⇒ ∃z : (P (x, z) ∧ P (z, y) ∧ F^{∗}|_{x↦z}))

F ATNEXT G := \begin{matrix}∃y : (P (x, y) ∧ F^{∗}|_{x↦y} ∧ G^{∗}|_{x↦y} ∧ ∀z : ((P (x, z) ∧ P (z, y)) ⇒ ¬G^{∗}|_{x↦y}))∨ \\ ∀y : (P (x, y) ⇒ ¬G^{∗}|_{x↦y}) \end{matrix}

Man gebe eine sprachliche Interpretation der obigen Operatoren und zeige, dass sie sich modallogisch ausdrücken lassen.

Aufgabe 37: Der nicht ganz so wirre Programmierer In einem Programm kommen drei Variablen x_{1}, x_{2}, x_{3} vor, welche alle beim Start des Programms den Wert 0 haben. Im Programmablauf gilt x_{1} < 4 solange x_{2} < 4. Es bleibt x_{3} = 0 bis x_{1} ≥ 4, allerdings muss dieser Fall nicht auftreten.

a) Man drücke die Zusammenhänge zwischen den Variablen durch eine temporallogische Formel aus.

b) Man finde für diese Formel eine Struktur, in der sie gilt, und eine, in der sie nicht gilt.