Transfer und Entwicklung von Kalkülen für Modallogiken und Verwandte Systeme

Neben der klassischen, Booleschen Logik werden vor allem auch viele nichtklassische Logik erfolgreich in der Informatik, Philosophie, Epistemologie und in der künstlichen Intelligenz eingesetzt. Verschiedene nichtklassische Logiken erlauben unter anderem notwendige und kontingente Wahrheiten zu unterscheiden (alethische Modallogiken), hypothetisches Schließen zu formalisieren (Konditionallogiken), unterstützen systematisches Schließen über Wissen (epistemische Logiken), über Verpflichtungen und Verbote (deontische Logiken) oder auch über verschiedene Typen von Ressourcen (sogenannte bunched implication logics). Diese Vielzahl von Anwendungen führt zu einer explosionsartigen Vermehrung der Anzahl neuer Logiken. Unsere Untersuchungen setzen die Beweistheorie in den methodischen Brennpunkt um Varianten und Verallgemeinerungen der genannten Typen von Logiken uf der Basis formaler, analytischer Beweissysteme zu studieren. Solche analytischen Kalküle sind die Basis der Charakterisierung wichtiger logischer Eigenschaften, aber auch der Schlüssel zur Entwicklung automatisierter Beweisverfahren. Wir unterscheiden zwei Typen von Beweissytemen: Einerseits interne Kalküle (z.B. Gentzens Sequentialkalküle) in denen alle Basisobjekte des Schließens mit Formeln der jeweiligen Logik identifiziert werden können. Andererseits externe Kalküle deren Basisobjekte Formeln ausdrucksstärkerer Sprachen sind, die es erlauben die Semantik der betroffenen Logiken zu formalisieren. Interne und externe Kalküle weisen sehr unterschiedliche Charakteristka auf. Beispielsweise unterstützen interne Kalküle meist sehr direkt den Nachweis von Entscheidbarkeit und die Extraktion von Interpolanten. Externe Kalküle hingegen sind oft leichter zu konstruieren und in analytische Form zu bringen. TICAMORE setzt sich die Klärung der Beziehung zwischen den beiden genannten, systematisch und historisch unterschiedlichen Typen von Beweissystemen zum Ziel. Dies sollte zu einer gegenseitigen Befruchtung, wenn nicht sogar Vereinheitlichung der beiden bislang getrennten Forschungstraditionen in der Beweistheorie führen. Eine solche intergrieterte und systematische Studie von internen und externen Kalkülen ist seit etwa 30 Jahren überfällig.Unsere Untersuchungen setzen die Beweistheorie in den methodischen Brennpunkt um Varianten und Verallgemeinerungen der genannten Typen von aLogiken uf der Basis formaler analytischer Beweissysteme zu studieren. Solche analytischen Kalküle sind die Basis der Charakterisierung wichtiger logischer Eigenschaften, aber auch der Schlüssel zur Entwicklung automatisierter Beweisverfahren. Unser Forschungsvorhaben wird den Transfer beweistheoretischer Eigenschaften zwischen verschiedenen Kalkülen ermöglichen und zur Entwicklung neuer interner Kalküle für wichtige Logiken führen. Diese neuen Kalküle werden zur Lösung bedeutender theoretischer Fragen wie denjenigen nach Interpolation, Entscheidbarkeit oder Konservativität beitragen. Des weiteren wird das Projekt zur Entwicklung neuer Hilfsmittel für das automatische Schließen beitragen, mit Anwendungsgebieten in der Wissensrepräsentation und in der formalen Verifikation.

Logik bietet gewissensschaffende Präzision und ist daher grundlegend für Anwendungen in vielen Bereichen, von Philosophie bis zur künstlichen Intelligenz (KI). Beweistheorie ist ein zentrales Gebiet der Logik, das heutzutage Computern ermöglicht, automatisch Beweise zu erstellen. Klassische Logik befasst sich mit Objekten die entweder wahr oder falsch sein können. Sie ist nicht als Grundlage für alle möglichen Anwendungen geeignet, da verschiedene Anwendungen oft Logiken erfordert, die aussagekräftiger sind als die klassische Logik. Dieses Projekt konzentrierte sich auf die Beweistheorie nützlicher Familien von Logiken, die feinere Unterscheidungen und eine direkte Darstellung von Begriffen ermöglichen, die in der klassischen Logik nur unzureichend ausgedrückt werden können. Bei diesen Logiken handelt es sich um Varianten und Verallgemeinerungen von Modallogiken, die verwendet werden, um verschiedene Konzepte von Wahrheit auszudrücken und verschiedene Arten des Schlussfolgerns zu untersuchen, wie z. B. Schlussfolgern über Verpflichtungen und Verbote (zentral z. B. bei juristischem Schlussfolgern), über Wissen, über hypothetische und plausible Sachverhalte und über Computerprogramme. Neben der Formalisierung und Analyse von Schlussfolgerungen werden diese Logiken auch verwendet, um Systeme mit mathematischer Präzision zu beschreiben (z. B. KI-Agenten) und Eigenschaften über sie zu beweisen, um so ihr korrektes Verhalten sicherzustellen. Eine Voraussetzung für die Anwendung einer Logik auf konkrete Probleme zu deren Lösung, ist das Vorhandensein einer algorithmischen Darstellung der Logik, d.h. eines Beweissystems. Für Modallogiken und verwandte Logiken sind verschiedene Arten von Beweissystemen (Kalküle) vorgeschlagen worden, die sich in zwei Kategorien einteilen lassen: interne Kalküle, deren Basisobjekte als Formeln der Logik gelesen werden können, und externe Kalküle, deren Basisobjekte Formeln einer ausdrucksstärkeren Sprache sind, die die Semantik der Logik teilweise kodieren und daher schwieriger zu automatisieren sind. Interne und externe Kalküle weisen unterschiedliche Eigenschaften auf und haben ihre Stärken und Schwächen. Externe Kalküle sind zum Beispiel einfacher zu definieren, aber schwieriger handzuhaben. Interne und externe Kalküle wurden als zwei unabhängige, gelegentlich gegensätzliche Strömungen in der Beweistheorie mit unterschiedlichem Erfolg eingeführt. Für bestimmte Klassen von Modallogiken und verwandten Logiken sind jedoch überhaupt keine Kalküle bekannt. Im Rahmen des TICAMORE-Projekts haben wir eine ganzheitliche und systematische Studie interner und externer Kalküle für modale und verwandte Logiken durchgeführt. Wir haben die Beziehungen zwischen den beiden Arten von Kalkülen untersucht und Ergebnisse zwischen ihnen übertragen. Wir lieferten auch erste Kalküle für wichtige Klassen von Logiken und neue Werkzeuge, um wichtige offene mathematische Probleme der formalisierten Logiken anzugehen und zu lösen (Entscheidbarkeit, Komplexität, Interpolation...). Darüber hinaus haben wir Computerprogramme erstellt, die einige der Kalküle für die Klasse der betrachteten Logiken implementieren und so deren Einsatz in Anwendungsbereichen erleichtern.