Übungsblatt 1 - Logik

1. Auf Folie 92 ist eine Aufgabe zum T_P-Operator zu finden.
   • Berechnen Sie T⁰_P, T¹_P, T²_P, ... für dieses Programm.
   • Geben Sie eine Charakterisierung an, die für jedes abgeleitete Faktum reachable(c1,c2) beschreibt, in der wievielten T_P-Runde es abgeleitet wird
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,...
   • Ein Knoten ist ein "win-Knoten", wenn derjenige Spieler, der am Zug ist gewinnen kann. Ein Knoten ist ein "lose-Knoten", wenn er verliert. Es wird angenommen, dass jeder Spieler optimal spielt.
   • Betrachten Sie ein Spiel, das aus den Kanten (p1,p2), (p2,p3), ... (pn-1,pn) besteht. Welche Knoten sind win-Knoten, welche Knoten sind lose-Knoten.
   • Beschreiben Sie darauf basierend allgemein, welche Knoten in einem beliebigen Spiel win-Knoten sind, welche Lose-Knoten sind, und welche Unentschieden sind.
     
     • betrachten Sie dabei zuerst nur Abzweige, z.B. ein Spiel, das aus den Kanten (p1,p2), (p2,p3), ..., (pn-1,pn) und (p2,pn+1), (pn+1,pn+2), ..., (pn+k-1,pn+k) besteht.
     • betrachten Sie dann Zyklen, aus denen Pfade hinausführen.
   • Wie entsprechen die logischen Quantoren dabei dem Gedanken "gewinnen wollen" bzw. "nicht verlieren wollen" und der Annahme einer optimalen Spielweise beider Teilnehmer?
5. Betrachten Sie die folgenden Formeln:
   F₁:    forall x: (p(x) -> exists y: q(x,y))
   F₂:    forall x: exists y: (p(x) -> q(x,y))
   F₃:    exists y: forall x: (p(x) -> q(x,y))
   Überprüfen Sie die Gültigkeit der folgenden Aussagen:
   • F₁ entails F₂
   • F₂ entails F₁
   • dasselbe für F₁ und F₃
   • Was gilt für F₂ und F₃?
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.