| |
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
-
Beweismethoden für Prädikatenlogik
-
Induktive Strukturen und Induktionsbeweise
-
Beweisen in Logik höherer Ordnung
-
Simplifikation, Entscheidungsprozeduren, BDDs
Parallel zu Vorlesung und Übungen wird ein
Praktikum
angeboten. Die Vorlesung vermittelt die konzeptionellen Grundlagen,
die im Praktikum anhand von konkreten, großen 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.
|