Isabelle, ein generischer ATP Sebastian Wiemer

Einige WWW resources zu Isabelle

• http://www.cl.cam.ac.uk/users/lcp/

Larry Paulsons homepage.

• http://www.cl.cam.ac.uk/Research/HVG/Isabelle/

Die “Isabelle homepage”.

• http://www.cl.cam.ac.uk/Research/HVG/Isabelle/isabelle.html

Die Isabelle Internet Bibliographie.

• http://foxnet.cs.cmu.edu/people/fp/homepage.html

Interessantes über HOL

• http://www.mathematik.th-darmstadt.de/ pfenning/lfs.html

Logical Frameworks

Historischer Überblick 1969-1974

• 1969: Scott entwickelt LCF (Logic of Computational Functions) LCF markiert einen neuen Meilensteil in der von der klassischen FOL dominierten Logik.

• 1974: Robin Milner entwickelt Edinburgh-LCF, einen programmierbaren proof-checker.

– LCF’s Metasprache ist ML. ML kann nicht nur Befehle ausführen ML repräsentiert Logik.

– Terme und Formeln sind wie Theoreme berechenbare Daten in ML.

– Jede Inferenzregel ist eine Funktion von Theoremen zu einem Theorem. Theoreme können in ML nur erzeugt werden, indem die Regeln auf bereits vorhandene Theoreme angewendet werden.

Historischer Überblick 1986

• 1986: Paulson entwickelt erste brauchbare Versionen von Isabelle. Zu diesem Zeitpunkt...

– sind Isabelles Inferenzregeln noch durch Horn-Klauseln repräsentiert, die für Beweise miteinander kombiniert werden können.

– ist Isabelle noch hauptsächlich dazu gedacht, LCF-style proofs auch in anderen Logiken zu benutzen, ohne dazu jedesmal für jede Inferenzregel eine neue Funktion schreiben zu müssen.

– ist Isabelle bereits ein “logical framework”, weil bereits eine Metalogik (die oben genannten Horn Klauseln) und die Objektlogik von einander getrennt sind.

Historischer Überblick 1987-1992

• 1987: HOL wird zu Isabelles Metasprache • 1988: beschränkter Polymorphismus und

natürliches Schließen

• 1989: Parser, pretty printer generator

• 1992: type classes, nun werden auch mehrfach geordnete und höherwertige Logiken (als Objektlogik) unterstützt Überblick - Was Isabelle heute ist:

• generisch theoretisch kann Isabelle mit jeder Logik als Objektlogik arbeiten

• interaktiv Beweise werden im Dialog mit dem Nutzer geführt

• halbautomatisch Beweisschritte (tactics) können zusammengefaßt werden (zu tacticals).

Objekt-Logiken, die dabei sind, sind

• FOL - First-Order Logic with Natural Deduction

• HOL - Higher-Order Logic

• CTT - Constructive Type Theory

• CCL - Classical Computational Logic (in FOL)

• ZF - Zermelo Fraenkel Set Theory (in FOL)

• LK - classical FO sequent calculus

• Modal - Modal Logic (Über LK)

• Barendregt’s Lambda-Cube Über Isabelles Implementationssprache: ML

• infix und mixfix Notation a fun b (infix)

if a then b else c (mixfix)

• polymorphe Typen

fun swap (a,b) = (b,a); ist vom Typ

α × β → β × α (α und β sind Typvariablen)

Ein: swap (1,''Test'');
Aus: val it = (``Test'',1) :  string * int

• symbol overloading Das Symbol “+” kann z.B. nach der Funktionsdefinition fun a + b = a^b; wie ein string concat eingesetzt werden: ``Test''+''program''

= ``Testprogram''

• function currying Currying:

• f(x, y) : α × β → γ

• f̄ : α → (β → γ)

• α → (β → γ) ≅ α × β → γ

• partial application: f̄(x_{α}) : β → γ • (f̄x_{α})y_{β→γ} = f(x, y)

Syntax der Meta-Axiome: Symbole • ⇒ Meta-Implikation

• ≡ Meta-Equivalenz

• ⋀ Meta-Allquantifikation

• [[…]] Prämisse

• [[ϕ_{1}, … ϕ_{n}]] ⇒ ϕ Regel

IPC Meta-Axiome - 1 (∧I) [[P; Q]] ⇒ P ∧ Q

(∧E1) P ∧ Q ⇒ P (∧E2) P ∧ Q ⇒ Q (∨I1) P ⇒ P ∨ Q (∨I2) Q ⇒ P ∨ Q

IPC Meta-Axiome - 2 (∨E) [[P ∨ Q; P ⇒ R; Q ⇒ R]] ⇒ R (→ I) (P ⇒ Q) ⇒ P → Q (→ E) [[P → Q; P]] ⇒ Q (⊥E) ⊥ ⇒ P Quantoren und Substitution: (∀I) (⋀ x.P (x)) ⇒ ∀.P (x) (∀E) (∀x.P (x)) ⇒ P (t) (∃I) P (t) ⇒ ∃x.P (x) (∃E) [[∃x.P (x); ⋀ x.P (x) ⇒ Q]] ⇒ Q

(subst) [[t = u; P (t)]] ⇒ P (u)

Higher Order Unification:

• Beispiel für Higher Order Logic: t(u) = Applikation eines Termes auf einen Term.

• Unification höherer Ordnung ist Unification von Funktionen

• Bsp.: P(x) = G(x)

Resolution: • standard form [[?P →?Q; ?P]] ⇒ Q • [[?P_{1} →?Q_{1}; ?P_{1}]] ⇒?Q_{1}

• [[P_{1} → (P → Q); P_{1}]] ⇒ (P → Q)

• [[P_{1} → (P → Q); P_{1}; P]] ⇒ Q

• Unifikation von ?Q_{1} und ?P →?Q

→ E \frac{[[?P_{1}→?Q_{1};?P_{1}]]⇒?Q_{1} [[?P →?Q;?P]]⇒?Q}{[[?P_{1}→(?P →?Q);?P_{1};?P]]⇒?Q}

• renaming: \frac{R→(P →Q) R P}{Q} Lifting over assumption:

• (?P ⇒?Q) ⇒?P →?Q

• (?P ⇒ (?P_{1} ⇒?Q_{1}))

⇒ (?P ⇒ (?P_{1} → Q_{1}))

• [[[[?P; ?P_{1}]] ⇒?Q_{1}; ?P_{1}]] ⇒?P_{1} →?Q_{1} • Unifikation von ?P ⇒?P_{1} →?Q_{1} mit

?P ⇒?Q ergibt:

• ([[?P; ?P_{1}]] ⇒?Q_{1}) ⇒?P → (?P_{1} →?Q_{1})