Grundlagen der Künstlichen Intelligenz III
Logik und Erfüllbarkeit
Dieser Kurs ist Teil der Kursreihe „Grundlagen der Künstlichen Intelligenz I–VI“, die eine Vielzahl von Algorithmen und Methoden behandelt, die in der KI von zentraler Bedeutung und von großer praktischer Relevanz sind.
Überblick
Der Kurs "Grundlagen der Künstlichen Intelligenz III" führt in die Grundlagen der mathematischen Logik und der Erfüllbarkeitsprüfung ein. Der Kurs behandelt die Sprachen der Aussagen- und Prädikatenlogik. Er führt in deren Syntax und Semantik ein, definiert verschiedene Normalformen, die von KI-Algorithmen für logisches Schließen verwendet werden, und stellt das Resolutionsverfahren sowie den Davis-Putman Logemann-Loveland (DPLL)-Algorithmus vor.
Wir besprechen insbesondere, wie die Erfüllbarkeit von logischen Formeln automatisch überprüft werden kann, und führen in die Grundlagen moderner Satisfiability (SAT)-Solver ein, die eine immer größere Bedeutung beim Lösen von umfangreichen Such-, Optimierungs- und Verifizierungsproblemen mit KI-Methoden erlangen.
Die umfassende theoretische Behandlung der logischen Sprachen und Algorithmen wird durch zahlreiche Beispiele ergänzt.
Der Kurs liefert außerdem die theoretischen Grundlagen für die Kurse zu Wissensrepräsentation und Constraint-Optimierung in dieser Kursreihe.
Der Kurs basiert auf dem Lehrbuch von Stuart Russell und Peter Norvig: Introduction to Artificial Intelligence – A Modern Approach, 3. Auflage, 2012, oder 4. Auflage 2020. Die 3. Auflage ist auch auf Deutsch erhältlich: Stuart Russell und Peter Norvig: Künstliche Intelligenz – Ein moderner Ansatz, 3. aktualisierte Auflage, Pearson 2012.
Zudem wird Material aus dem Buch von Uwe Schönig: Logik für Informatiker, Modern Birkhäuser Classics, 1989 verwendet.
Welche Themen werden behandelt?
Modul Aussagenlogik
- Einführung in die Aussagenlogik
- Syntax
- Semantik
- Konjunktive und disjunktive Normalformen
- Interpretation und Modell einer Formel
- Schlussfolgern in der Aussagenlogik
- Resolution
- Erfüllbarkeitsprüfung
- Davis-Putnam-Logemann-Loveland-Algorithmus
Modul Prädikatenlogik erster Stufe
- Einführung in die Prädikatenlogik erster Stufe
- Syntax
- Semantik
- Erfüllbarkeit
- Normalformen
- Pränex-Normalform
- Skolem-Normalform
- Klauselnormalform
- Herbrandsche Theorie
- Herbrand-Universum und Herbrand-Struktur
- Herbrand-Expansion
- Gödel-Herbrand-Skolem und Herbrand-Theorem
- Grundlegende Substitution
Was werde ich erreichen?
Am Ende des Kurses werden Sie in der Lage sein,
- die logischen Grundlagen der logikbasierten Methoden, die in der KI verwendet und entwickelt werden, zu verstehen,
- die praktische Bedeutung der Erfüllbarkeitsprüfung zu verstehen,
- ein einfaches Problem in Aussagenlogik oder Prädikatenlogik erster Stufe zu formalisieren,
- Normalformen für Formeln der Aussagenlogik und Prädikatenlogik erster Stufe zu berechnen,
- zu verstehen, wie Resolution und der Davis-Putnam-Logemann-Loveland-Algorithmus funktionieren und diese Algorithmen auf kleine Beispiele anzuwenden
Welche Voraussetzungen muss ich erfüllen?
Keine.
