Links und Funktionen
Sprachumschaltung

Navigationspfad
Sie sind hier: Startseite / Lehre / WS 2010/11 / Rechnergestütztes Beweisen


Inhaltsbereich

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

 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 mit tutch.
Coq
Beweisassistent basierend auf Typentheorie.
Am CIP installiert. Eigene graphische IDE: Aufruf mit coqide. Plug-in für Emacs ProofGeneral: Aufruf mit proofgeneral.
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

Skript Konstruktive Logik der Vorlesung WS 2007/08
Skript Lambda-Kalkül
Skript Klassische Logik und PVS der Vorlesung WS 2003/04
Emacs short tutorial

Artikelaktionen


Funktionsleiste