Nichtklassische Beweise: Theorie, Automatisierung, Anwendung

Logiken treten in vielen Erscheinungsformen auf. Einige dieser Erscheinungsformen sind semantischer, andere syntaktischer Natur. Die verschiedenen Erscheinungsformen betonen unterschiedliche Eigenschaften und erlauben es unerwartete Verbindungen zwischen Logiken wahrzunehmen. Das ermöglicht zugleich weiterführende mathematische Analysen und die Entwicklungen von Anwendungen. Das allgemeine Problem der zufriedenstellenden Charakterisierung der Beziehung verschiedener syntaktischer und semantischer Repräsentationen der gleichen Logik ist jedoch ungelöst. Vorhandene Lösungen sind von Logik zu Logik verschieden und es ist nicht offensichtlich, inwieweit sich Erkenntnisse für eine bestimmte Logik (oder eine bestimmte Klasse von Logiken) auf verwandte Logiken (oder verwandte Klassen von Logiken) übertragen lassen. Ziel des vorliegenden Projektes ist es für allgemeine Logiken effektive Transformationen von semantischen Repräsentationen (ausgedrückt durch Hilbert-Typ Axiomatisierungen) in syntaktische Repräsentationen (ausgedrückt durch analytische Kalküle) zu entwickeln. Die Liste wichtiger Logiken ist lang - sie umfasst die Familien der modalen, intermediären, fuzzy, und substrukturellen Logiken - und ständig wachsend, da neue Anwendungen in Mathematik und Informatik die Entwicklung neuer Logiken zur Folge haben. (Ein bemerkenswertes Beispiel ist das zunehmende Interesse an Zeitlogiken mit Bezug auf die automatische Verifikation von Computerprogrammen.) Hilbert-artige Repräsentationen bestehen aus endlich vielen Axiomen und Regeln und stellen meist den intuitivsten Zugang zur Beschreibung von Logiken dar. Die Axiome spiegeln die Eigenschaften der zugehörigen algebraischen Strukturen wieder weshalb Hilbert-artige Repräsentationen algebraischen Spezifikationen nahekommen. Hilbert artige Repräsentationen sind jedoch nur bedingt geeignet für das tatsächliche Schließen in den jeweiligen Logiken. Das gilt a forteriori für die Automatisierung des Schließens, das heißt für die Entwicklung von geeigneten Algorithmen des automatischen Beweisens. Deshalb ist es notwendig analytische Repräsentationen zu finden. (Der Begriff "analytisch" geht auf Leibnitz zurück und bezeichnet die Tatsache, dass im Beweis nur Begriffe auftreten die in dem bewiesenen Satz vorkommen. Daher erlaubt eine analytische Repräsentation nach einem Beweis zu suchen, da die möglichen Bestandteile bekannt sind. Die Suche nach Beweisen erfolgt dann durch eine schrittweise Zerlegung der zu beweisenden Aussagen.) Der Sequenzkalkül von Gentzen ist seit seiner Einführung 1934 der Archetypus analytischer Kalküle. Allerdings genügt dieser Formalismus im wörtlichen Sinn nur der klassischen und intuitionistischen Logik. Deshalb wurden in letzter Zeit zahlreiche Varianten und Erweiterungen des Formalismus entwickelt mit der Absicht, immer mehr Logiken analytisch zu repräsentieren.Mit Ausnahme weniger spezifischer Klassen (z.B. endlichwertige Logiken) ist die Entwicklung analytischer Kalküle bislang auf auf den Einzelfall zugeschnitten. Die Forschungsergebnisse des vorliegenden Projektes sollen die genannte Konstruktion mathematisch systematisieren und damit eine Automatisierung der Entwicklung und Analyse analytischer Kalküle für nicht klassische Logiken ermöglichen.

Logik ist die Wissenschaft des korrekten Schliessens. Mit ihrer Hilfe lässt sich die Richtigkeit verschiedener Argumentationsweisen überprüfen, wie beispielsweise von mathematischen Beweisen, medizinischen Diagnosen, oder gerichtlichen Entscheidungen. Logik ist zudem grundlegend für das Verhalten von "intelligenten" und autonomen Maschinen. Die bekannteste Logik, Klassische Logik, beschäftigt sich mit Aussagen, welche entweder wahr oder falsch sind. Diese sind angemessen beispielsweise fuer die Formalisierung mathematischer Aussagen oder bei der Modellierung von Schaltkreisen mit "Ein/Aus" Zuständen. Allerdings erfordern einige Anwendungsfälle darüber hinausgehende Logiken, wie bei medizinischen Diagnosen mittels verschiedener Schmerzgrade, oder normativen Schlüssen, für welche neben Wahrheit oder Falschheit einer Aussage auch relevant ist was zu tun geboten ist. Grundsätzlich erfordern unterschiedliche Arten des Schliessens damit unterschiedliche, und insbesondere oft nichtklassische, Logiken. Die hierbei angewandte mathematische und formale Betrachtungsweise erlaubt nun eindeutig zu beweisen, ob eine Schlussfolgerung oder ein Computerprogramm korrekt sind. Um dies effizient zu bewerkstelligen sind mathematische und computerbasierte Werkzeuge vonnöten. Im Rahmen des START Projektes "Non classical Proofs: Theory, Applications and Tools" entwickelten wir derartige Werkzeuge für große Klassen nichtklassischer Logiken. Aufgrund der hohen und ständig wachsenden Anzahl solcher Logiken lag der Schwerpunkt nicht auf einzelnen Logiken, sondern auf der Entwicklung von generellen und einheitlichen Methoden und Resultaten, welche auf grosse Klassen von Logiken anwendbar sind. Wir entwickelten algorithmische Darstellungen für verschiedene Familien von relevanten Logiken in Form von analytischen Kalkülen, also formalen Systemen, in deren Herleitungen nur solche Formeln vorkommen, welche schon in der herzuleitenden Formel enthalten sind. Diese Kalküle sind der Schlüssel zur Entwicklung automatischer Beweismethoden. Insbesondere nutzten wir die entwickelten Kalküle, um anwendungsrelevante theoretische Ergebnisse über die betrachteten Logiken zu erzielen, wie beispielsweise Entscheidbarkeit, Komplexität, Interpolation oder algebraische Vervollständigungen, sowie zur Entwicklung neuer nebenläufiger Programmiersprachen. Die Instantiierung unserer allgemeinen Ergebnisse in konkreten Fällen lieferte darüberhinaus Lösungen für seit Langem offene Probleme für bestimmte Logiken, Kalküle und Algebren. Desweiteren implementierten wir computerbasierte Hilfsmittel für die Erforschung und Anwendung nichtklassischer Logiken.