During the early days of relational database theory it was realized that "acyclic" database schemas possess a number of desirable properties. In fact, three different notions of "acyclicity" were identified and investigated during the 1980s, namely, α-acyclicity, β-acyclicity, and γ-acyclicity. Much more recently, the study of α-acyclicity was extended to annotated relations, where the annotations are values from some positive commutative monoid. The recent results about α-acyclic schemas and annotated relations give rise to results about β-acyclic schemas and annotated relations, since a schema is β-acyclic if and only if every sub-schema of it is α-acyclic. Here, we study γ-acyclic schemas and annotated relations. Our main finding is that the characterization of γ-acyclic schemas in terms of monotone sequential join expression extends to annotated relations, provided the annotations come from a positive commutative monoid that has the inner consistency property. Furthermore, the results reported here shed light on the role of the join of two standard relations. Specifically, our results reveal that the only relevant property of the join of two standard relations is that it is a witness to the consistency of the two relations, provided that these two relations are consistent. For the more abstract setting of annotated relations, this property of the standard join is captured by the notion of a consistency witness function, a notion which we systematically utilize in this work.

We investigate the expressive power of generalized quantifiers closed under partial polymorphism conditions motivated by the study of constraint satisfaction problems. We answer a number of questions arising from the work of Dawar and Hella (CSL 2024) where such quantifiers were introduced. For quantifiers closed under partial near-unanimity polymorphisms, we establish hierarchy results clarifying the interplay between the arity of the polymorphisms and of the quantifiers: The expressive power of $(\ell+1)$-ary quantifiers closed under $\ell$-ary partial near-unanimity polymorphisms is strictly between the class of all quantifiers of arity $\ell-1$ and $\ell$. We also establish an infinite hierarchy based on the arity of quantifiers with a fixed arity of partial near-unanimity polymorphisms. Finally, we prove inexpressiveness results for quantifiers with a partial Maltsev polymorphism. The separation results are proved using novel algebraic constructions in the style of Cai-Fürer-Immerman and the quantifier pebble games of Dawar and Hella (2024).

We study the status of classical model-theoretic preservation theorems such as the Łoś-Tarski theorem and the homomorphism preservation theorem in the context of semiring semantics. Semiring semantics has its origins in the provenance analysis of database queries but has been extended to a systematic way of evaluating logical statements to values in a commutative semiring. Depending on the underlying semiring, this allows us to track descriptions of the atomic facts that are responsible for the truth of a statement or practical information about the evaluation such as costs or confidence. The systematic development of semiring semantics for first-order logic and other logical systems raises the question to what extent classical model-theoretic results can be generalised to this setting and how such results depend on the underlying semiring. The definitions of semantic properties such as preservation under extensions, substructures, or homomorphisms naturally generalise to the setting of semiring semantics. However, the status of the corresponding preservation theorem strongly depends on the algebraic properties of the particular semirings. We prove that these preservation theorems do indeed hold for all lattice semirings (a quite large class, encompassing practically relevant semirings and in particular all min-max semirings). The proofs combine adaptations of the classical compactness and amalgamation methods with specific reduction methods for logical entailment that have been developed in semiring semantics. On the other side, variants of the existential preservation theorem fail for many other semirings, including the tropical semiring, the Viterbi semiring, the Łukasiewicz semiring, and the natural semirings ℕ and ℕ^∞. Surprisingly, the existential preservation theorem does hold for finite interpretations in a number of semirings, including the three-element min-max semiring, which extends the Boolean by just a single additional truth value. Thus, the situation for these semirings is in sharp contrast to the Boolean case, where the Łoś-Tarski theorem holds in general, but not in the finite.

The central open question of algebraic complexity is whether VP ≠ VNP, which is saying that the permanent cannot be represented by families of polynomial-size algebraic circuits. For symmetric algebraic circuits, this has been confirmed by Dawar and Wilsenach (2020), who showed exponential lower bounds on the size of symmetric circuits for the permanent. In this work, we set out to develop a more general symmetric algebraic complexity theory. Our main result is that a family of symmetric polynomials admits small symmetric circuits if and only if they can be written as a linear combination of homomorphism counting polynomials of graphs of bounded treewidth. We also establish a relationship between the symmetric complexity of subgraph counting polynomials and the vertex cover number of the pattern graph. As a concrete example, we examine the symmetric complexity of immanant families (a generalisation of the determinant and permanent) and show that a known conditional dichotomy due to Curticapean (2021) holds unconditionally in the symmetric setting.

The Kochen-Specker no-go theorem established that hidden-variable theories in quantum mechanics necessarily admit contextuality. This theorem is formally stated in terms of the partial Boolean algebra structure of projectors on a Hilbert space. Each partial Boolean algebra provides a semantics for interpreting propositional logic. In this paper, we examine the complexity of propositional satisfiability for various classes of partial Boolean algebras. We first show that the satisfiability problem for the class of non-trivial partial Boolean algebras is NP-complete. Next, we consider the satisfiability problem for the class of partial Boolean algebras arising from projectors on finite dimensional Hilbert spaces. For real Hilbert spaces of dimension greater 2 and any complex Hilbert spaces of dimension greater than 3, we demonstrate that the satisfiability problem is complete for the existential theory of the reals. Interestingly, the proofs of these results make use of Kochen-Specker sets as gadgets. As a corollary, we conclude that deciding quantum homomorphism in these fixed dimensions are also complete for the existential theory of the reals. Finally, we show that the satisfiability problems for the class of all Hilbert spaces and all finite-dimensional Hilbert spaces is undecidable.

Recent work by Atserias and Dawar [Albert Atserias and Anuj Dawar, 2019] and Tucker-Foltz [Jamie Tucker-Foltz, 2024] has established undefinability results in fixed-point logic with counting (FPC) corresponding to many classical complexity results from the hardness of approximation. In this line of work, NP-hardness results are turned into unconditional FPC undefinability results. We extend this work by showing the FPC undefinability of any constant factor approximation of weighted 2-to-2 games, based on the NP-hardness results of Khot, Minzer and Safra. Our result shows that the completely satisfiable 2-to-2 games are not FPC-separable from those that are not ε-satisfiable, for arbitrarily small ε. The perfect completeness of our inseparability is an improvement on the complexity result, as the NP-hardness of such a separation is still only conjectured. This perfect completeness enables us to show the FPC undefinability of other problems whose NP-hardness is conjectured. In particular, we are able to show that no FPC formula can separate the 3-colourable graphs from those that are not t-colourable, for any constant t.

Krebs et al. (2007) gave a characterization of the complexity class TC⁰ as the class of languages recognized by a certain class of typed monoids. The notion of typed monoid was introduced to extend methods of algebraic automata theory to infinite monoids and hence characterize classes beyond the regular languages. We advance this line of work beyond TC⁰ by giving a characterization of NC¹. This is obtained by first showing that NC¹ can be defined as the languages expressible in an extension of first-order logic using only unary quantifiers over regular languages. The expressibility result is a consequence of a general result showing that finite monoid multiplication quantifiers of higher dimension can be replaced with unary quantifiers in the context of interpretations over strings, which also answers a question of Lautemann et al. (2001). We estblish this collapse result for a much more general class of interpretations using results on interpretations due to Bojańczyk et al. (2019), which may be of independent interest.

We consider the Ideal Proof System (IPS) introduced by Grochow and Pitassi and pose the question of which tautologies admit symmetric proofs, and of what complexity. The symmetry requirement in proofs is inspired by recent work establishing lower bounds in other symmetric models of computation. We link the existence of symmetric IPS proofs to the expressive power of logics such as fixed-point logic with counting and Choiceless Polynomial Time, specifically regarding the graph isomorphism problem. We identify relationships and tradeoffs between the symmetry of proofs and other parameters of IPS proofs such as size, degree and linearity. We study these on a number of standard families of tautologies from proof complexity and finite model theory such as the pigeonhole principle, the subset sum problem and the Cai-Fürer-Immerman graphs, exhibiting non-trivial upper bounds on the size of symmetric IPS proofs.

We study Lindström quantifiers that satisfy certain closure properties which are motivated by the study of polymorphisms in the context of constraint satisfaction problems (CSP). When the algebra of polymorphisms of a finite structure B satisfies certain equations, this gives rise to a natural closure condition on the class of structures that map homomorphically to B. The collection of quantifiers that satisfy closure conditions arising from a fixed set of equations are rather more general than those arising as CSP. For any such conditions P, we define a pebble game that delimits the distinguishing power of the infinitary logic with all quantifiers that are P-closed. We use the pebble game to show that the problem of deciding whether a system of linear equations is solvable in Z /2 Z is not expressible in the infinitary logic with all quantifiers closed under a near-unanimity condition.

A graph class $\mathscr{C}$ is called monadically stable if one cannot interpret, in first-order logic, arbitrary large linear orders in colored graphs from $\mathscr{C}$. We prove that the model checking problem for first-order logic is fixed-parameter tractable on every monadically stable graph class. This extends the results of [Grohe, Kreutzer, and Siebertz; J. ACM '17] for nowhere dense classes and of [Dreier, Mählmann, and Siebertz; STOC '23] for structurally nowhere dense classes to all monadically stable classes. As a complementary hardness result, we prove that for every hereditary graph class $\mathscr{C}$ that is edge-stable (excludes some half-graph as a semi-induced subgraph) but not monadically stable, first-order model checking is $\mathrm{AW}[*]$-hard on $\mathscr{C}$, and $\mathrm{W}[1]$-hard when restricted to existential sentences. This confirms, in the special case of edge-stable classes, an on-going conjecture that the notion of monadic NIP delimits the tractability of first-order model checking on hereditary classes of graphs. For our tractability result, we first prove that monadically stable graph classes have almost linear neighborhood complexity. Using this, we construct sparse neighborhood covers for monadically stable classes, which provides the missing ingredient for the algorithm of [Dreier, Mählmann, and Siebertz; STOC '23]. The key component of this construction is the usage of orders with low crossing number [Welzl; SoCG '88], a tool from the area of range queries. For our hardness result, we prove a new characterization of monadically stable graph classes in terms of forbidden induced subgraphs. We then use this characterization to show that in hereditary classes that are edge-stable but not monadically stable, one can effectively interpret the class of all graphs using only existential formulas.

Game comonads, introduced by Abramsky, Dawar and Wang and developed by Abramsky and Shah, give an interesting categorical semantics to some Spoiler-Duplicator games that are common in finite model theory. In particular they expose connections between one-sided and two-sided games, and parameters such as treewidth and treedepth and corresponding notions of decomposition. In the present paper, we expand the realm of game comonads to logics with generalised quantifiers. In particular, we introduce a comonad graded by two parameters $n \leq k$ such that isomorphisms in the resulting Kleisli category are exactly Duplicator winning strategies in Hella's $n$-bijection game with $k$ pebbles. We define a one-sided version of this game which allows us to provide a categorical semantics for a number of logics with generalised quantifiers. We also give a novel notion of tree decomposition that emerges from the construction.

We study the first-order (FO) model checking problem of dense graphs, namely those which have FO interpretations in (or are FO transductions of) some sparse graph classes. We give a structural characterization of the graph classes which are FO interpretable in graphs of bounded degree. This characterization allows us to efficiently compute such an FO interpretation for an input graph. As a consequence, we obtain an FPT algorithm for successor-invariant FO model checking of any graph class which is FO interpretable in (or an FO transduction of) a graph class of bounded degree. The approach we use to obtain these results may also be of independent interest.

Let G be a graph on n vertices with adjacency matrix A, and let 1 be the all-ones vector. We call G controllable if the set of vectors 1, A1,..., An-11 spans the whole space Rn. We characterize the isomorphism problem of controllable graphs in terms of other combinatorial, geometric and logical problems. We also describe a polynomial time algorithm for graph isomorphism that works for almost all graphs.

Abstract This note draws conclusions that arise by combining two recent papers, by Anuj Dawar, Erich Grädel and Wied Pakusa, published at ICALP 2019, and by Moritz Lichter, published at LICS 2021. In both papers, the main technical results rely on the combinatorial and algebraic analysis of the invertible-map equivalences ${\equiv ^{\text {IM}}_{k, Q}}$ on certain variants of Cai–Fürer–Immerman structures (CFI-structures for short). These ${\equiv ^{\text {IM}}_{k, Q}}$-equivalences, for a natural number $k$ and a set of primes $Q$, refine the well-known Weisfeiler–Leman equivalences used in algorithms for graph isomorphism. The intuition is that two graphs $G{\equiv ^{\text {IM}}_{k, Q}}H$ cannot be distinguished by iterative refinements of equivalences on $k$-tuples defined via linear operators on vector spaces over fields of characteristic $p \in Q$. In the first paper it has been shown, using considerable algebraic machinery, that for a prime $q \notin Q$, the ${\equiv ^{\text {IM}}_{k, Q}}$ equivalences are not strong enough to distinguish between non-isomorphic CFI-structures over the field $\mathbb {F}_q$. In the second paper, a similar but not identical construction for CFI-structures over the rings $\mathbb {Z}_{2^i}$ has, again by rather involved combinatorial and algebraic arguments, been shown to be indistinguishable with respect to ${\equiv ^{\text {IM}}_{k, \{2\}}}$. Together with an earlier work on rank logic, this second result suffices to separate rank logic from polynomial time. We show here that the two approaches can be unified to prove that CFI-structures over the rings $\mathbb {Z}_{2^i}$ are in fact indistinguishable with respect to ${\equiv ^{\text {IM}}_{k, {\mathbb {P}}}}$, for the set ${\mathbb {P}}$ of all primes. In particular, this implies the following two results. First, there is no fixed $k$ such that the invertible-map equivalence ${\equiv ^{\text {IM}}_{k, {\mathbb {P}}}}$ coincides with isomorphism on all finite graphs. Second, no extension of fixed-point logic by linear-algebraic operators over fields can capture polynomial time.

is an extension of first-order logic with a logarithmic recursion operator. It was introduced by Grohe et al. and shown to capture the complexity class L over trees and interval graphs. It does not capture L in general as it is contained in —fixed-point logic with counting. We show that this containment is strict. In particular, we show that the path systems problem, a classic P-complete problem which is definable in —fixed-point logic—is not definable in . This shows that the logarithmic recursion mechanism is provably weaker than general least fixed points.

Fixed-point logic with rank (FPR) is an extension of fixed-point logic with counting (FPC) with operators for computing the rank of a matrix over a finit field. The expressive power of FPR properly extends that of FPC and is contained in P, but it is not known if that containment is proper. We give a circuit characterization for FPR in terms of families of symmetric circuits with rank gates, along the lines of that for FPC given by Anderson and Dawar in 2017. This requires the development of a broad framework of circuits in which the individual gates compute functions that are not symmetric (i.e., invariant under all permutations of their inputs). This framework also necessitates the development of novel techniques to prove the equivalence of circuits and logic. Both the framework and the techniques are of greater generality than the main result.

Game comonads, introduced by Abramsky, Dawar and Wang and developed by Abramsky and Shah, give an interesting categorical semantics to some Spoiler-Duplicator games that are common in finite model theory. In particular they expose connections between one-sided and two-sided games, and parameters such as treewidth and treedepth and corresponding notions of decomposition. In the present paper, we expand the realm of game comonads to logics with generalised quantifiers. In particular, we introduce a comonad graded by two parameter n ≤ k such that isomorphisms in the resulting Kleisli category are exactly Duplicator winning strategies in Hella’s n-bijection game with k pebbles. We define a one-sided version of this game which allows us to provide a categorical semantics for a number of logics with generalised quantifiers. We also give a novel notion of tree decomposition that emerges from the construction.

It is well known that the classic Łoś-Tarski preservation theorem fails in the finite: there are first-order definable classes of finite structures closed under extensions which are not definable (in the finite) in the existential fragment of first-order logic. We strengthen this by constructing for every $n$, first-order definable classes of finite structures closed under extensions which are not definable with $n$ quantifier alternations. The classes we construct are definable in the extension of Datalog with negation and indeed in the existential fragment of transitive-closure logic. This answers negatively an open question posed by Rosen and Weinstein.

Lovász (1967) showed that two finite relational structures A and B are isomorphic if, and only if, the number of homomorphisms from C to A is the same as the number of homomorphisms from C to B for any finite structure C. Soon after, Pultr (1973) proved a categorical generalisation of this fact. We propose a new categorical formulation, which applies to any locally finite category with pushouts and a proper factorisation system. As special cases of this general theorem, we obtain two variants of Lovász' theorem: the result by Dvořák (2010) that characterises equivalence of graphs in the k-dimensional Weisfeiler-Leman equivalence by homomorphism counts from graphs of tree-width at most k, and the result of Grohe (2020) characterising equivalence with respect to first-order logic with counting and quantifier depth k in terms of homomorphism counts from graphs of tree-depth at most k. The connection of our categorical formulation with these results is obtained by means of the game comonads of Abramsky et al. We also present a novel application to homomorphism counts in modal logic.

We compare the capabilities of two approaches to approximating graph isomorphism using linear algebraic methods: the invertible map tests (introduced by Dawar and Holm) and proof systems with algebraic rules, namely polynomial calculus, monomial calculus and Nullstellensatz calculus. In the case of fields of characteristic zero, these variants are all essentially equivalent to the Weisfeiler-Leman algorithms. In positive characteristic we show that the distinguishing power of the monomial calculus is no greater than the invertible map method by simulating the former in a fixed-point logic with solvability operators. In turn, we show that the distinctions made by this logic can be implemented in the Nullstellensatz calculus.

Invertible map equivalences are approximations of graph isomorphism that refine the well-known Weisfeiler-Leman method. They are parameterized by a number k and a set Q of primes. The intuition is that two equivalent graphs G equiv^IM_{k, Q} H cannot be distinguished by means of partitioning the set of k-tuples in both graphs with respect to any linear-algebraic operator acting on vector spaces over fields of characteristic p, for any p in Q. These equivalences have first appeared in the study of rank logic, but in fact they can be used to delimit the expressive power of any extension of fixed-point logic with linear-algebraic operators. We define {LA^{k}}(Q), an infinitary logic with k variables and all linear-algebraic operators over finite vector spaces of characteristic p in Q and show that equiv^IM_{k, Q} is the natural notion of elementary equivalence for this logic. The logic LA^{omega}(Q) = Cup_{k in omega} LA^{k}(Q) is then a natural upper bound on the expressive power of any extension of fixed-point logics by means of Q-linear-algebraic operators. By means of a new and much deeper algebraic analysis of a generalized variant, for any prime p, of the CFI-structures due to Cai, Fürer, and Immerman, we prove that, as long as Q is not the set of all primes, there is no k such that equiv^IM_{k, Q} is the same as isomorphism. It follows that there are polynomial-time properties of graphs which are not definable in LA^{omega}(Q), which implies that no extension of fixed-point logic with linear-algebraic operators can capture PTIME, unless it includes such operators for all prime characteristics. Our analysis requires substantial algebraic machinery, including a homogeneity property of CFI-structures and Maschke’s Theorem, an important result from the representation theory of finite groups.

We consider families of symmetric linear programs (LPs) that decide a property of graphs (or other relational structures) in the sense that, for each size of graph, there is an LP defining a polyhedral lift that separates the integer points corresponding to graphs with the property from those corresponding to graphs without the property. We show that this is equivalent, with at most polynomial blow-up in size, to families of symmetric Boolean circuits with threshold gates. In particular, when we consider polynomial-size LPs, the model is equivalent to definability in a non-uniform version of fixed-point logic with counting (FPC). Known upper and lower bounds for FPC apply to the non-uniform version. In particular, this implies that the class of graphs with perfect matchings has polynomial-size symmetric LPs, while we obtain an exponential lower bound for symmetric LPs for the class of Hamiltonian graphs. We compare and contrast this with previous results (Yannakakis 1991), showing that any symmetric LPs for the matching and TSP polytopes have exponential size. As an application, we establish that for random, uniformly distributed graphs, polynomial-size symmetric LPs are as powerful as general Boolean circuits. We illustrate the effect of this on the well-studied planted-clique problem.

Abstract We consider the hardness of approximation of optimization problems from the point of view of definability. For many $\textrm{NP}$-hard optimization problems it is known that, unless $\textrm{P} = \textrm{NP} $, no polynomial-time algorithm can give an approximate solution guaranteed to be within a fixed constant factor of the optimum. We show, in several such instances and without any complexity theoretic assumption, that no algorithm that is expressible in fixed-point logic with counting (FPC) can compute an approximate solution. Since important algorithmic techniques for approximation algorithms (such as linear or semidefinite programming) are expressible in FPC, this yields lower bounds on what can be achieved by such methods. The results are established by showing lower bounds on the number of variables required in first-order logic with counting to separate instances with a high optimum from those with a low optimum for fixed-size instances.

The Ackermann Award is the EACSL Outstanding Dissertation Award for Logic in Computer Science. It is presented during the annual conference of the EACSL (CSL'xx). This contribution reports on the 2017 edition of the award.

Pebble games are a powerful tool in the study of finite model theory, constraint satisfaction and database theory. Monads and comonads are basic notions of category theory which are widely used in semantics of computation and in modern functional programming. We show that existential k-pebble games have a natural comonadic formulation. Winning strategies for Duplicator in the k-pebble game for structures A and B are equivalent to morphisms from A to B in the coKleisli category for this comonad. This leads on to comonadic characterisations of a number of central concepts in Finite Model Theory: · Isomorphism in the co-Kleisli category characterises elementary equivalence in the k-variable logic with counting quantifiers. · Symmetric games corresponding to equivalence in full k-variable logic are also characterized. · The treewidth of a structure A is characterised in terms of its coalgebra number: the least k for which there is a coalgebra structure on A for the k-pebbling comonad. · Co-Kleisli morphisms are used to characterize strong consistency, and to give an account of a Cai-Fürer-Immerman construction. · The k-pebbling comonad is also used to give semantics to a novel modal operator. These results lay the basis for some new and promising connections between two areas within logic in computer science which have largely been disjoint: (1) finite and algorithmic model theory, and (2) semantics and categorical structures of computation.

We show that the ellipsoid method for solving semidefinite programs (SDPs) can be expressed in fixed-point logic with counting (FPC). This generalizes an earlier result that the optimal value of a linear program can be expressed in this logic. As an application, we establish lower bounds on the number of levels of the Lasserre hierarchy required to solve many optimization problems, namely those that can be expressed as finite-valued constraint satisfaction problems (VCSPs). In particular, we establish a dichotomy on the number of levels of the Lasserre hierarchy that are required to solve the problem exactly. We show that if a finite-valued constraint problem is not solved exactly by its basic linear programming relaxation, it is also not solved exactly by any sub-linear number of levels of the Lasserre hierarchy. The lower bounds are established through logical undefinability results. We show that the SDP corresponding to any fixed level of the Lasserre hierarchy is interpretable in a VCSP instance by means of FPC formulas. Our definability result of the ellipsoid method then implies that the solution of this SDP can be expressed in this logic. Together, these results give a way of translating lower bounds on the number of variables required in counting logic to express a VCSP into lower bounds on the number of levels required in the Lasserre hierarchy to eliminate the integrality gap. As a special case, we obtain the same dichotomy for the class of MAXCSP problems, generalizing earlier Lasserre lower bound results by Schoenebeck [17]. Recently, and independently of the work reported here, a similar linear lower bound in the Lasserre hierarchy for general-valued CSPs has also been announced by Thapper and Zivny [20], using different techniques.

We study the descriptive complexity of summation problems in Abelian groups and semigroups. In general, an input to the summation problem consists of an Abelian semigroup G, explicitly represented by its multiplication table, and a subset X of G. The task is to determine the sum over all elements of X. Algorithmically this is a very simple problem. If the elements of X come in some order, then we can process these elements along that order and calculate the sum in a trivial way. However, what makes this fundamental problem so interesting for us is that from the viewpoint of logical definability its tractability is much more delicate. If we consider the semigroup G as an abstract structure and X as an abstract set, without a linear order and hence without a canonical way to process the elements one by one, then it is unclear how to define the sum in any logic that does not have the power to quantify over a linear order. Indeed the trivial summation algorithm cannot be expressed in any polynomial-time logic or, in fact, in any computational model which works on abstract mathematical structures in an isomorphism-invariant way without violating polynomial resource bounds. The surprising difficulty, in terms of logical definability, of this basic mathematical problem is the reason why Ben Rossman asked, more than ten years ago, whether it can be expressed in the logic Choiceless Polynomial Time with counting (CPT). Note that, to date, CPT is one of the most powerful known candidates for a logic that might be capable of defining every polynomial-time property of finite structures. In this paper we clarify the status of the definability for the summation problem for Abelian groups and semigroups in important polynomial-time logics. In our first main result we show that the problem can be defined in fixed-point logic with counting (FPC). Since FPC is contained in CPT this settles Rossman's question. Our proof is based on a dynamic programming approach and heavily uses the counting mechanism of FPC. In our second main result we give a matching lower bound and show that the use of counting operators cannot be avoided: the summation problem, even over Abelian groups, cannot be defined in pure fixed-point logic without counting. Our proof is based on a probabilistic argument.

We show that for various classes $$\mathcal {C}$$ of sparse graphs, and several measures of distance to such classes (such as edit distance and elimination distance), the problem of determining the distance of a given graph G to $$\mathcal {C}$$ is fixed-parameter tractable. The results are based on two general techniques. The first of these, building on recent work of Grohe et al. establishes that any class of graphs that is slicewise nowhere dense and slicewise first-order definable is $$\mathrm {FPT} $$ . The second shows that determining the elimination distance of a graph G to a minor-closed class $$\mathcal {C}$$ is $$\mathrm {FPT} $$ . We demonstrate that several prior results (of Golovach, Moser and Thilikos and Mathieson) on the fixed-parameter tractability of distance measures are special cases of our first method.

We define a general framework of partition games for formulating two-player pebble games over finite structures. We show that one particular such game, which we call the invertible-map game, yields a family of polynomial-time approximations of graph isomorphism that is strictly stronger than the well-known Weisfeiler-Lehman method. The general framework we introduce includes as special cases the pebble games for finite-variable logics with and without counting. It also includes a matrix-equivalence game, introduced here, which characterises equivalence in the finite-variable fragments of matrix-rank logic. We show that the equivalence defined by the invertible-map game is a refinement of the equivalence defined by each of these games for finite-variable logics.

The finite spectrum of a first-order sentence is the set of positive integers that are the sizes of its models. The class of finite spectra is known to be the same as the complexity class NE. We consider the spectra obtained by limiting models to be either planar (in the graph-theoretic sense) or by bounding the degree of elements. We show that the class of such spectra is still surprisingly rich by establishing that significant fragments of NE are included among them. At the same time, we establish non-trivial upper bounds showing that not all sets in NE are obtained as planar or bounded-degree spectra.

We study properties of relational structures, such as graphs, that are decided by families of Boolean circuits. Circuits that decide such properties are necessarily invariant to permutations of the elements of the input structures. We focus on families of circuits that are symmetric, i.e., circuits whose invariance is witnessed by automorphisms of the circuit induced by the permutation of the input structure. We show that the expressive power of such families is closely tied to definability in logic. In particular, we show that the queries defined on structures by uniform families of symmetric Boolean circuits with majority gates are exactly those definable in fixed-point logic with counting. This shows that inexpressibility results in the latter logic lead to lower bounds against polynomial-size families of symmetric circuits.

The Ackermann Award is the EACSL Outstanding Dissertation Award for Logic in Computer Science. It is presented during the annual conference of the EACSL (CSL'xx). This contribution reports on the 2016 edition of the award.

A commonly studied means of parameterizing graph problems is the deletion distance from triviality (Guo et al., Parameterized and exact computation, Springer, Berlin, pp. 162–173, 2004), which counts vertices that need to be deleted from a graph to place it in some class for which efficient algorithms are known. In the context of graph isomorphism, we define triviality to mean a graph with maximum degree bounded by a constant, as such graph classes admit polynomial-time isomorphism tests. We generalise deletion distance to a measure we call elimination distance to triviality, based on elimination trees or tree-depth decompositions. We establish that graph canonisation, and thus graph isomorphism, is $$\mathsf {FPT}$$ when parameterized by elimination distance to bounded degree, extending results of Bouland et al. (Parameterized and exact computation, Springer, Berlin, pp. 218–230, 2012).

The eleventh Ackermann Award is presented at CSL'15 in Berlin, Germany. This year, again, the EACSL Ackermann Award is generously sponsored by the Kurt Gödel Society. Besides providing financial support for the Ackermann Award, the Kurt Gödel Society has also committed to inviting the recipients of the Award for a special lecture to be given to the Society in Vienna.

Finite valued constraint satisfaction problems are a formalism for describing many natural optimisation problems, where constraints on the values that variables can take come with rational weights and the aim is to find an assignment of minimal cost. Thapper and Zivny have recently established a complexity dichotomy for valued constraint languages. They show that each such languages either gives rise to a polynomial-time solvable optimisation problem, or to an NP-hard one, and establish a criterion to distinguish the two cases. We refine the dichotomy by showing that all optimisation problems in the first class are definable in fixed-point language with counting, while all languages in the second class are not definable, even in infinitary logic with counting. Our definability dichotomy is not conditional on any complexity-theoretic assumption.

We show that for various classes C of sparse graphs, and several measures of distance to such classes (such as edit distance and elimination distance), the problem of determining the distance of a given graph G to C is fixed-parameter tractable. The results are based on two general techniques. The first of these, building on recent work of Grohe et al. establishes that any class of graphs that is slicewise nowhere dense and slicewise first-order definable is FPT. The second shows that determining the elimination distance of a graph G to a minor-closed class C is FPT.

We show that the ellipsoid method for solving linear programs can be implemented in a way that respects the symmetry of the program being solved. That is to say, there is an algorithmic implementation of the method that does not distinguish, or make choices, between variables or constraints in the program unless they are distinguished by properties definable from the program. In particular, we demonstrate that the solvability of linear programs can be expressed in fixed-point logic with counting (FPC) as long as the program is given by a separation oracle that is itself definable in FPC. We use this to show that the size of a maximum matching in a graph is definable in FPC. This settles an open problem first posed by Blass, Gurevich and Shelah [Blass et al. 1999]. On the way to defining a suitable separation oracle for the maximum matching program, we provide FPC formulas defining canonical maximum flows and minimum cuts in undirected capacitated graphs.

We study properties of relational structures such as graphs that are decided by families of Boolean circuits. Circuits that decide such properties are necessarily invariant to permutations of the elements of the input structures. We focus on families of circuits that are symmetric, i.e., circuits whose invariance is witnessed by automorphisms of the circuit induced by the permutation of the input structure. We show that the expressive power of such families is closely tied to definability in logic. In particular, we show that the queries defined on structures by uniform families of symmetric Boolean circuits with majority gates are exactly those definable in fixed-point logic with counting. This shows that inexpressibility results in the latter logic lead to lower bounds against polynomial-size families of symmetric circuits.

Kolaitis and Kopparty have shown that for any first-order formula with parity quantifiers over the language of graphs, there is a family of multivariate polynomials of constant-degree that agree with the formula on all but a 2 −Ω( n ) -fraction of the graphs with n vertices. The proof bounds the degree of the polynomials by a tower of exponentials whose height is the nesting depth of parity quantifiers in the formula. We show that this tower-type dependence is necessary. We build a family of formulas of depth q whose approximating polynomials must have degree bounded from below by a tower of exponentials of height proportional to q . Our proof has two main parts. First, we adapt and extend the results by Kolaitis and Kopparty that describe the joint distribution of the parities of the numbers of copies of small subgraphs in a random graph to the setting of graphs of growing size. Second, we analyze a variant of Karp's graph canonical labeling algorithm and exploit its massive parallelism to get a formula of low depth that defines an almost canonical pre-order on a random graph.

Report on the Ackermann Award 2013.

We establish the expressibility in fixed-point logic with counting (FPC) of a number of natural polynomial-time problems. In particular, we show that the size of a maximum matching in a graph is definable in FPC. This settles an open problem first posed by Blass, Gurevich and Shelah [1], who asked whether the existence of perfect matchings in general graphs could be determined in the more powerful formalism of choiceless polynomial time with counting. Our result is established by noting that the ellipsoid method for solving linear programs of full dimension can be implemented in FPC. This allows us to prove that linear programs of full dimension can be optimised in FPC if the corresponding separation oracle problem can be defined in FPC. On the way to defining a suitable separation oracle for the maximum matching problem, we provide FPC formulas defining maximum flows and canonical minimum cuts in capacitated graphs.

We study 0-1 laws for extensions of first-order logic by Lindström quantifiers. We state sufficient conditions on a quantifier Q expressing a graph property, for the logic FO[Q] – the extension of first-order logic by means of the quantifier Q – to have a 0-1 law. We use these conditions to show, in particular, that FO[Rig], where Rig is the quantifier expressing rigidity, has a 0-1 law. We also show that extensions of first-order logic with quantifiers for Hamiltonicity, regularity and self-complementarity of graphs do not have a 0-1 law. Blass and Harary pose the question whether there is a logic which is powerful enough to express Hamiltonicity or rigidity and which has a 0-1 law. It is a consequence of our results that there is no such regular logic (in the sense of abstract model theory) in the case of Hamiltonicity, but there is one in the case of rigidity. We also consider sequences of vectorized quantifiers, and show that the extensions of first-order logic obtained by adding such sequences generated by quantifiers that are closed under substructures have 0-1 laws. The positive results also extend to the infinitary logic with finitely many variables.

If computational complexity is the study of what makes certain computational problems inherently difficult to solve, an important contribution of descriptive complexity in this regard is the separation it provides between the specification of a decision problem and the structure against which this specification is checked. The formalisation of these two aspects leads to tools for studying them as sources of complexity, and on the one hand leads to results in the characterisation of complexity classes and on the other elates to parameterized complexity. In these notes accompanying the invited talk, some definitions and results are presented leading to recent work on the characterisation of polynomial time and on the parameterized complexity of first-order logic on restricted graph classes.

We investigate the parameterized complexity of generalisations and variations of the dominating set problem on classes of graphs that are nowhere dense. In particular, we show that the distance-$d$ dominating-set problem, also known as the $(k,d)$-centres problem, is fixed-parameter tractable on any class that is nowhere dense and closed under induced subgraphs. This generalises known results about the dominating set problem on $H$-minor free classes, classes with locally excluded minors and classes of graphs of bounded expansion. A key feature of our proof is that it is based simply on the fact that these graph classes are uniformly quasi-wide, and does not rely on a structural decomposition. Our result also establishes that the distance-$d$ dominating-set problem is FPT on classes of bounded expansion, answering a question of Ne{\v s}et{\v r}il and Ossona de Mendez.

We introduce extensions of first-order logic (FO) and fixed-point logic (FP) with operators that compute the rank of a definable matrix. These operators are generalizations of the counting operations in FP+C (i.e. fixed-point logic with counting) that allow us to count the dimension of a definable vector space, rather than just count the cardinality of a definable set. The logics we define have data complexity contained in polynomial time and all known examples of polynomial time queries that are not definable in FP+C are definable in FP+rk, the extension of FP with rank operators. For each prime number p and each positive integer n, we have rank operators rkpfor determining the rank of a matrix over the finite field GFpdefined by a formula over n-tuples. We compare the expressive power of the logics obtained by varying the values p and n can take. In particular, we show that increasing the arity of the operators yields an infinite hierarchy of expressive power. The rank operators are surprisingly expressive, even in the absence of fixed-point operators. We show that FO+rkpcan define deterministic and symmetric transitive closure. This allows us to show that, on ordered structures, FO+rkpcaptures the complexity class MODpL, for all prime values of p.

A class of relational structures is said to have the extension preservation property if every first-order sentence that is preserved under extensions on the class is equivalent to an existential sentence. The class of all finite structures does not have the extension preservation property. We study the property on classes of finite structures that are better behaved. We show that the property holds for classes of acyclic structures, structures of bounded degree, and more generally structures that are wide in a sense that we will make precise. We also show that the preservation property holds for the class of structures of treewidth at most k, for any k. In contrast, we show that the property fails for the class of planar graphs.

We introduce the concept of locally excluded minors. Graph classes locally excluding a minor are a common generalisation of the concept of excluded minor classes and of graph classes with bounded local tree-width. We show that first-order model-checking is fixed-parameter tractable on any class of graphs locally excluding a minor. This strictly generalises analogous results by Flum and Grohe on excluded minor classes and Frick and Grohe on classes with bounded local tree-width. As an important consequence of the proof we obtain fixed-parameter algorithms for problems such as dominating or independent set on graph classes excluding a minor, where now the parameter is the size of the dominating set and the excluded minor. We also study graph classes with excluded minors, where the minor may grow slowly with the size of the graphs and show that again, first-order model-checking is fixed-parameter tractable on any such class of graphs.

Let phi(X) be a first-order formula in the language of graphs that has a free set variable X, and assume that X only occurs positively in phi(X). Then a natural minimisation problem associated with phi(X) is to find, in a given graph G, a vertex set S of minimum size such that G satisfies phi(S). Similarly, if X only occurs negatively in phi(X), then phi(X) defines a maximisation problem. Many well-known optimisation problems are first-order definable in this sense, for example, minimum dominating set or maximum independent set. We prove that for each class Gscr of graphs with excluded minors, in particular for each class of planar graphs, the restriction of a first-order definable optimisation problem to the class Gscr has a polynomial time approximation scheme. A crucial building block of the proof of this approximability result is a version of Gaifman's locality theorem for formulas positive in a set variable. This result may be of independent interest

Unions of conjunctive queries, also known as select-project-join-union queries, are the most frequently asked queries in relational database systems. These queries are definable by existential positive first-order formulas and are preserved under homomorphisms. A classical result of mathematical logic asserts that the existential positive formulas are the only first-order formulas (up to logical equivalence) that are preserved under homomorphisms on all structures, finite and infinite. The question of whether the homomorphism-preservation theorem holds for the class of all finite structures resisted solution for a long time. It was eventually shown that, unlike other classical preservation theorems, the homomorphism-preservation theorem does hold in the finite. In this article, we show that the homomorphism-preservation theorem holds also for several restricted classes of finite structures of interest in graph theory and database theory. Specifically, we show that this result holds for all classes of finite structures of bounded degree, all classes of finite structures of bounded treewidth, and, more generally, all classes of finite structures whose cores exclude at least one minor.

We investigate model theoretic characterisations of the expressive power of modal logics in terms of bisimulation invariance. The paradigmatic result of this kind is van Benthem's theorem, which says that a first-order formula is invariant under bisimulation if and only if it is equivalent to a formula of basic modal logic. The present investigation primarily concerns ramifications for specific classes of structures. We study in particular model classes defined through conditions on the underlying frames, with a focus on frame classes that play a major role in modal correspondence theory and often correspond to typical application domains of modal logics. Classical model theoretic arguments do not apply to many of the most interesting classes -for instance, rooted connected frames, well-founded frames, finite rooted connected frames, finite transitive frames, finite equivalence frames - as these are not elementary. Instead we develop and extend the game-based analysis (first-order Ehrenfeucht-Fraisse versus bisimulation games) over such classes and provide bisimulation preserving model constructions within these classes.

Unions of conjunctive queries, also known as select-project-join-union queries, are the most frequently asked queries in relational database systems. These queries are definable by existential positive first-order formulas and are preserved under homomorphisms. A classical result of mathematical logic asserts that existential positive formulas are the only first-order formulas (up to logical equivalence) that are preserved under homomorphisms on all structures, finite and infinite. It is long-standing open problem in finite model theory, however, to determine whether the same homomorphism-preservation result holds in the finite, that is, whether every first-order formula preserved under homomorphisms on finite structures is logically equivalent to an existential positive formula on finite structures. In this paper, we show that the homomorphism-preservation theorem holds for several large classes of finite structures of interest in graph theory and database theory. Specifically, we show that this result holds for all classes of finite structures of bounded degree, all classes of finite structures of bounded treewidth, and, more generally, all classes of finite structures whose cores exclude at least one minor.

We consider an extension of modal logic with an operator for constructing inflationary fixed points, just as the modal μ-calculus extends basic modal logic with an operator for least fixed points. Least and inflationary fixed-point operators have been studied and compared in other contexts, particularly in finite model theory, where it is known that the logics IFP and LFP that result from adding such fixed-point operators to first-order logic have equal expressive power. As we show, the situation in modal logic is quite different, as the modal iteration calculus (MIC), we introduce has much greater expressive power than the μ-calculus. Greater expressive power comes at a cost: the calculus is algorithmically much less manageable.

The inductive operators nio (due to Arvind and Biswas) and c-ifp (due to Gire and Hoang) allow for a nondeterministic choice of tuples at each stage in the inductive construction of a relation. We consider the extensions of first-order logic with each of these operators, presenting a formal semantics for each, in which formulae denote sets of relations. We derive normal forms for these formulae and prove that the operators have equal expressive power. Finally, we show that, by using an appropriate notion of satisfaction for nondeterministic formulae, essentially any computational complexity class defined in terms of nondeterministic Turing machines operating within polynomial time bounds can be expressed in terms of nondeterministic fixed-point formulae.

Let Q be a finite set of generalized quantifiers. By L/sup k/(Q) we denote the k-variable fragment of FO(Q), first order logic extended with Q. We show that for each k, there is a PFP(Q)-definable linear pre-order whose equivalence classes in any finite structure 21 are the L/sup k/(Q)-types in 21. For some special classes of generalized quantifiers Q, we show that such an ordering of L/sup k/(Q)-types is already definable in IFP(Q). As applications of the above results, we prove some generalizations of the Abiteboul-Vianu theorem. For instance, we show that for any finite set Q of modular counting quantifiers, P=PSPACE if, and only if, IFP(Q)=PFP(Q) over finite structures. On the other hand, we show that an ordering of L/sup k/(Q)-types is not always definable in IFP(Q). Indeed, we construct a single, polynomial time computable quantifier P such that the equivalence relation /spl equiv//sup k,P/, and hence ordering on L/sup k/(P)-types, is not definable in IFP(P).

We study 0-1 laws for extensions of first-order logic by Lindstrom quantifiers. We state sufficient conditions on a quantifier Q expressing a graph property, for the logic FO[Q]-the extension of first-order logic by means of the quantifier Q-to have a 0-1 law. We use these conditions to show, in particular, that FO[Rig], where Rig is the quantifier expressing rigidity, has a 0-1 law. We also show that FO[Ham], where Ham is the quantifier expressing Hamiltonicity, does not have a 0-1 law. Blass and Harary pose the question whether there is a logic which is powerful enough to express Hamiltonicity or rigidity and which has a 0-1 law. It is a consequence of our results that there is no such regular logic (in the sense of abstract model theory) in the case of Hamiltonicity, but there is one in the case of rigidity. We also consider sequences of vectorized quantifiers, and show that the extensions of first-order logic obtained by adding such sequences generated by quantifiers that are closed under substructures have 0-1 laws.

The extensions of first-order logic with a least fixed point operator (FO + LFP) and with a partial fixed point operator (FO + PFP) are known to capture the complexity classes P and PSPACE respectively in the presence of an ordering relation over finite structures. Recently, Abiteboul and Vianu (in "Proceedings of the 23rd ACM Symposium on the Theory of Computing," 1991) investigated the relationship of these two logics in the absence of an ordering, using a machine model of generic computation. In particular, they showed that the two languages have equivalent expressive power if and only if P = PSPACE. These languages can also be seen as fragments of an infinitary logic where each formula has a bounded number of variables, Lω∞ω, (see, for instance, Kolaitis and Vardi, in "Proceedings of the 5th IEEE Symposium on Logic in Computer Science," pp. 156-167, 1990). We investigate this logic on finite structures and provide a normal form for it. We also present a treatment of Abiteboul and Vianu′s results from this point of view. In particular, we show that we can write a formula of FO + LFP that defines an ordering of the Lk∞ω, types uniformly over all finite structures. One consequence of this is a generalization of the equivalence of FO + LFP and P from ordered structures to classes of structures where every element is definable. We also settle a conjecture mentioned by Abiteboul and Vianu by showing that FO + LFP is properly contained in the polynomial time computable fragment of Lω∞ω, raising the question of whether the latter fragment is a recursively enumerable class.

We consider the problem of defining a logic that captures exactly the polynomial time computable properties of finite structures, by extending first-order logic (FO) and fixed-point logic (FP) by means of Lindstrom quantifiers. In particular,we define infinite uniform sequences of quantifiers and show that these correspond to a natural notion of logical reducibility. We show that if there is any logic that captures the complexity class PTTME, in the sense of a recursive enumeration of PTIME properties, then there is one that is an extension of FO by a uniform sequence of quantifiers. This is established through a general result linking the existence of complete problems for a complexity class to the existence of recursive index sets for the class, for a wide variety of complexity classes.

We consider extensions of first order logic (FO) and fixed [Bpoint logic (FP) by means of generalized quantifiers in the sense of P. Lindstrom (1966). We show that adding a finite set of such quantifiers to FP fails to capture PTIME, even over a fixed signature. We also prove a stronger version of this result for PSPACE, which enables us to establish a weak version of a conjecture formulated previously by Ph.G. Kolaitis and M.Y. Vardi (1992). These results are obtained by defining a notion of element type for bounded variable logics with finitely many generalized quantifiers. Using these, we characterize the classes of finite structures over which the infinitary logic L/sub /spl infin/wsup w/ extended by a finite set of generalized quantifiers Q and is no more expressive than first order logic extended by the quantifiers in Q.>

Feature structures are informational elements that have been used in several linguistic theories and in computational systems for natural-language processing. A logical calculus has been developed and used as a description language for feature structures. In the present work, a framework in three-valued logic is suggested for defining the semantics of a feature structure description language, allowing for a more complete set of logical operators. In particular, the semantics of the negation and implication operators are examined. Various proposed interpretations of negation and implication are compared within the suggested framework. One particular interpretation of the description language with a negation operator is described and its computational aspects studied.