Rechnergestütztes Beweisen (PG)
Hauptstudium, PG
WS 2005/06
Vorlesung: Mi, 12-14, Do, 14-16, Prof. Martin Hofmann
Übung: Do, 10-12, Andreas Abel
Schein: ja
SWS: 4 Vorlesung + 2 Übung
Aktuelles
- Hier die Dateien zur Pipeline Architektur und das zugehoerige Tutorial .
- Hier die Modellierung des Addierwerks.
- Das Skript wurde erweitert auf den Stoff der VL 18 und enthält noch eine Bemerkung zur elim-Taktik in Coq.
- Ein Skript zum natürlichen Schliessen (in Coq) ist verfügbar.
- Coq ist am Cip-Pool installiert, siehe Rubrik Software
- Das Vorlesungs-Skript wurde erweitert (29.1.06 21:59).
- Die Arbeit von Georges Gonthier zu seiner Formalisierung des Vierfarbensatzes wurde in der Vorlesung vorgestellt.
- Die Arbeit von Oostdijk und Caprotti zu ihrer Zertifizierung von Primzahlen in Coq wurde in der Vorlesung vorgestellt.
Hier ist das dazugehoerige Applet, leider fuer eine unklare Coq-Version.
- Emacs Einführung.
Organisatorisches
|
| Tag
| Zeit
| Ort
| Beginn
| Dozent
|
|---|
| Vorlesung
| Mi
| 12.15 - 14.00
| 1.39 (Oettingenstr. 67)
| 19.10.05
| Prof. Martin Hofmann
|
|---|
|
| Do
| 14.15 - 16.00
| 1.43 (Oettingenstr. 67)
|
|
|
|---|
| Übung
| Do
| 10.15 - 12.00
| Rechnerraum Z11
| 20.10.05
| Andreas Abel
|
|---|
| Für
| Studierende der Informatik im Hauptstudium
Studierende der Mathematik im Hauptstudium
|
|---|
| Prüfungsbereich
| PG
|
|---|
| Vorkenntnisse
| Grundkenntnisse in Informatik |
|
|---|
| Schein
| gilt für Diplomprüfung im Haupt- oder Nebenfach Informatik |
|
|---|
| Scheinerwerb
| Klausur am Ende des Semesters mit Zulassungsvoraussetzung: 50% Übungspunkte
|
|---|
|
|
|
|
|---|
Einführung
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.
Inhalt
Theoretischer Teil
- Sequenzenkalkül
- Resolution
- Typtheorie
- model checking
- Entscheidungsprozeduren
Praktischer Teil
- Prototype Verification System PVS
- Beweissystem Coq
- Beweissystem Isabelle
- Automatischer Beweiser SPASS
Literatur
|
Andreas Abel
Last modified: Wed Feb 8 16:13:05 CET 2006
|
|
|