Program
Click on the title to show/hide the abstract.Sunday 25
19:30—21:00 | 🍽 Dinner |
Monday 26
07:45—08:45 | ☕ Breakfast |
08:50 | Welcome & some information on the week |
09:00—10:00 |
Martin Grohe: Logic and the Power of Recurrent Graph Neural Networks invited talkGraph neural networks (GNNs) are deep learning models for
graph data that play a key role in machine learning on graphs. A GNN
describes a distributed algorithm carrying out local computations at
the vertices of the input graph. Typically, the parameters governing
this algorithm are acquired through a data-driven learning process. |
Long break (30 min) | |
10:30—11:30 |
Harry Vinall-Smeeth: Unambiguity Makes Context Free Grammars BigA context free grammar (CFG) is unambiguous if each word has a unique derivation. This property can be useful algorithmically, particularly in the
case where the grammar represents a finite language. But do we have to pay a cost for this extra algorithmic power? In this talk, we answer this question with a
resounding yes: for finite languages, representations by general CFGs can be doubly-exponentially smaller than those by unambiguous CFGs. The talk will focus on the
mysterious nature of unambiguous models of computation, how we overcame these difficulties and some promising directions for future research. The talk is based on
joint work with Stefan Mengel [1], which will be presented at PODS 2025. Sophie Brinke: Semiring Semantics: Algebraic Properties vs. Logical ResultsSemiring provenance was originally introduced in database theory with the aim of explaining why certain tuples are (not) contained in the answer of a query — to explain their provenance. To this end, logical statements are not just evaluated to true or false but by values from a commutative semiring. This allows us to track which combinations of atomic facts are responsible for the truth of a statement and to derive practical information about costs, access levels, or confidence scores. Recently, this approach has been expanded to a systematic study of semiring semantics for first-order logic and other logical systems. This talk gives an overview of the recent results on the generalisation of model-theoretic properties and methods such as compactness, Ehrenfeucht-Fraïssé games, or locality beyond the Boolean semiring. Many model-theoretic notions admit natural generalisations to the semiring framework (e.g. entailments can be understood as inequalities of semiring valuations) while even simple properties lead to surprisingly difficult questions that require new proof techniques. It turns out that most of the classical logical results and methods can be generalised to some semirings but fail for others. We shall discuss how this is related to algebraic properties of the underlying semirings such as idempotence and absorption. Christoph Berkholz: Succinct representations for join query evaluationIn this talk I will discuss how to represent the result of a multi-way
join in a succinct way and how these data structures can be used to
support efficient postprocessing such as counting or enumeration tasks.
The representation formats we consider are known as factorised databases
in the database(theory) literature and are closely connected to variants
of DNNF-circuits from knowledge compilation.
The main theme of this talk is to present structural characterisations
of those input instances where small representations are possible and to
provide matching lower bounds.
The talk is based on the recent joint work [1] with Harry Vinall-Smeeth |
Short break (10 min) | |
11:40—12:20 |
Jerzy Marcinkowski: What we can show about the multiset-semantics conjunctive query containmentDecidability, and complexity, of multiset-semantics
conjunctive query containment is
one of the most fascinating and most frustrating open problems in
database theory.
It has been studied for over 30 years now, and no major progress has
been achieved. Thomas Zeume: Learning Formal Foundations of Computer Science with IltisIntroductory courses in the formal foundations of computer science are
often attended by large numbers of students from diverse backgrounds. In
this talk, I will outline how this challenge can be addressed using
web-based, interactive exercises provided by Iltis
(https://iltis.rub.de/), a modern educational support system covering
the foundations of logic, formal languages, and (parts of) complexity
theory. I will give a brief introduction to Iltis and outline the
research challenges and opportunities for theoretical computer science
that arise in the development of such a system. |
12:30—14:30 | 🍽 Lunch |
14:30—15:30 |
Michał Pilipczuk: Logic through the lens of structural graph theory invited tutorialFor a pair of classes of graphs C and D, we say D can be transduced from C if every graph from D can be interpreted in some vertex-colored graph from C using a fixed one-dimensional First-Order interpretation. Transducibility provides a quasi-order on graph classes that naturally stratifies them with respect to their First-Order "complexity" or "expressive power". The goal of the talk is to give a broad overview of a recent line of advances in constructing a logically-motivated structure theory for dense graphs by setting transductions as the cornerstone definition. We will particularly focus on monadically dependent classes — those that do not transduce the class of all graphs — and monadically stable classes — those that do not transduce the class of all total orders. Also, we will discuss analogies between the constructed theory and the classic structure theory for sparse graphs. |
Long break (30 min) | |
16:00—16:40 |
Patrice Ossona de Mendez: Characterization of stability by quasibounded-size bounded-shrubdepth decompositionsThe notions of bounded-size and quasibounded-size decompositions with bounded treedepth base classes are central to the structural theory of graph
sparsity introduced some years ago, and provide a characterization of both classes with bounded expansions and nowhere dense classes. Strong connections of this
theory with model theory led to considering first-order transductions, which are logically defined graph transformations, and to initiate a comparative study of
combinatorial and model theoretical properties of graph classes, with an emphasis on the model theoretical notions of dependence (or NIP) and
stability. Szymon Toruńczyk: Merge-width and First-Order Model CheckingWe introduce merge-width, a family of graph parameters that unifies
several structural graph measures, including treewidth, degeneracy,
twin-width, clique-width, and generalized coloring numbers. Our
parameters are based on new decompositions called construction
sequences. These are sequences of ever coarser partitions of the vertex
set, where each pair of parts has a specified default connection, and
all vertex pairs of the graph that differ from the default are marked as
resolved. The radius-r merge-width is the maximum number of parts
reached from a vertex by following a path of at most r resolved edges.
Graph classes of bounded merge-width — for which the radius-r
merge-width parameter can be bounded by a constant, for each fixed
r=1,2,3,… — include all classes of bounded expansion or of bounded
twin-width, thus unifying two central notions from the Sparsity and
Twin-width frameworks. Furthermore, they are preserved under first-order
transductions, which attests to their robustness. We conjecture that
classes of bounded merge-width are equivalent to the previously
introduced classes of bounded flip-width. |
Break (10 min) | |
16:50—18:00 | Open Problem Session |
19:00—19:30 | 🍹 Welcome cocktail |
19:30—21:00 | 🍽 Dinner |
Tuesday 27
07:45—08:45 | ☕ Breakfast |
09:00—10:00 |
Anuj Dawar: Games and Symmetric Circuits invited tutorialThe connection between logical definability and circuit complexity, particularly the tight connection between fixed-point logic with counting and polynomially-uniform symmetric circuits, has highlighted the potential use of pebble games in proving circuit lower bounds. In this tutorial talk, I review the connection between games and circuits with a focus on symmetric algebraic circuits. I end with pointers on current and future directions. |
Long break (30 min) | |
10:30—11:30 |
Anatole Dahan: Representations of permutation groups in Fixed-point logicI’ll discuss how finite permutation groups can be represented in a logical context, and why this matters for capturing PTIME. While permutation groups have been key to recent progress in efficient algorithms for Graph Isomorphism and Graph Canonization, our ability to represent them concisely often relies on a linear order. In particular, we will see that some computable permutation groups do not admit small symmetric generating sets. In a second time, we will exhibit some structural assumptions under which this issue can be circumvented. Isolde Adler: Some recent advances in logic and graph property testingProperty testing (for a property P) asks for a given graph, whether it has
property P, or is "structurally far" from having that property. A "testing
algorithm" is a probabilistic algorithm that answers this question with high
probability correctly, by only looking at small parts of the input. Testing
algorithms are thought of as "extremely efficient", making them relevant in
the context of large data sets. Benjamin Rossman: Equirank Homomorphism Preservation Theorem on Finite StructuresThe Homomorphism Preservation Theorem (HPT) states that a first-order sentence is preserved under homomorphisms iff it is equivalent to an existential-positive sentence. The classical compactness proof of the HPT, however, (i) yields no computable upper bound on the quantifier rank of the equivalent existential-positive sentence, and (ii) fails to relativize to non-elementary classes such as the finite structures. Previous work by the author [R’08] addressed these drawbacks separately, proving an Equirank HPT (with no blow-up in quantifier rank) and a Finitary HPT (valid over finite structures, but with a large blow-up). In this work we unify the two results by establishing an Equirank Finitary HPT: over finite structures, every homomorphism-preserved sentence is equivalent to an existential-positive sentence with the same quantifier rank. The proof combines the Finitary HPT of [R.08] with an application of the Cai–Furer–Immerman construction to the minimal cores of a homomorphism-preserved sentence’s model class. Paper available at https://users.cs.duke.edu/~br148/equirank-hpt.pdf |
Short break (10 min) | |
11:40—12:20 |
Colin Geniet: Stability under first-order transduction for variants of twin-widthTwin-width is a graph complexity parameter primarily motivated by model
checking algorithms for first-order logic. Bounded twin-width is also
preserved by first-order transduction.
This talk gives a new simple presentation of this proof of stability
under transduction. It only uses a standard statement of Gaifman's
locality, a variant of the definition of twin-width involving rank, and
some elementary logical tools.
With this point of view, it becomes easy to observe that the same proof
also applies to a class of restrictions of twin-width, such as the
so-called reduced bandwidth. Steffen van Bergerem: Evaluation of First-Order Logic with Counting on Sparse ClassesNowhere dense classes of relational structures are the largest family of sparse classes with a tractable model-checking problem for first-order logic. We study the model-checking and term-evaluation problem for fragments of first-order logic with counting (FOC). Prior work by Grohe and Schweikardt shows that these two problems are fixed-parameter tractable for the fragment FOC1 of FOC on nowhere dense classes, while for the full logic FOC, they are already AW[*]-hard for the class of unranked trees. In this talk, I introduce guarded fragments of FOC that extend FOC1, and I characterise the dividing line of tractability on nowhere dense classes with respect to the expressivity of these fragments. |
12:30—14:30 | 🍽 Lunch |
14:30—15:30 |
Maryanthe Malliaris: New perspectives on model-theoretic complexity invited talkPart of the power of model-theoretic dividing lines comes from having many different equivalent definitions. The talk will discuss several recent theorems in which certain (infinite) model theoretic dividing lines appear inherently in combinatorics and computer science, and consider what this means from different sides. |
Long break (30 min) | |
16:00—17:00 |
Samuel Braunfeld: Limits of sequences of finite structures from monadically stable classesIn search of a notion of graph limit for sequences of sparse graphs, Nešetřil and Ossona de Mendez introduced first-order convergence for sequences of finite structures (requiring that for every formula, the probability that it is satisfied by a tuple chosen uniformly at random converges) and corresponding analytic limit objects called modeling limits. A modeling limit is a Borel structure, i.e. its domain is a standard Borel space and every parameter-definable relation is Borel, equipped with a probability measure assigning the appropriate limiting value to definable relations. We show that a modeling limit can be constructed for any convergent sequence of finite structures from a monadically stable class. Joint work with Jarik Nešetřil and Patrice Ossona de Mendez. Ioannis Eleftheriadis: Separability properties of monadically dependent graph classesA graph class C is monadically dependent if one cannot interpret all graphs in coloured graphs from C using a fixed first-order interpretation; this property originates from classical model theory and is conjectured to delimit the tractability of the first-order model checking problem over hereditary classes. Here, we prove a novel characterisation of monadically dependent graph classes in terms flip-separability, a combinatorial property that ensures that local vicinities of graphs coming from this class can be made small after applying a bounded number of flips, i.e. complementations of the adjacency relation on a subset of vertices. Towards this, we introduce a robust toolbox for working with various notions of local separations in monadically dependent classes. This is joint work with Édouard Bonnet, Sam Braunfeld, Colin Genniet, Nikolas Mählmann, Michał Pilipczuk, Wojciech Przybyszewski, and Szymon Toruńczyk. Pablo Barceló: Separating Automatic RelationsWe study the separability problem for automatic relations (i.e., relations on finite words definable by synchronous automata) in terms of
recognizable relations (i.e., finite unions of products of regular languages). This problem takes as input two automatic relations R and R', and asks if there
exists a recognizable relation S that contains R and does not intersect R'. We show this problem to be undecidable when the number of products allowed in the
recognizable relation is fixed. In particular, checking if there exists a recognizable relation S with at most k products of regular languages that separates R from
R' is undecidable, for each fixed k > 1. Our work reveal tight connections, of independent interest, between the separability problem and the finite coloring
problem for automatic graphs, where colors are regular languages. |
17:01 | 📷 Group photo |
19:30—21:00 | 🍽 Dinner |
Wednesday 28
07:45—08:45 | ☕ Breakfast |
09:00—10:00 |
Antoine Mottet: State of the art in infinite-domain constraint satisfaction invited tutorialThe complexity of all constraint satisfaction problems with finite templates is by now well understood, but most CSPs cannot be expressed with a finite template. In this tutorial, we will see what is the current state of the field of infinite-domain constraint satisfaction with an emphasis on particular classes of templates for which a “big picture” started to emerge in the recent years. |
Long break (30 min) | |
10:30—11:30 |
Santiago Guzmán Pro: Hereditary First-Order Logic and Extensional ESOWe consider two families of computational problems. The first ones are de-
scribed by a fixed first-order sentence φ, and given an input structure A the task is to Moritz Lichter: Limitations of Affine Relaxations for CSPs via Finite Model Theory and Graph IsomorphismConstraint satisfaction problems (CSPs) provide a universal framework that covers many different computational problems, for example, boolean satisfiability, solving system of equations, or graph coloring. CSPs satisfy a dichotomy: a CSP is tractable, that is, polynomial-time solvable, or NP-complete. For the tractable case, multiple algorithms based on affine relaxations of an integer linear formulation of CSPs were proposed. This line of research has two goals: understanding the power of the affine relaxations and finding a universal algorithm - an algorithm that uniformly solves all tractable CSPs in polynomial time. This talks presents how techniques and constructions from finite model theory and the graph isomorphism problem show limitations of the affine approach: neither Z-affine k-consistency, BLP+AIP, every fixed level of the BA^k-hierarchy, nor the CLAP algorithm solve all polynomial-time CSPs. This answers open problems of Brakensiek, Guruswami, Wrochna, and Živný (ECCC 2020) and of Dalmau and Opršal (LICS 2024). The talk is based in joint work with Benedikt Pago. Albert Atserias: On Certifying the Chromatic Number of Sparse Random GraphsA simple first-moment calculation shows that for every number of colors q there is a d = d(q) = O(q.log(q)) such that a sparse random graph G(n,d/n) is asymptotically almost surely non-q-colorable. The argument is famously non-constructive in that it fails to provide any easily-checkable certificate for non-q-colorability that applies with asymptotic, not even positive, probability. Motivated by the on-going project of isolating what makes hard instances of the constraint satisfaction problem hard, in this talk I will give a brief overview of the status of the question whether there exist logic-based or algebra-based tests of non-q-colorability that are effective for sparse random graphs. |
Short break (10 min) | |
11:40—12:20 |
Jakub Opršal: A topological proof of the H-colouring dichotomyAs it is well-known, the existence of a colouring of a given graph with $2$ colours can be decided in polynomial-time, and colouring with $k > 2$ colours is NP-complete. In a seminal paper, Hell and Nešetřil [1990] extended this dichotomy to a more general *graph homomorphism problem*, also called the $H$-colouring problem. More precisely, they proved that deciding whether there is a graph homomorphism from a given graph to a fixed graph $H$ is in P if $H$ is bipartite (or contains a self-loop), and is NP-complete otherwise. This dichotomy served as an important test case for the Feder–Vardi dichotomy conjecture, and Bulatov–Zhuk dichotomy of complexity of finite-template CSPs. I will present a new proof of the Hell–Nešetřil theorem using tools from topological combinatorics based on ideas of Lovász [1978] and Brower’s fixed-point theorem. This is joint work with Sebastian Meyer (TU Dresden). Jaroslav Nešetřil: On orderingsStructures which have a linear ordering of their vertices with given local properties have a rich spectrum of complexities. Some have full power of class NP (and thus no dichotomy) but for biconnected patterns we get dichotomy. This also displays the importance of Sparse Incomparability Lemma. This is a joint work with Gabor Kun (Budapest). |
12:30—14:30 | 🍽 Lunch |
14:30—15:30 |
Dan Suciu: The Fine Grained Data Complexity of Conjunctive Query Evaluation invited talkThe conjunctive query evaluation problem asks whether there exists a homomorphism between two structures, Q -> D, where Q is called the
"query"
and D is the "database". In data complexity, the query is fixed and the complexity is a function of the database. Variations of this problem include:
enumerating
all homomorphisms or counting the number of homomorphisms. This talk is a brief survey of recent results on the fine-grained data complexity of conjunctive query
evaluation. |
Long break (30 min) | |
16:00—17:00 |
Antoine Amarilli: Edge-Minimum Walks for RPQsWe consider regular path queries (RPQs) on graph databases, i.e., fixing
an alphabet Σ, a graph database D is a graph with edges labeled by
elements of Σ, and a RPQ Q is simply a regular expression over Σ. For
two vertices s and t, a match of Q on D is an st-walk in D where the
edge labels form a word of Q. We study the problem of computing
*edge-minimum walks*, i.e,. for a fixed query Q, given a graph database
D, we want to compute a match of Q in D that uses a minimum number of
*distinct* edges. Equivalently, we want to compute a minimum-cardinality
subset D' of D which contains a Q-match. Wim Martens: Rel: Programming in the Large with DataFrom the moment of their inception, languages for relational data have been described as sublanguages embedded in a host programming language. Rel is a new relational language whose key design goal is to go beyond this paradigm with features that allow for programming in the large, making it possible to fully describe end to end application semantics. With the new approach we can model the semantics of entire enterprise applications relationally, which helps significantly reduce architecture complexity and avoid the well-known impedance mismatch problem. This paradigm shift is enabled by 50 years of database research, making it possible to revisit the sublanguage/host language paradigm, starting from the fundamental principles. We present the main features of Rel: those that give it the power to express traditional query language operations and those that are designed to grow the language and allow programming in the large. Rémi Morvan: Minimizing Conjunctive Regular Path QueriesWe study the minimization problem for Conjunctive Regular Path Queries (CRPQs) and unions of CRPQs (UCRPQs). This is the problem of checking, given a query and a number k, whether the query is equivalent to one of size at most k. For CRPQs we consider the size to be the number of atoms, and for UCRPQs the maximum number of atoms in a CRPQ therein, motivated by the fact that the number of atoms has a leading influence on the cost of query evaluation. We show that the minimization problem is decidable, both for CRPQs and UCRPQs. This is joint work with Diego Figueira and Miguel Romero. |
19:30—21:00 | 🍽 Dinner |
Thursday 29
07:45—08:45 | ☕ Breakfast |
09:00—10:00 |
Tim Seppelt: Homomorphism Indistinguishability: Theory and Applications invited tutorialIn 1967, Lovász proved that two graphs G and H are isomorphic if, and only if, they are homomorphism indistinguishable over the the family of all
graphs, i.e. for all graphs F the number of homomorphisms from F to G is equal to the number of homomorphisms from F to H. In recent years, many natural relaxations
of graph isomorphism from fields as diverse as quantum information theory, algebraic graph theory, convex optimisation, and category theory have been characterised
as homomorphism indistinguishability relations over restricted graph classes. |
Long break (30 min) | |
10:30—11:30 |
Nina Runde: The Complexity of Homomorphism ReconstructibilityRepresenting graphs by their homomorphism counts has led to the beautiful theory of homomorphism indistinguishability in recent years. Moreover,
homomorphism counts have promising applications in database theory and machine learning, where one would like to answer queries or classify graphs solely based on
the representation of a graph G as a finite vector of homomorphism counts from some fixed finite set of graphs to G. We study the computational complexity of the
arguably most fundamental computational problem associated to these representations, the homomorphism reconstructibility problem: given a finite sequence of graphs
and a corresponding vector of natural numbers, decide whether there exists a graph G that realises the given vector as the homomorphism counts from the given
graphs. Eva Fluck: Monotonicity of cops-and-robber-gamesWe study variations of the cops-and-robber-game regarding the following question: If the cop-player has a winning strategy, do they also have a
winning strategy that is cop- or robber-monotone? We say the respective variant is cop- or robber-monotone. Here cop-monotonicity denotes that the cop-player is
never allowed to move to a position that they previously left and robber-monotonicity denotes that the robber-player can never move to a vertex that was previously
occupied by the cops. In the well-known cops-and-robber-game as defined by Seymour and Thomas (1993) these notions coincide. Balder ten Cate: Adaptive Query Algorithms for Relational Structures Based on Homomorphism CountsA query algorithm based on homomorphism counts is a procedure to decide membership for a class of finite relational structures using only
homomorphism count queries. A left query algorithm can ask the number of homomorphisms from any structure to the input structure and a right query algorithm can ask
the number of homomorphisms from the input structure to any other structure. We systematically compare the expressive power of different types of left or right
query algorithms, including non-adaptive query algorithms, adaptive query algorithms that can ask a bounded number of queries, and adaptive query algorithms that
can ask an unbounded number of queries. We also consider query algorithms where the homomorphism counting is done over the Boolean semiring, meaning that only the
existence of a homomorphism is recorded, not the precise number of them. |
Short break (10 min) | |
11:40—12:20 |
Benedikt Pago: Symmetric algebraic circuits and homomorphism polynomialsAlgebraic complexity studies families of polynomials in terms of the size of the smallest algebraic circuits representing them. We study the restriction to symmetric polynomials and symmetric cicuits because it allows to prove strong lower bounds that are out of reach in the general setting: For example, exponential lower bounds on the symmetric circuit complexity of the permanent were shown by Dawar and Wilsenach (2020). 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 efficient symmetric circuits if and only if they can be written as linear combinations of homomorphism counting polynomials of graphs of bounded treewidth. We also establish a relationship between the symmetric complexity of subgraph counting and the vertex cover number. Finally, we examine the symmetric complexity of immanant families (a generalisation of the determinant and permanent) and show that a known conditional complexity dichotomy due to Curticapean (2021) holds unconditionally in the symmetric setting. Joint work with Anuj Dawar and Tim Seppelt. Aliaume Lopez: Well-Quasi-Orders and Logic on GraphsIn this talk I will give a survey on the results and conjectures on classes of graphs that are (labelled) well-quasi-ordered by the induced subgraph relation. I will discuss how this seemingly purely combinatorial property is deeply connected to logic and structural decompositions of graphs. Starting from the early results of Ding regarding bounded tree-depth, we will explore classes of bounded clique-width, monadically stable classes, monadically dependent classes, and state various conjectures, old and new. The goal of this talk is to give an overview of the questions of interest and is targeted as a broad “Finite and algorithmic model theory” audience. |
12:30—14:30 | 🍽 Lunch |
Free (see Excursion for ideas) | |
19:30—21:00 | 🍽 Dinner |
Friday 30
07:45—08:45 | ☕ Breakfast |
09:00—10:00 |
Mikołaj Bojańczyk: Deciding equivalence for first-order interpretations invited talkFirst-order interpretations are a formalism of defining functions from structures to structures. The idea is that elements of the output structure are represented by k-tuples of elements in the input structure, and the relations of the output structure are defined using first-order logic. In this talk, I will discuss the equivalence problem for such interpretations. This is a problem that is parameterised by two classes of structures C and D. We are given two first-order interpretations that define functions C -> D, and we want to know if they are equivalent, i.e. for every input structure in C, the two output structures in D are isomorphic. I will show that this problem is decidable if both C and D are classes of graphs of bounded tree-depth (joint work with Bartek Klin). I will also place this result in the context of a wider research programme, which considers classes of structures such as strings, or graphs of bounded treewidth. |
Long break (30 min) | |
10:30—11:30 |
Thomas Colcombet: String-to-string MSO-set-interpretationsMSO-set-interpretations are variants of standard logical MSO-interpretations that transform logical structures into logical structures, with the
particularity that the elements of the output structure are sets of elements of the original one. It can for instance transform a linear order of length n into a
linear order of length 2^n by lexicographically ordering its subsets. A straightforward property of this notion is that the inverse image of an FO-definable
property is effectively an MSO-definable property, and can be used for describing the various form of automatic structures [C., Löding
07]. Bartosz Bednarczyk: Guarded Fragments Meet Dynamic Logic: The Story of Regular GuardsWe study the Guarded Fragment with Regular Guards (RGF), which combines the expressive power of the Guarded Fragment (GF) with Propositional Dynamic Logic with Intersection and Converse (ICPDL). Our logic generalizes, in a uniform way, many previously-studied extensions of GF, including (conjunctions of) transitive or equivalence guards, transitive or equivalence closure and more. We prove 2ExpTime-completeness of the satisfiability problem for RGF, showing that RGF is not harder than ICPDL or GF. Shifting to the query entailment problem, we provide undecidability results that significantly strengthen and solidify earlier results along those lines. We conclude by identifying, in a natural sense, the maximal ExpSpace-complete fragment of RGF. David Carral: Expressibility vs Rewritability in Ontology Based Query AnsweringWe consider the problem of checking whether a Boolean conjunctive query (BCQ) is a logical consequence of a knowledge base (KB), which in our context is a pair (R, F) where R and F are finite sets of existential rules and facts. We can sometimes tackle this problem via rewriting into a union of BCQs: given an (existential) rule query (R, q) consisting of a rule set R and a BCQ q, we compute a UBCQ qR such that, for every fact set F, the KB (R, F) entails q if and only if F entails qR. In fact, a uniform procedure exists for computing these rewritings, with guaranteed termination for any input rule query that can be expressed as a UBCQ. This naturally raises the question: can we design a uniform rewriting procedure with similar termination guarantees for more expressive target languages, such as Datalog? What about fragments of this well-known KR language, such as linear or monadic Datalog? Unfortunately, we show that no such terminating uniform procedure exists for either of these languages. |
Short break (10 min) | |
11:40—12:20 |
Erich Grädel: Semiring Semantics in the InfiniteSemiring semantics evaluates database queries or logical statements not just by true or false but by values in some commutative semiring.
This permits to track which combinations of atomic facts are responsible for the truth of a statement, and to derive further
information, for instance concerning costs, confidence scores, number of successful evaluation strategies, or access levels to protected data.
The focus of this approach has originally been on the provenance analysis for positive database query languages, but has later been extended
to a systematic semiring semantics for first-order logic and other logical systems, as well as to a method for the strategy analysis of
games. Wojciech Przybyszewski: Low rank MSOWe introduce a new logic for describing properties of graphs, which is called low rank MSO. This is the fragment of monadic second-order logic (MSO), in which set quantification is restricted to sets of bounded rank. We prove that over any class of graphs that is weakly sparse, low rank logic has the same expressive power as separator logic, which is another extension of first-order order logic that can talk about non-local behavior such as connectivity. We also compare the expressive power of low rank MSO with variants of separator logic that involve flips. This is joint work with Mikołaj Bojańczyk, Michał Pilipczuk, Marek Sokołowski, and Giannos Stamoulis. |
12:30—14:30 | 🍽 Lunch |