Algebraic Methods in Finite Model Theory

我们想研究有限模型理论中代数技术的应用，以分析逻辑系统对有限结构的表达能力。我们的中心动机是描述复杂性理论的主要开放问题：是否有一个逻辑，可以精确地表达多项式时间的有限结构的可判定性？这个问题的重要性源于这样一个事实，即如果我们找到多项式时间的逻辑特征，那么这将极大地增强我们对有效可解算法问题的理解，而如果我们可以证明不存在这样的逻辑，那么这将把PTIME从NP中分离出来。（线性）代数为这个长期存在的开放性挑战提供了新的动力，主要是由于以下两个原因：首先，来自代数和群论的基本算法技术，例如高斯消去法，在迄今为止提出的所有逻辑中都是不可定义的。更引人注目的是，所有已知的“困难的”基准属性都可以被看作是这种代数问题的特殊情况，例如在有限域上求解线性方程组的问题。在这个意义上，代数为迄今为止所考虑的逻辑的缺点提供了统一的解释，并且它引导了能够表达这种代数查询的新逻辑形式主义的道路。其次，代数方法，特别是群论的思想，在证明下界方面发挥了核心作用例如，我们最近应用代数方法证明了多项式时间内的（片段）的两个最重要的当前候选逻辑多项式时间，即无选择多项式时间和秩逻辑。在这个项目中，我们希望将联合收割机的代数思想与有限模型理论的强大工具和技术相结合，以获得多项式时间内的逻辑形式的新的上下界，如无选择多项式时间和秩逻辑。特别地，我们希望研究有限群上的计数不动点逻辑的表达能力。此外，作为一个相关的方面，我们要调查的权力，一阶逻辑的扩展不变的辅助关系，如顺序不变的一阶逻辑。最后，我们想研究最近的方法，图同构问题的基础上代数和逻辑的方法。

We want to study applications of algebraic techniques in finite model theory in order to analyse the expressive power of logical systems over finite structures. Our central motivation is the main open question of descriptive complexity theory: is there a logic which can express precisely the polynomial-time decidable properties of finite structures?The significance of this question stems from the fact that if we find a logical characterisation of polynomial time, then this would greatly enhance our understanding of the efficiently solvable algorithmic problems, while if one could show that no such logic exists, then this would separate PTIME from NP.In recent years, (linear) algebra has given a fresh impulse to this long-standing open challenge mainly due to the following two reasons.First of all, fundamental algorithmic techniques from algebra and group theory, such as Gaussian elimination, turned out to be undefinable in all logics that had been proposed so far. More strikingly, it turned out that all known "difficult" benchmark properties can be viewed as special cases of such algebraic problems, for instance of the problem of solving linear equation systems over finite fields.In this sense, algebra provides a uniform explanation for the shortcomings of the logics that had been considered so far and it guides the way to new logical formalisms that are able to express such algebraic queries.Secondly, algebraic methods, in particular ideas from group theory, have played a central role for proving lower bounds (that is, undefinability results) for many logical formalisms inside polynomial time.For instance, we recently applied algebraic methods to prove lower bounds for (fragments of) the two most important current candidates of logics for polynomial time, that is for Choiceless Polynomial Time and for rank logic.In this project, we want to combine algebraic ideas with the strong tools and techniques from finite model theory to obtain new lower and upper bounds for logical formalisms inside polynomial time such as Choiceless Polynomial Time and rank logic.In particular, we want to study the expressive power of fixed-point logic with counting over finite groups. Furthermore, as a related aspect we want to investigate the power of extensions of first-order logic by invariant auxiliary relations such as order-invariant first-order logic. Finally, we want to study recent approaches to the graph isomorphism problem which are based on algebraic and logical methods.