Logik, Symmetrie und Komplexität

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

Das zentrale Anliegen dieses Vorhabens ist die Untersuchung der Ausdrucks- und Berechnungsstärke von Algorithmen, welche(1) direkt auf mathematischen Strukturen operieren,(2) in einem geeigneten logischen Formalismus spezifiziert sind, und damit(3) in jedem Berechnungsschritt alle Symmetrien der Eingabestruktur und des aktuellen Berechnungszustands respektieren.Solche symmetrie-invarianten Algorithmen sind überall dort wichtig, wo mit Objekten gearbeitet wird, welche in der Spezifikation des Algorithmus als abstrakte mathematische Strukturen verstanden und behandelt werden (z.B. Datenbanken, Wissensbasen, Transitionssysteme). Viele wichtige klassische Algorithmen (z.B. Tiefensuche oder Gauß-Elimination) sind dagegen nicht symmetrie-invariant; sie brechen Symmetrien durch explizite Auswahlen aus Kollektionen von in gewissem Sinn äquivalenten Objekten. Welche Konsequenzen erzwingt nun die (in gewissen Anwendungsszenarien unverzichtbare) Forderung nach Symmetrieinvarianz? Ist es vielleicht sogar möglich, symmetrie-invariante Berechnungsmodelle und Algorithmen ohne wesentliche Einbuße an Berechnungsstärke und Komplexität zu entwickeln. Eine klassische Inkarnation dieser allgemeinen Zielsetzung ist die Frage nach einer Logik für Polynomialzeit, welche als das wichtigste offene Problem der Deskriptiven Komplexitätstheorie gilt. Aktuelle Kandidaten für solche Logiken sind die Ranglogik und Choiceless Polynomial Time. Von besonderem Interesse ist dabei die Analyse algorithmischer Probleme aus der Linearen Algebra und Permutationsgruppentheorie, und das Lösen von linearen Gleichungssystemen. Neben endlichen Strukturen werden auch endlich definierbare Mengen über unendlichen Strukturen behandelt. Die Untersuchung der auftretenden Symmetrien ist dabei von entscheidender Bedeutung.Darüber hinaus soll die Ausdrucks- und Berechnungsstärke symmetrie-invarianter Berechnungsmodelle und Logiken in ihren Zusammenhängen zu Low-Level-Komplexität, symmetrischen Schaltkreisen und aussagenlogischen Beweissystemen untersucht werden.

• DFG-Verfahren: Sachbeihilfen