Zielstellung

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.

In der Veranstaltung werden die wichtigsten Konzepte des automatischen Schliessens vorgestellt und demonstriert. Im einzelnen sind die folgenden Themen vorgesehen:

Gliederung

• • 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

Lehrveranstaltungen

• Die in der Vorlesung verwendeten Folien werden auf den Servern des Lehrgebiets (wenn möglich im Voraus) bereitgestellt.
• Die Übungen dienen der Vertiefung und Anwendendung der in der Vorlesung vorgestellten Themen.