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

• Erstellungsjahr: 2022

Zusammenfassung der Projektergebnisse

Die generelle Zielsetzung dieses Vorhabens war 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. Es geht letztlich also um ein umfassendes Verständnis symmetrie-invarianter Berechnungen und die Frage, welche Konsequenzen, und welche Einschränkungen an Berechnungsstärke die (in gewissen Szenarien unverzichtbare) Forderung nach Symmetrieinvarianz erzwingt. Ist es vielleicht sogar möglich, symmetrie-invariante Berechnungsmodelle und Algorithmen ohne wesentliche Einbuße an Berechnungsstärke und Komplexität zu entwickeln? Die zentrale Frage der Endlichen Modelltheorie nach der Existenz einer Logik für Polynomialzeit kann als eine spezifische Inkarnation dieser generellen Zielsetzung gesehen werden. Die Haupresultate dieses Projekts fassen wir kurz wie folgt zusammen: Logiken mit linear-algebraischen Operatoren und Invertible-Map-Äquivalenzen. Wir haben inhärente Grenzen der Ausdrucksstärke von Logiken mit Operatoren der Linearen Algebra und der damit verbundenen Invertible-Map-Äquivalenzen aufgedeckt, und damit einige zentrale offene Fragen zur Deskriptiven Komplexitätstheorie und zum Graphen-Isomorphieproblem geklärt. • Es gibt kein festes k, so dass die Invertible-Map-Äquivalenz ≡IMk,P die Graphenisomorphie vollständig beschreibt. • Keine Erweiterung der Fixpunktlogik durch linear-algebraische Operatoren über Körpern kann Polynomialzeit vollständig charakterisieren. Choiceless Computation. Wir haben das Konzept symmetrieinvarianter Berechnungen, welche durch das Modell der choiceless computation formalisiert wird, auf verschiedenen Komplexitätsniveaux untersucht. Choiceless Polynomial Time (CPT) ist aktuell der naheliegendste Kandidat für eine Logik für Polymnomialzeit. Eine Reihe von strukturellen Resultaten über den Zusammenhang der Stärke von CPT mit den Symmetrien der Eingabestrukturen wurden bewiesen. Außerdem wurde ein adäquates Konzept von choiceless logspace vorgeschlagen und untersucht, welches als Modell für effiziente symmetrie-invariante Berechnungen für big data gesehen werden kann. Endliche Modelltheorie und aussagenlogische Beweissysteme. Zusammenhänge zwischen Fixpunktformalismen der Endlichen Modelltheorie einerseits und aussagenlogischen Beweissystemen andererseits wurden vertieft und insbesondere auf die Beweisstärke des polynomial calculus angewandt. Damit konnten auch Grenzen des polynomial calculus als Graphisomorphietest aufgezeigt werden.

Projektbezogene Publikationen (Auswahl)

• Approximations of Isomorphism and Logics with Linear-Algebraic Operators. In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019) (C. Baier, I. Chatzigiannakis, P. Flocchini, and S. Leonardi, Eds.), vol. 132 of Leibniz International Proceedings in Informatics (LIPIcs), pp
  A. Dawar, E. Grädel & W. Pakusa
  
• Choiceless computation and logic. PhD thesis, RWTH Aachen University, 2019
  S. Schalthöfer
  
• Choiceless Logarithmic Space. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019) (P. Rossmanith, P. Heggernes, and J. Katoen, Eds.), vol. 138 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 31:1–31:15, Dagstuhl, Germany. Schloss Dagstuhl–Leibniz-Zentrum für Informatik
  E. Grädel & S. Schalthöfer
  
• Convergence and Nonconvergence Laws for Random Expansions of Product Structures. Lecture Notes in Computer Science, 118-132. Springer International Publishing.
  Dawar, Anuj; Grädel, Erich & Hoelzel, Matthias
  
• Choiceless Computation and Symmetry: Limitations of Definability. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021) (C. Baier and J. Goubault-Larrecq, Eds.), vol. 183 of Leibniz International Proceedings in Informatics (LI- u PIcs), pp. 33:1–33:21, Dagstuhl, Germany. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 2021
  B. Pago
  
• A Finite-Model-Theoretic View on Propositional Proof Complexity. Logical Methods in Computer Science, Volume 15, Issue 1.
  Grädel, Erich; Grohe, Martin; Pago, Benedikt & Pakusa, Wied
  
• Limitations of the invertible-map equivalences. Journal of Logic and Computation, 33(5), 961-969.
  Dawar, Anuj; Grädel, Erich & Lichter, Moritz