Prof. Dr. M. Kreuzer Abgabe: 26.01.2004, 12.15 Uhr Peter Ackermann

Logik für Informatiker

Übungsblatt 13

Aufgabe 30: Seien F, G temporallogische Formeln. Drücken Sie die folgenden prädikatenlogischen Übersetzungen von zweistelligen Operatoren temporallogisch aus:

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

2. F while G := ∃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})

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

4. F atnext G := ∃y : (P (x, y) ∧ F^{∗}|_{x↦y} ∧ G^{∗}|_{x↦y} ∧ ∀z : ((P (x, z) ∧ P (z, y)) ⇒ (¬G)^{∗}|_{x↦z})) ∨ ∀y : (P (x, y) ⇒ ¬G^{∗}|_{x↦y})

Aufgabe 31: Seien A, B Aussagensymbole. Zeigen Sie, dass

(□A ∧ (¬A before B)) ⇒ ¬♢♢B

eine Tautologie ist.