Universität Ulm, Fakultät für Ingenieurwissenschaften und Informatik, Institut für Künstliche Intelligenz up: weitere Lehrveranstaltungen

Maschinelles Beweisen

Unterlagen zur Vorlesung im WS'07/08


 Termin

 

Vorlesung und Übungen:
dienstags 14:15 - 15:45 Uhr in O 27 / 2203
donnerstags, 14:15 - 15:45 Uhr in O 27 / 441
Dr. Holger Pfeifer, O 27 / 446
Sprechstunde: mittwochs, 14.00 - 15.00, sowie nach Voranmeldung

 Inhalt der Vorlesung

 

Für viele Anwendungen in der Informatik, speziell der Künstlichen Intelligenz, spielt die Fähigkeit, neues Wissen aus gegebenen Fakten abzuleiten, eine zentrale Rolle. In dieser Vorlesung beschäftigen wir uns mit den logischen Grundlagen des Schlussfolgerns und seiner Unterstützung in einem maschinellen Beweissystem.

Insbesondere werden folgende Themen behandelt:

  • Grundlegende Begriffe formaler deduktiver Systeme
  • Beweisen mit Gleichungen
  • Beweismethoden für Prädikatenlogik
  • Beweisen in Logik höherer Ordnung
  • Induktive Strukturen und Induktionsbeweise
  • Simplifikation, Entscheidungsprozeduren
  • Anwendungen des maschinellen Beweisens, insbesondere im Bereich der Verifikation von Software und Hardware
Die in der Vorlesung behandelten Methoden werden im Rahmen der Übungen mit dem Spezifikations- und Verifikationssystem PVS an praktischen Beispielen eingeübt und vertieft.

 Materialien

 

Das in den Übungen verwendete Beweisersystem PVS ist frei verfügbar und kann von der PVS Homepage (Computer Science Lab, SRI International, Menlo Park, California) bezogen werden.

 Technisches

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


KI Startseite HP - Stand: 18.10.07