Rechnergestütztes Beweisen
Vorlesung, 3-std., Mo 14-17; Übungen 2-std., Mi 16-18; Abel, Jost, Schöpp
Aktuelles
- Übungen finden im Rechnerraum Takla-Makan statt.
Inhalt
In der Vorlesung werden Spezifikationsformalismen, Konzepte der Systemmodellierung, Grundtechniken für die Automatisierung der Verifikation, Typsysteme und statische Analyse eingeführt.
Unter rechnergestütztem Beweisen versteht man das Führen mathematischer Beweise am Computer, dessen Aufgabe es hier ist, Beweisschritte zu überprüfen, Buchhaltungsaufgaben zu übernehmen und Routineschritte zu automatisieren. Dies verhält sich zum gewohnten manuellen Führen eines Beweises in etwa wie die konkrete Implementierung eines Algorithmus zu dessen informeller Beschreibung. Rechnergestütztes Beweisen hat zahlreiche Anwendungen in der Programm- und Hardwareverifikation, sowie der Prototypentwicklung; in geringerem Maße auch in der Formalisierung "echter" mathematischer Beweise.
Organisation
- Umfang: 3+2 Semesterwochenstunden
- Voraussetzung: Grundstudiumsvorlesungen der Informatik
- Vorlesung und Übungen: Dr. Andreas Abel, Steffen Jost, Dr. Ulrich Schöpp
Die Vorlesung wird anerkannt:
- für Studierende im Studiengang Informatik Master für das Modul Logik und Spezifikation
- für Studierende in den Studiengängen Informatik und Medieninformatik Bachelor für das Modul Vertiefende Themen der (Medien-) Informatik
- für Studierende in den Studiengängen Informatik Diplom (Prüfungs-Schiene T) und Mathematik Diplom
Zeit und Ort
| Veranstaltung | Zeit | Ort | Beginn |
|---|---|---|---|
| Vorlesung | Mo, 14.00-16.30 Uhr | Hörsaal B046 (Theresienstr. 39) | 18.10.2010 |
| Übung | Mi, 16.15-17.45 Uhr | Takla-Makan, CIP (Oettingenstr. 41) | 27.10.2010 |
Vorlesung und Übung
| Datum | Stoff | Material |
|---|---|---|
| 18.10. | Von Aristoteles zur modernen Logik; Konstruktivismus; Natürliches Schliessen | Folien |
| 25.10. | Beweisreduktion und Expansion; Lokale Korrektheit und Vollständigkeit; Verifikationen (normale Beweise) | Skript Pfenning Tutch demo |
| 27.10.Ü | Aussagenlogische Beweise in Tutch | Übungsblatt 1 Lösung |
| 03.11.Ü | Aussagenlogische Beweise in Coq | Coq Intro Übungsblatt 2 Lösung |
| 08.11. | BHK-Interpretation; Beweisterme; Curry-Howard-Isomorphismus; Termreduktion | |
| 10.11.Ü | Beweisterme in Tutch | Tutch-Beweisterme Übungsblatt 3 Lösung |
| 15.11. | Herleitbare und zulässige Regeln; Normalisierung | |
| 17.11.Ü | Beweisterme in Coq | Coq-Beweisterme Übungsblatt 4 Lösung |
| 22.11. | Prädikatenlogik erster Stufe (FOL) | |
| 24.11.Ü | FOL in Tutch | FOL-Beweise in Tutch Übungsblatt 5 Lösung |
| 29.11. | Kripke-Modelle; Korrektheit und Vollständigkeit des natürlichen Schließens für Aussagenlogik | |
| 01.12.Ü | FOL in Coq | Taktiken und Beweisterme für FOL in Coq Übungsblatt 6 |
| 06.12. | Kripke-Modelle für Prädikatenlogik erster Stufe; Arithmetik | |
| 08.12.Ü | Arithmetik in Tutch | Beispiele für Arithmetik in Tutch Übungsblatt 7 Template |
| 13.12. | Listen, Vektoren, abhängige Typen | |
| 15.12.Ü | Datentypen, Rekursion, Induktion in Coq | Übungsblatt 8 |
| 20.12. | Agda | Agda.agda |
| 22.12.Ü | Agda: Matrices and Sublists | Exercise 2.1 und 2.3 aus Agda Tutorial (Seite 19f) |
| 10.01. | Klassische Aussagenlogik: Sequenzenkalkül und Resolution | |
| 12.01.Ü | Sequenzenkalkül und Resolution; Seq.K. in Agda | Übungsblatt 10 Agda Übung |
| 17.01. | Korrektheit der Resolution; SAT-Solver DPLL; Prädikatenlogik | |
| 19.01.Ü | PVS | Übungsblatt 11 PVS Beispiele Lösung.pvs Lösung.prf |
| 24.01. | Korrektheit und Vollständigkeit des Sequenzenkalküls für Prädikatenlogik; Resolution | |
| 26.01.Ü | Prädikatenlogik in PVS; Resolution; Unifikation | Übungsblatt 12 Aufgabe 1 |
| 31.01. | Pränexform und Skolemisierung; Gleichheit und Gleichungstheorien | |
| 02.02.Ü | Gleichheit und Induktion in PVS und Coq | Übungsblatt 13 (PVS) Übungsblatt 13 (Coq) Teil-Lösung.pvs Teil-Lösung.prf Lösung.v |
| 07.02. | Konvexität und Entscheidung von Gleichungstheorien; Normalisierung durch Auswertung | Coq Demo: Binärbäume |
| 09.02.Ü | Klausur |
Software
- Tutch
- Einstiegstool für Beweise im natürlichen Schliessen.
Am CIP installiert, Aufruf mittutch. - Coq
- Beweisassistent basierend auf Typentheorie.
Am CIP installiert. Eigene graphische IDE: Aufruf mitcoqide. Plug-in für Emacs ProofGeneral: Aufruf mitproofgeneral. - Agda
- Abhängig getypte Programmier- und Beweissprache
Am CIP installiert. Emacs Agda-modus wird aktiviert beim Öffnen einer.agda-Datei. Wichtigste Befehle:Ctrl-c Ctrl-l- Laden der editierten Datei in den Agda-interpreter.
Ctrl-c Ctrl-,- Betrachten des Typs des aktuellen Lochs.
Ctrl-c Ctrl-Space- Den in das Loch eingetragenen Code senden.
Ctrl-c Ctrl-c- An der in das Loch eingetragenen Variablen Fälle (cases) unterscheiden.
Ctrl-c Ctrl-a- Loch automatisch füllen.
- PVS
- Beweissystem für klassische Logik basierend auf dem Sequenzenkalkül
Am CIP installiert. Plug-in für Emacs: Aufruf mit/soft/IFI/sci/PVS-4.2-allegro/iX86-unknown-linux/pvs.
Literatur
