Gödel, Escher, Bach, Isabelle SoSe 98

1’. Aufgabenblatt

Ausgabe: 22.06.1996 Bearbeitungszeit: eine Woche

Sofie Czernik Christoph Lüth

Aufgabe 1: Zum Warmwerden

Wiederhole (in der Theorie gcd) den Beweis, daß 1 alle Zahlen teilt, und zeige, daß alle Zahlen 0 teilen.

Aufgabe 2: Verschiedene Theoreme in HOL

1. Zeige die Symmetrie und Transitivität der Gleichheit.

2. Zeige jeweils eine Einführungs- oder Eliminationsregeln für den Existenzund den Allquantor.

3. Zeige die Kongruenz der Funktionsapplikation:

(a)

{x = y \atop f(x) = f(y)} arg cong

(b)

\begin{matrix}x = y & f = g \\ f(x) = g(y) \end{matrix} cong

Aufgabe 3: proof debugging

Gegeben ist folgendes Beweisskript:

goal thy "(A|B)&~A-->B";
br impI 1;
br conjE 1;
ba 1;
br conjE 1;
ba 1;
be disjE 1;
br notE 1;
ba 1;
ba 1;
ba 1;

1. Spiele den Beweis in Isabelle nach und kommentiere die Ausführung: welche Regeln werden angewandt, welche Unfikation findet statt, welche Subgoals erscheinen, warum?

2. Wie läßt sich der Beweis verbessern?