Projekt

Für die in der Deskriptiven Komplexitätstheorie (oder Endlichen Modelltheorie) verwendeten Logiken (wie DTC, TC, Fixpunktlogiken, Logiken zweiter Stufe, Logiken mit verallgemeinerten Quantoren, etc.) gibt es keine finitären Kalküle, die die allgemeingültigen Sätze generieren; schon für FOL gibt es keinen finitären Kalkül, der alle Sätze liefert, die in allen endlichen Modellen wahr sind.
Dennoch existieren meistens Kalküle mit infinitären Regeln, die genau die (im Endlichen) allgemeingültigen Sätze der betreffenden Logik herleiten. Hierbei genügen bereits Anwendungen der infinitären Regeln, die eine sehr geringe komputationelle (und deskriptive!) Komplexität besitzen.
Ziele des Projekts:
(a) Entwicklung spezifisch beweistheoretischer Methoden zur Bestimmung der Ausdrucksstärke der betreffenden Logiken
(b) Komplementierung des (semantischen) Model-Checking durch formale (eventuell infinitäre!) Herleitbarkeit.

(Weiteres siehe Webseite)