Fixpunktlogiken: Ausdrucksstärke, Struktur, Komplexität

• Antragsteller: Professor Dr. Erich Grädel
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2011 bis 2018
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 199814663

Das zentrale offene Problem der Endlichen Modelltheorie ist die Frage nach einer Logik für Ptime: Gibt es eine Logik (im Sinn einer präzisen Definition von Gurevich) in welcher sich genau diejenigen Eigenschaften endlicher Strukturen definieren lassen, die in polynomialer Zeit entscheidbar sind? Dies ist äquivalent zu der Frage, ob es eine Anfragesprache für endliche relationale Datenbanken gibt, in denen sich genau die in polynomaler Zeit berechenbaren Anfragen programmieren lassen.Natürliche Kandidaten für solche Logiken sind Erweiterungen der Fixpunktlogiken LFP (least fixed-point logic) oder IFP (inflationary fixed-point logic). Eine klassische, aber nicht hinreichende, solche Erweiterung beruht auf Zählmechanismen. Der neue Ansatz, der hier verfolgt werden soll beruht auf Erweiterungen um Konstrukte der Linearen Algebra (Rang von definierbaren Matrizen, Ähnlichkeit von Matrizen, Lösbarkeit linearer Gleichungssysteme). Ziel ist das Verständnis der Ausdrucksstärke solcher Fixpunktlogiken, das Bereitstellen modelltheoretischer Methoden für diese Logiken, und die Klärung der Frage ob, wie weit, und auf welchen Strukturklassen man damit das Ziel einer Logik für Ptime erreichen kann.Zudem möchten wir dem Bereich modaler Fixpunktlogiken einen neuen Impuls geben durch Konstruktion von Logiken die über Zustandsformeln und monadische Fixpunkte hinausgehen. Wir werden diese und andere Ansätze auch benutzen, um den Zusammenhang von Fixpunktlogiken und unendlichen Spielen zu vertiefen, insbesondere im Zusammenhang der Definierbarkeit von Gewinnregionen und Gewinnstrategien.

• DFG-Verfahren: Sachbeihilfen