Algebraic Methods in Finite Model Theory

点击翻译按钮获取中文摘要

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.