Beweistheorie in der Deskriptiven Komplexitätstheorie

Internally funded project


Project Details

Project leader:
Dr. Wolfgang Degen


Contributing FAU Organisations:
Lehrstuhl für Informatik 10 (Systemsimulation)

Start date: 01/01/2000
End date: 31/05/2012


Abstract (technical / expert description):

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.


Publications

Degen, W., & Werner, J. (2007). Towards Intuitionistic Dynamic Logic. In Proceedings of Studia Logica 2006 (pp. 305-324). Torùn, Polen, PL: Torun: Nicolaus Copernicus University Press.

Last updated on 2019-18-03 at 13:37