Logisches Schließen steht im Zentrum allen intelligenten Handelns. Die
Fähigkeit, logische Schlüsse zu ziehen, ist die Voraussetzung für das
Lösen von Problemen, für das Planen von Aktionen, für kognitives
Verständnis und damit im Endeffekt für jede Form des wissenschaftlichen
Fortschritts. Inferenzmethoden, die
automatische Verarbeitung von Wissen mittels logischer Schlüsse, sind
daher eine der Schlüsseltechniken der Künstlichen Intelligenz. Speziell
spielen sie bei Expertensystemen, intelligenten Agenten, logischen
Programmiersprachen, der Verifikation und Synthese von Programmen, und
in vielen weiteren Anwendungen eine fundamentale Rolle. Im Modul werden
die wichtigsten Konzepte des automatischen Schließens vorgestellt und
demonstriert.
Themenschwerpunkte sind
- Prädikatenlogik und formale Kalküle (Sequenzen und Tableauxverfahren)
- Die Konnektionsmethode und ihre Beziehung zu Resolution und deren Verfeinerungen
- Unifikation; Optimierungstechniken; Spezielle Verfahren für Aussagenlogik
- Einbau von Theorien, insbesondere Gleichheit, Induktion und Termersetzung
- Behandlung von Modallogik; konstruktive Logik, lineare Logik; Logik höherer Stufe
- Kursleiter*in: Prof. Dr. Christoph Kreitz