Logic, Symmetry, and Complexity

• Applicant: Professor Dr. Erich Grädel
• Subject Area: Theoretical Computer Science
• Term: from 2018 to 2022
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 405342984

The central objective of this project is the investigation of the expressive and computational power of algorithms that(1) operate directly on mathematical structures,(2) are specified in some adequate logical formalism, and(3) respect in each computational step all symmetries of the input structure and of the current state of the computation.Such symmetry-invariant algorithms arise in such scenarios where we work with objects that are understood and treated as abstract mathematical structures (databases, knowledge bases, transition systems etc.). However, many classical algorithms (such as depth first search or Gaußian elimination) are not symmetry-invariant; they break symmetries by explicit choices out of collections of equivalent objects.What are now the consequences of the (in many cases indispensible) requirement of symmetry-invariance? Is is possible to develop computation models and algorithms that are symmetry invariant, without paying a high prize in terms of computational power and complexity?A classical incarnation of this general objective is the question whether there is a logic for polynomial time, which is generally considered as the main open problem of descriptive complexity theory. The most important current candidates for such a logic are Rank Logic and Choiceless Polynomial Time. Algorithmic problems of foremost interest in this connection come from domains such as linear algebra, permutation group theory and linear equation systems.Besides finite structures, we shall also consider finitely definable sets over infinite structures. It is important to understand the arising symmetries in such contexts.Further objectives of this project concern the expressive and computational power of symmetry-invariant computation models and logics in connection with low-level-complexity, symmetric circuits, and propositional proof systems.

• DFG Programme: Research Grants