| Universität Ulm, Fakultät für Informatik, Abtl. Künstliche Intelligenz | up: weitere Lehrveranstaltungen |
| Termin |
|
|
| 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:
Die Übungen zur Vorlesung finden in Form eines Praktikums (mit Praktikumsschein) statt. Die Vorlesung vermittelt die konzeptionellen Grundlagen, die dann im Praktikum anhand von konkreten Anwendungsbeispielen vertieft werden. Hörern der Vorlesung wird zur Vertiefung und praktischen Anwendung der erlernten Modellierungs- und Analysemethoden die Teilnahme am Praktikum empfohlen. |
| Vorlesungsfolien |
|
| Übungs- und Praktikumaufgaben |
|
Anleitung zu PVS
Übungsaufgaben
Lösungsvorschläge Die Lösungsvorschläge werden als PVS-Dump-Dateien bereitgestellt. Diese müssen innerhalb von PVS mit dem Kommando M-x undump-pvs-files ausgepackt werden.
|
| Materialien |
|
| Technisches |
| Typ: | Vorlesung im Hauptstudium (2V) | |
| Zuordnung: | Theoretische und mathematische Methoden der Informatik,
Praktische und Angewandte Informatik (Kernfach)
Künstliche Intelligenz (Vertiefungsgebiet) |
| Abtl. KI Startseite | Hilfe | Mail an Webmaster | H. Pfeifer - geändert: 08.12.04 |