Rechnergestütztes Beweisen

Hauptstudium Informatik und Mathematik
WS 2007/08
Vorlesung: Prof. Martin Hofmann, Dr. Andreas Abel, Di 10-12 Uhr, Oe .15, Mi 14-16 Uhr, Oe 1.15
Übung: Dr. Andreas Abel, Mo 10-12 Uhr, CIP-Raum Z 11
Schein: ja
SWS: 4 Vorlesung + 2 Übung

Aktuelles

Klausur am Dienstag, 5. Februar 2008, 10.00 Uhr im Rechnerraum Z11 (Takla-Makan).

Für	Studierende der Informatik im Hauptstudium Studierende der Mathematik im Hauptstudium
Prüfungsbereich	PG, T
Vorkenntnisse	Grundkenntnisse in Informatik
Schein	gilt für Diplomprüfung im Haupt- oder Nebenfach Informatik
Scheinerwerb	Klausur am Ende des Semesters

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

Michael Huth and Mark Ryan: Logic in Computer Science, Cambridge University Press
Literatur zu PVS: siehe PVS Homepage
Skript (engl.) der Vorlesung vom WS 05/06
Einführung in die konstruktive Logik
A Tutorial on Recursive Types in Coq

Andreas Abel

Last modified: Tue Dec 11 10:11:18 CET 2007