Prof. Dr. M. Kreuzer Abgabe: 01.11.2002, 14h

Logik für Informatiker

Übungsblatt 3

Aufgabe 6: Die UNO-Resolution Man prüfe mittels der Resolutionsmethode, ob

F = ((U ⇒ N) ∨ (¬O ∧ U)) ∧ (U ∨ N) ∧ (¬((¬O ∧ U) ∨ N))

erfüllbar ist.

Aufgabe 7: Man zeige mit der Resolutionsmethode:

a) F = (A ⇒ B) ∨ (A ∧ ¬(B ∨ C)) ∨ (A ∧ C) ist Tautologie.

b) B ist eine Folgerung aus der Formelmenge {(A ∨ B ∨ ¬C), (A ∨ B ∨ C), (¬A ∨ B)}.