Gödel, Escher, Bach, Isabelle

Sofie Czernik, Christoph Lüth

Sommersemester 1998 Kursfahrplan

• Grundlagen von Isabelle I— III

• Beispiel: Schaltungslogik

• Beispiel: Naive Mengenlehre

• Beispiel: Spezifikation und Synthese von Programmen Isabelle: Generischer Taktischer LCF-Beweiser

• Generisch: mehr als eine Logik

• Taktisch: selbstprogrammierbare Beweisprozeduren

• LCF:

– implementiert in ML

– Benutzerschnittstelle ML

– Theoreme als abstrakter Datentyp

Christoph Lüth  Gödel, Escher, Bach, Isabelle  3

Beweisen in Isabelle • Natürliches Schließen

• Vorwärtsresolution (neue Theoreme)

• Rückwärtsresolution (Beweisarbeit)

Theorien • Repräsentiert durch externe Textdateien

• Definition von – Typen

– Konstanten, Funktionen

– Syntax

– Axiome

• Hierarchie von vordefinierten Theorien (e.g. HOL, Nat, Arith)

Christoph Lüth  Gödel, Escher, Bach, Isabelle  5

Meta-Variablen

• Meta-Variablen ?x:

Beliebig, können instantiiert werden.

• Objekt-Variablen x:

Beliebig aber fest, können nicht instantiiert werden.

• Beispiel: ?s = ?s vs. s = s Meta vs. Objekt II

• Meta-Implikation: Inferenzregel der Logik

• Objekt-Implikation: formelbildende Operation

• Beispiel: modus ponens

             \frac{P → Q P}{Q}  [| ?P --> ?Q; ?P |] ==> ?Q

• Weitere Syntax:

? x.P x für ∃x.P x, ! x.P x für ∀x.P x,
P | Q für P ∨ Q,  P & Q für P ∧ Q.
Christoph Lüth  Gödel, Escher, Bach, Isabelle  7