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.