| Lerninhalte |
Beschreibung
Theorembeweisersysteme sind Computerprogramme die eine Menge von Annahmen und eine Vermutung als Eingabe erhalten, und versuchen zu entscheiden bzw. zu überprüfen, ob die eingegebene Vermutung eine logische Konsequenz der Annahmen ist. Im Fall von automatischen Theorembeweisern passiert dieser Vorgang vollständig automatisch, d.h. ohne Hilfe von menschlicher Interaktion.
Mit solchen Systemen wurden zuvor offene mathematische Fragestellungen beantwortet (u.a., Vier-Farben-Satz, Keplersche Vermutung), Software- und Hardwaresysteme formal verifiziert, oder auch Themen der theoretischen Philosophie bearbeitet. In dieser Veranstaltung werden theoretische Grundlagen zur Logik, zur Vorgehensweise von automatischer Beweissuche, und praktische Grundlagen zur Verwendung dieser Systeme thematisiert.
Qualifikationsziele
Nach erfolgreicher Absolvierung der Veranstaltung sind die Studierenden in der Lage ...
- die zentrale Rolle von Logikformalismen in wissensbasierten Systemen zu verstehen und zu erklären,
- den Unterschied zwischen syntaktischen und semantischen Konzepten logischer Systeme zu erklären,
- zentrale modelltheoretische Begriffe logischer Systeme sicher zu handhaben und einordnen zu können (u.a.: Interpretationen, Gültigkeit, Erfüllbarkeit, ...),
- mit zentralen beweistheoretischen Begriffen logischer Systeme sicher umzugehen und diese einzuordnen (u. a.: Beweiskalküle, Korrektheit, Vollständigkeit, ...),
- klassische Aussagenlogik und Prädikatenlogik erster Ordnung zu definieren; und vorgegebene Ausdrücke bezüglich fester Interpretationsstrukturen auszuwerten,
- grundlegende metalogische Erkenntnisse über die beiden genannten Logiken und ihre Konsequenzen erläutern,
- die eingeführten logischen Systeme zur Darstellung von Sachverhalten und Eigenschaften (z.B. natürlichsprachliche Aussagen) zu verwenden,
- die allgemeine Funktionsweise von Theorembeweisern und ausgewählten verwandten Ansätzen zu verstehen und erklären zu können, und
- bestehende Theorembeweiser zur Modellierung und Auswertung von Logikproblemen praktisch zu nutzen.
Themen umfassen:
- Propositionallogik, Syntax and Semantik, Erfüllbarkeitsproblem, Normalformen, Brute-force, DPLL,
- Prädikatenlogik erster Stufe, Syntax und Semantik, Normalformen, Skolemisierung, Resolution, Tableaux,
- Wissensrepräsentation und Anwendungen,
- Praxis: Standards, Beweiser, Beweisformate,
- Ausblick: Prädikatenlogik höherer Stufe, Nichtklassische Logiken
|
