Übungsblatt 1 - Logik

1. Auf den überarbeiteten Folien, Folie 87 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 borders(c1,c2) beschreibt, in der wievielten T_P-Runde es abgeleitet wird
2. Auf Folie 88 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. S. 91 [korrigierte Folie!]) reachable(e,h).
   Versuchen Sie, reachable(br,e) zu beweisen.
4. Betrachten Sie das win-move-Game (Folie 99). 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. [neu: einfache Aufgabe zum Tableau-Kalkül]
   Betrachten Sie die beiden 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 beiden 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 96 wird in der Vorlesung diskutiert und einige Dinge unter Verwendung des Tableaukalküls (ab Folie 101) bewiesen. Machen Sie dasselbe für die Ontologie von Folie 97.