Abstract
Albert Atserias
Title: Past and Present of Descriptive Complexity Theory
Abstract: Descriptive complexity theory can be thought of as addressing the same fundamental questions as computational complexity theory but in a different model of computation. Unlike Turing machines or Boolean circuits, that get their inputs as strings, the machines and circuits of the relational model get their inputs as unordered sets of tuples of atomic objects that reflect structure. The prototypical examples are graphs, i.e., binary relations among abstract vertices. This model of data has its origins in Codd's theory of relational databases (CACM 1970) with deep connections to logic and finite model theory. Since relational machines can be thought of as operating on inputs at varying levels of abstraction, the relational model has proved to be a flexible framework of wide applicability. From the point of view of the complexity theorist, a particularly appealing aspect of descriptive complexity is that it offers the opportunity to prove unconditional lower bounds for a fairly broad fragment of standard polynomial time computation (and beyond!). To get a sense of the power of the model, here is a list of computational tasks that relational machines operating in polynomial time *are* able to do: check graph connectivity, decompose into strongly connected components, compute shortest paths lengths, count walks in graphs, decide the existence of perfect matchings in graphs, compute determinants over rationals, decide solvability of systems of linear equations over rationals, solve linear programs and flow problems, approximately compute eigenvalues, solve semidefinite programs and more general convex programming problems, decide isomorphism of graphs with excluded minors or other structural restrictions, as well as be closed under some (but not all) of the most powerful methods of reduction between problems. I will start the talk by defining the relational model, state the early results of descriptive complexity, and quickly move to describe some of the non-trivial ideas that go into the aforementioned upper and lower bounds. Time permitting, I will briefly point out the possible directions of future work.
Benedikt Pago
Title: A Finite-Model-Theoretic View on Propositional Proof Complexity
Abstract: We establish connections between propositional proof systems and well-studied fixed-point logics from finite model theory, showing that these formalisms can mutually simulate each other in a natural sense.
Specifically, we consider Horn resolution, bounded-width resolution and the bounded-degree polynomial calculus and relate them to least fixed-point logic, existential least fixed-point logic and fixed-point logic with counting, respectively.
As a main application, this allows to transfer known lower bounds from finite model theory to proof complexity.
Antonina Kolokolova
Title: Reasoning Systems from Descriptive Complexity
Abstract: In descriptive complexity, the focus is on expressive power of various logics. But what is the power of reasoning with concepts expressible in these logics? Here, I will talk about building systems of arithmetic, a uniform version of proof systems, directly from logics of known complexity, and show when the resulting system captures exactly the reasoning with the corresponding power.