Gödel, Escher, Bach, Isabelle SoSe 98

2. Aufgabenblatt

Ausgabe: 29.06.1996 Bearbeitungszeit: eine Woche

Sofie Czernik Christoph Lüth

Aufgabe 1: Bekannte Theoreme

Zeige, zuerst auf dem Papier, dann in Isabelle — 1. Den K-Kombinator: P → (P → Q)

2. Den S-Kombinator: (P → Q → R) → (P → Q) → (P → R) Hinwies: Zuerst werden die drei Implikationen im S-Kombinator durch Rückwärtsresolution mit der Einführungsregel für die Implikation impI aufgelöst. Danach werden Eliminationsresolutionen mit den Eliminationsregeln der Implikation (impE, mp) durchgeführt (warum?), bis zwei Beweisziele übrig blieben, die durch Annahme bewiesen werden.

3. Den Satz von Pierce: P ∨¬P → ((P → Q) → P) → P (Zusatzaufgabe)

Aufgabe 2: Animal Kingdom

1. Erweitere die Theorie Animals.thy (siehe Webseite) um die restlichen im Logikskript angeführten Begriffe und Regeln.

2. Zeige dann, daß (a) Pinguine Eier legen.

(b) Adler Eier legen und fliegen können.

3. Welche der folgenden Aussagen läßt sich beweisen:

(a) Pinguine können fliegen.

(b) Ein Tiger ist kein Pottwal, und ein Pottwal ist kein Tiger.

(c) Ein Pottwal ist kein Fisch.

4. Erweitere die Theorie um die Begriffe istMaus und die binären Begriffe

istGroesserAls und frißt, und folgende Regeln:

• Eine Maus ist ein Säugetier; • Adler und Uhu fressen jeweils Mäuse und Schlangen (das sind 4

einzelne Regeln)

• Regeln über die Größe nach eigenem Ermessen: z.b. sind Pottwale größer als alle anderen Tiere.

5. Zusatzaufgabe: Welche Regeln wären zusätzlich nötig, um zeigen zu können, daß es einen Vogel gibt, der Säugetiere frißt?