Universität Ulm, Fakultät für Informatik, Abtl. Künstliche Intelligenz up: weitere Lehrveranstaltungen

Maschinelles Beweisen

Unterlagen zur Vorlesung im WS'06/07

 Termin

 

Vorlesung:
Do. 14:15 - 15:45 Uhr in O 27 / 2203
Prof. Dr. F. W. von Henke, O 27 / 450
Sprechstunde: nach der Vorlesung oder n.V.

Übungen:
Do. 16 - 18 Uhr in O 27 / 2203
Dr. Holger Pfeifer, O 27 / 446
Sprechstunde: dienstags, 14.00 - 15.00 und n. V.

 Inhalt der Vorlesung

 

Die Vorlesung beschäftigt sich mit Methoden des logischen Schließens und ihrer Unterstützung in einem maschinellen Beweissystem. Im Zentrum der Vorlesung stehen Anwendungsbeispiele sowohl aus dem Software- als auch dem Hardware-Bereich, sowie deren Modellierung und Analyse im Spezifikations- und Verifikationssystem PVS.

Insbesondere werden folgende Themen behandelt:
  • Grundlegende Begriffe formaler deduktiver Systeme
  • Beweisen mit Gleichungen
  • Beweismethoden für Prädikatenlogik
  • Induktive Strukturen und Induktionsbeweise
  • Beweisen in Logik höherer Ordnung
  • Simplifikation, Entscheidungsprozeduren, BDDs

Über die Vorlesung und Übungen hinausgehend wird ein Praktikum angeboten. Die Vorlesung vermittelt die konzeptionellen Grundlagen, die im Praktikum anhand von konkreten, größeren Anwendungsbeispielen vertieft werden. Hörern der Vorlesung, die die erlernten Modellierungs- und Analysemethoden über die Übungen hinaus vertiefen und praktisch anwenden wollen, wird die Teilnahme am Praktikum empfohlen.

 Vorlesungsfolien

1. Einführendes     [PDF]
2. Beweisen mit Gleichungen: Gleichungslogik und Termersetzung        Teil 1 [PDF]   Teil 2 [PDF]
3. Grundlegende Begriffe von Logiken - Aussagenlogik        [PDF]
4. Prädikatenlogik        [PDF]   Teil 2 [PDF]
5. Lambda-Kalkül und Logik höherer Stufe     [PDF]
6. Induktion     rev. 14.12.06 [PDF], Ergänzungen [PDF]
7. Abstrakte Datentypen und Strukturelle Induktion     [PDF]
8. Einfache Fixpunkttheorie     [PDF]
9. Fallstudie Compiler-Verifikation     [PDF]
10. Entscheidungsprozeduren     [PDF]

 Übungsaufgaben

  Kurze Einführung in den Umgang mit PVS: Folienkopien [PDF]

Beispieldateien der PVS-Demo: proptest.pvs - proptest.prf sowie predtest.pvs - predtest.prf
 
  Anleitung zu PVS

Übungsaufgaben

 Materialien

 
PVS zum Download:
Ausführliche Anleitung und Installationshinweise finden sich auf der Seite zum PVS Mirror in Ulm.
Hinweis: Die angebotenen tar-Archive sind zwischen 1 MB und 13 MB groß.

Eine detailierte Dokumentation ist z. Zt. nur für die Vorgänger-Version verfügbar enthält aber alle wichtigen Informationen. Erhältlich als pvs-2.4-doc.tgz (komprimiertes tar-Archiv, 2.8 MB).

 Technisches

  Typ: Vorlesung im Hauptstudium (2V / 2Ü)
  Zuordnung:  Theoretische und mathematische Methoden der Informatik, Praktische und Angewandte Informatik (Kernfach)
Künstliche Intelligenz (Vertiefungsgebiet)

Abtl. KI Startseite Hilfe Mail an Webmaster HP - Stand: 08.02.07