Übungsblatt 1 - Logik

Besprechung am [noch festzulegen].
  1. Auf Folie 92 ist eine Aufgabe zum TP-Operator zu finden.
  2. Auf Folie 93 wird das Programm um die Regel
         unreachable(X,Y) :- country(X), country(Y), not reachable(X,Y). 
    ergänzt. Verdeutlichen Sie sich daran das Prinzip der Stratifizierung.
  3. Beweisen Sie ausgehend von dem o.g. Programm und beweisen Sie per Resolutionsverfahren (vgl. Folien 95, 96) reachable(e,h).
    Versuchen Sie, reachable(br,e) zu beweisen.
  4. Betrachten Sie das win-move-Game (Folie 104). Die Positionen seien p1,p2,...
  5. Betrachten Sie die folgenden Formeln:
    F1:    forall x: (p(x) -> exists y: q(x,y))
    F2:    forall x: exists y: (p(x) -> q(x,y))
    F3:    exists y: forall x: (p(x) -> q(x,y))
    Überprüfen Sie die Gültigkeit der folgenden Aussagen:
  6. Die Ontologie auf Folie 109 wird in der Vorlesung diskutiert und einige Dinge unter Verwendung des Tableaukalküls (ab Folie 125) bewiesen. Machen Sie dasselbe für die Ontologie von Folie 110.