Automatisierung der Deduktion

Vor dem Hintergrund der menschlichen Fähigkeit zur Erweiterung unseres Wissens durch logisches Schließen vermittelt dieser Beitrag einen Überblick der Automatischen Deduktion (AD), eines Teilgebiets der Disziplin der Künstlichen Intelligenz (KI). Er erläutert die Grundmerkmale sowohl der Resolutionsmethode als auch der Konnektionsmethode in der AD und umschreibt deren Varianten und Spezialisierungen sowie die aus der AD hervorgegangenen Beweissysteme, deren Leistungsfähigkeit und vielfältige Anwendungen. Der Text vermittelt zudem einen Einblick in die historische Entwicklung der AD sowie eine Vorstellung von ihrer Rolle, auch im Kontext von Lernverfahren, in der künftigen Entwicklung der KI.