Algebraische Methoden in der Endlichen Modelltheorie

• Antragsteller: Dr. Wied Pakusa
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2016 bis 2018
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 324066354

In diesem Projekt möchten wir Anwendungen von algebraischen Techniken in der Endlichen Modelltheorie untersuchen.Das Ziel ist die Entwicklung neuer Methoden um die Ausdrucksstärke von logischen Systemen über endlichen Strukturen zu analysieren.Die Motivation für unser Vorhaben ist die wichtigste offene Frage aus dem Gebiet der deskriptiven Komplexitätstheorie: Gibt es eine Logik die genau die Eigenschaften endlicher Strukturen definieren kann, die durch Polynomialzeitalgorithmen entschieden werden können?Die große Relevanz dieser Frage kommt daher, dass einerseits eine logische Charakterisierung von Polynomialzeit uns komplett neue Einblicke in die Natur effizient entscheidbarer Struktureigenschaften ermöglichen könnte, und dass andererseits ein Beweis, dass keine Logik für Polynomialzeit existiert, P von NP trennen würde.In den vergangenen Jahren hat die Betrachtung algebraischer Ideen zu neuen Ansätzen geführt und die Suche nach einer Logik für Polynomialzeit weiter vorangetrieben.Zunächst einmal hat sich gezeigt, dass viele fundamentale algorithmische Techniken aus dem Gebiet der Algebra und Gruppentheorie, wie etwa das Gauß'sche Eliminationsverfahren, nicht in den Logiken ausdrückbar sind, die bisher als Kandidaten untersucht wurden. Darüber hinaus stellte sich heraus, dass alle "schwierigen" Benchmark-Eigenschaften als Spezialfälle von solchen algebraischen Problemen aufgefasst werden können, wie z.B. dem Lösen von linearen Gleichungssystemen über endlichen Körpern.In diesem Sinne geben uns solche algebraischen Probleme einen recht allgemeinen Einblick in die Schwächen der bisherigen Kandidaten und motivieren die Definition von stärkeren Logiken durch die Hinzunahme von Operatoren, die in der Lage sind solche algebraischen Probleme auszudrücken.Auf der anderen Seite haben sich algebraische Techniken, insbesondere Ideen aus der Gruppentheorie, als wichtige Elemente für Beweise von unteren Schranken für logische Systeme über endlichen Strukturen herauskristallisiert.So konnten wir etwa erst kürzlich, unter Verwendung algebraischer Argumente, neue Nicht-Definierbarkeitsaussagen für die beiden aktuell wichtigsten Kandidaten von Logiken für Polynomialzeit beweisen, nämlich für Ranglogik und für Choiceless Polynomial Time.In diesem Projekt möchten wir algebraische Ideen mit den Werkzeugen und Techniken aus der endlichen Modelltheorie kombinieren, um neue obere und untere Schranken für logische Systeme über endlichen Strukturen zu beweisen. Ein weiteres Ziel ist die Untersuchung von Struktureigenschaften, welche in Fixpunktlogik mit Zähloperatoren über Klassen endlicher Gruppen definiert werden können.Als einen verwandten Aspekt möchten wir die Ausdrucksstärke von Erweiterungen der Prädikatenlogik um invariante Hilfsrelationen untersuchen. Schließlich möchten wir einige der neuen Ansätze zur effizienten, approximativen Lösung des Graphisomorphieproblems untersuchen, welche auf algebraischen und logischen Methoden basieren.

• DFG-Verfahren: Forschungsstipendien
• Internationaler Bezug: Großbritannien
• Gastgeber: Professor Dr. Georg Gottlob; Professor Luke Ong