Algebraische Methoden in der Endlichen Modelltheorie
Zusammenfassung der Projektergebnisse
In computer science, due to the pioneering work of Church and Turing, we have robust theoretical models that formalise our conception of computability. However, a severe limitation of these models is often neglected: they can only compute with very particular kinds of objects, basically with natural numbers. This is in stark contrast to the everyday reality in computer science, where we consider computations that operate with highly abstract and complex structures such as databases, (hyper-)graphs, networks, or even general algebraic structures. It might seem that, from the theoretical perspective, this mismatch does not cause any trouble, since all kinds of abstract structures can be encoded by natural numbers. This is, however, only true as long as we are interested in computability, as opposed to efficient computability. Indeed, if we try to formalise efficient computations with abstract structures, then it is no longer clear whether our standard theoretical models are still adequate. For instance, we don’t even know whether the encoding of structures by natural numbers is, by itself, an efficient operation. This raises the necessity to study more general kinds of computation models that better fit with our need to formalise computations with abstract structures, and not only with their encodings by numbers. The natural domain to find such formalisms is logic, more precisely finite model theory which studies the power of logics in the finite, as, indeed, logics are designed to reason about all different kinds of abstract mathematical structures. Unfortunately, as it turns out, it is quite hard to find a logical computation model that is, at the same time, compatible with our standard notion for efficient computability. Thus it remains one of the most intriguing and important open questions in finite model theory, which was first formulated more than 40 years ago, whether there is a logic that captures polynomial time, that is whether there is an efficient logical computation model that fits with our standard formalism for efficient computations (polynomial time). This fundamental question about the nature of efficient computations is of great importance also way beyond its own intrinsic value. Indeed, its study lead to the discovery of many deep and beautiful connections between logic and other important fields such as complexity theory, graph isomorphism testing, game theory, proof complexity, and even optimisation. Motivated by this long-standing open question, our project aimed to study new applications of algebraic techniques in finite model theory in order to analyse the power of logical computation systems, which may themselves be based on algebraic elements, and, in this way, to make progress towards finding a logic for polynomial time. For this project, the combination of algebraic and logical techniques has, once again, proven to be a powerful approach and we achieved many of our proposed research goals. For instance, we could answer a question of Rossman about the definability of summation problems in Abelian semigroups (which was open for more than ten years), several open questions of Berkholz and Grohe about the power of propositional proof systems, and we established a novel and strong framework to connect the research areas of finite model theory and proof complexity. As our work in this project has shown, this research line deserves further exploration and, in fact, in several ongoing collaborations, we are continuing our investigations on the role of algebraic techniques for logical computation models.
Projektbezogene Publikationen (Auswahl)
- (2019) A Finite-Model-Theoretic View on Propositional Proof Complexity.
Grädel, Erich; Grohe, Martin; Pago, Benedikt; Pakusa, Wied
(Siehe online unter https://doi.org/10.23638/LMCS-15(1:4)2019) - Descriptive Complexity of Linear Equation Systems and Applications to Propositional Proof Complexity, Logic in Computer Science (LICS), 2017
M. Grohe, W. Pakusa
(Siehe online unter https://doi.org/10.1109/LICS.2017.8005081) - Definability of Summation Problems for Abelian Groups and Semigroups, Logic in Computer Science (LICS), 2017
F. Abu Zaid, A. Dawar, E. Grädel, W. Pakusa
(Siehe online unter https://doi.ieeecomputersociety.org/10.1109/LICS.2017.8005082)
