Förderprojekte

Förderbeginn 01.07.2013

Algebraische Beweistheorie der Modallogik

Dr. Tadeusz Litak
Friedrich-Alexander-Universität Erlangen-Nürnberg
Lehrstuhl für Informatik 8 - Theoretische Informatik

Prof. Andrew Moshier
Chapman University
Center of Excellence in Computation, Algebra and Topology

Ziel der beabsichtigten Zusammenarbeit ist es, zu untersuchen, inwieweit Techniken der algebraischen Beweistheorie der Modallogik auf modale Formalismen angewendet werden können. Schnitt-Eliminationen für syntaktisch definierte Klassen des modalen Formalismus und bestehende Grenzen für Methoden im Stil von Gentzen stehen dabei besonders im Fokus. Ein geeigneter analytischer und schnitt-freier Sequenzenkalkül für eine vorgegebene Logik ist das Schlüsselwerkzeug, um algorithmische Beweisführung zu unterstützen. Die Existenz eines solchen Systems erlaubt es, Eigenschaften wie Entscheidbarkeit, Komplexität, Herbrandsatz und Interpolation abzuleiten und sogar Rechner- oder Programmierinhalte einer bestehenden Logik mit der Curry-Howard-Korrespondenz zu analysieren. Bis vor kurzem gab es jedoch nur wenige allgemeingültige mathematische Kriterien, um entscheiden zu können, ob eine gegebene Logik semantisch oder mit Hilbert-Axiomatisierung solch ein analytisches und normaliesierendes Gentzen-System besaß. Dies war der Ausgangspunkt der algebraischen Beweistheorie im vergangenen Jahrzehnt, auf deren Gebiet Prof. Jipsen sehr aktiv forschte. Insbesondere hat sich eine Übereinstimmung zwischen der Schnitt-Elimination und der algebraischen Vervollständigung gezeigt. Unter Anwendung der heutigen Algebra wollen wir den Bereich der generischen Schnitt-Eliminationstechniken erweitern und die Syntaxklassen der Axiome identifizieren für die diese Ergebnisse nicht zutreffen. Wir werden auch umfangreichere Formalismen untersuchen wie die algebraische Prädikatenlogik, die kürzlich von dem bayerischen Forscher zusammen mit Co-Autoren (ICALP 2012, TbiLLC 2011) vorgeschlagen wurde, und andere modale Systeme die für die Informatik relevant sind.