Beweistheorie in der Deskriptiven Komplexitätstheorie

Internally funded project


Start date : 01.01.2000

End date : 31.05.2012


Project details

Scientific Abstract

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.

Involved:

Contributing FAU Organisations: