Logic, Symmetry, and Complexity

该项目的中心目标是研究算法的表达能力和计算能力，这些算法(1)直接在数学结构上操作，(2)在一些适当的逻辑形式中指定，以及(3)在每个计算步骤中尊重输入结构和当前计算状态的所有对称性。这种对称不变算法出现在这样的场景中，我们使用的对象被理解为抽象的数学结构（数据库、知识库、转换系统等）。然而，许多经典算法（如深度优先搜索或gau ß - elimination）不是对称不变的；它们通过在等效对象集合之外的显式选择来打破对称性。对称不变性要求（在许多情况下是不可缺少的）的结果是什么？是否有可能开发对称不变的计算模型和算法，而不需要在计算能力和复杂性方面付出高昂的代价？这个一般目标的一个经典体现是多项式时间是否存在逻辑的问题，这通常被认为是描述复杂性理论的主要开放问题。目前最重要的候选逻辑是秩逻辑和无选择多项式时间。在这方面最重要的算法问题来自线性代数、置换群论和线性方程组等领域。除了有限结构外，我们还将考虑无限结构上的有限可定义集。理解在这种情况下产生的对称性是很重要的。该项目的进一步目标是关注与低水平复杂性、对称电路和命题证明系统相关的对称不变计算模型和逻辑的表达和计算能力。

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.