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


Valid HTML 4.01!
Andreas Abel
Last modified: Tue Dec 11 10:11:18 CET 2007
Valid CSS!