Konzeption
In der Übung unter Anleitung werden jede Woche anhand von Folien neue Konzepte von Isabelle/HOL vorgestellt, welche dann eigenständig angewandt werden. Dazu wird jede Woche ein Aufgabenblatt und ein Isabelle-Rahmen (eine thy-Datei) bereitgestellt, in welchem die zu bearbeitenden Probleme vorgestellt werden bzw. zu bearbeiten sind. Des weiteren werden weitere Handouts wichtige Konzepte und Hilfsmittel des Beweisens in Isabelle/HOL erläutern.
Voraussetzungen
Grundkenntnisse in funktionaler Programmierung aus Info I/II, Kenntnisse aus "Formale Systeme" sind von Vorteil.
Für die Übungen an den Rechnern im R -143 brauchen Sie einen gültigen
Studentenaccount der ATIS. Bitte prüfen Sie nach, ob ihr Account
funktioniert.
Inhalt
Themen
- Deduktion und prozedurales Beweisen
- Quantoren
- Simplifikation
- rekursive Datentypen und primitive Rekursion
- allgemeine Rekursion
- induktive Prädikate und Mengen
- wechselseitige Rekursion
- deklaratives Beweisen in Isar
Unterlagen
Die Dokumentation von Isabelle/HOL findet man hier.Vor allem "Tutorial on Isabelle/HOL", "Tutorial on Function definitions" und "Tutorial on Isar" könnten hilfreich sein.
Termine
vom 21.04.2009, bis 23.07.2009
| Tag | Beginn | Ende | Ort |
|---|---|---|---|
| Dienstag | 11:30h | 13:00h | R -143, 50.34 |
Veranstaltungen
| Datum | Thema | Unterlagen |
|---|---|---|
| 28.4. (11.30h) | Deduktion | Folien, Aufgabenblatt, Isabelle-Rahmen |
| 5.5. (11.30h) | Quantoren | Folien, Aufgabenblatt, Isabelle-Rahmen |
| 12.5. (11.30h) | Simplifikation | Folien, Aufgabenblatt, Isabelle-Rahmen, Handout |
| 19.5. (11.30h) | Primitive Rekursion | Folien, Aufgabenblatt, Isabelle-Rahmen, Handout |
| 26.5. (11.30h) | Induktive Prädikate | Folien, Aufgabenblatt, Isabelle-Rahmen |
| 2.6. (11.30h) | Kombination von Regeln | Folien, Aufgabenblatt, Isabelle-Rahmen |
| 9.6. (11.30h) | Allgemeine Rekursion | Folien, Aufgabenblatt, Isabelle-Rahmen |
| 16.6. (11.30h) | Wechselseitige Rekursion | Folien, Aufgabenblatt, Isabelle-Rahmen |
| 23.6. (11.30h) | Strukturierte Beweise mittels Isar (1) | Folien, Aufgabenblatt, Isabelle-Rahmen |
| 30.6. (11.30h) | Strukturierte Beweise mittels Isar (2) | Folien, Aufgabenblatt, Isabelle-Rahmen |
| 7.7. (11.30h) | Strukturierte Beweise mittels Isar (3) | Folien, Aufgabenblatt, Isabelle-Rahmen |
| 14.7. (11.30h) | Formalisierung von BigNat | Aufgabenblatt, Isabelle-Rahmen |
| 21.7. (11.30h) | Formalisierung einer Klammergrammatik | Aufgabenblatt, Isabelle-Rahmen |
Veranstalter
| Lehrstuhlinhaber |
|---|
| Prof. Gregor Snelting |
| Ehemalige Mitarbeiter |
|---|
| Dr.-Ing. Daniel Wasserrab |