Leveraging Graph Complexity Measures to Ensure Decidability of First-Order Logic Reasoning

In this seminar, we will present generic model-theoretic criteria used to define decidable fragments of first-order logic; that is, fragments for which reasoning tasks such as satisfiability can be effective solved. These criteria are based on the existence of (possibly infinite) counter-models which, when viewed as labelled hypergraphs, satisfy some graph complexity metric such as treewidth or cliquewidth.

1. When and Where

2. Program

  • 9:30 to 10:00: "A Pitch Rich with Width-Witchcraft: Model-Theoretic Criteria for Decidable Query Entailment" by Sebastian Rudolph
    • Abstract: Decidability of inferencing is commonly considered a very important property of logic-based knowledge representation formalisms, required for the algorithmization and automation of reasoning. Yet, oftentimes, the corresponding (un)decidability arguments are idiosyncratic and do not shed much light on the underlying principles governing the divide. In my talk, I will review generic model-theoretic criteria for decidability of querying in fragments of first-order logic. I will describe a general framework by means of which decidability of query entailment can be established based on the existence of countermodels with certain structural properties. These properties depend on the ontology and query language used and range from finite domain over forest-like shape to width-finiteness employing width notions like treewidth and cliquewidth.
    • Bio: Sebastian Rudolph is a full professor for Computational Logic at the Institute for Artificial Intelligence at the Faculty of Computer Science at the Technische Universität Dresden. His research interests comprise Artificial Intelligence, in particular Knowledge Representation and Reasoning using diverse formalisms (such as Description Logics, Existential Rules and Formal Concept Analysis) and their applications in diverse areas, for instance Semantic Technologies. He investigates topics ranging from theoretical foundations (e.g., decidability and complexity of reasoning tasks) to practical deployment (ontology modeling, interactive knowledge acquisition). In 2017, he received an ERC Consolidator Grant for investigating general principles of decidability in logic-based knowledge representation.
  • 10:00 to 10:45: "Bounded Treewidth and the Infinite Core Chase: Complications and Workarounds toward Decidable Querying " by Jean-François Baget
    • Paper link
    • Abstract: The core chase, a popular algorithm for answering conjunctive queries (CQs) over existential rules, is guaranteed to terminate and compute a finite universal model whenever one exists, leading to the equivalence of the universal-model-based and the chase-based definitions of finite expansion sets (fes), a class of rulesets featuring decidable CQ entailment. In case of non-termination, however, it is non-trivial to define a "result" of the core chase, due to its non-monotonicity. This causes complications when dealing with advanced decidability criteria based on the existence of (universal) models of finite treewidth. For these, sufficient chase-based conditions have only been established for weaker, monotonic chase variants. This paper investigates the (prima facie plausible) hypothesis that the existence of a treewidth-bounded universal model and the existence of a treewidth-bounded core-chase sequence coincide, which would conveniently entail decidable CQ entailment whenever the latter holds. Perhaps surprisingly, carefully crafted examples show that both directions of this hypothesized correspondence fail. On a positive note, we are still able to define an aggregation scheme for the infinite core chase that preserves treewidth bounds and produces a finitely universal model, i.e., one that satisfies exactly the entailed CQs. This allows us to prove that the existence of a treewidth-bounded core-chase sequence does warrant decidability of CQ entailment (yet, on other grounds than expected). Hence, for the first time, we are able to define a chase-based notion of bounded treewidth sets of rules that subsumes fes.
    • Bio: Jean-François Baget is an Inria researcher, member of the Boreal team. He is interested in algorithms for rule-based knowledge representation languages.
  • 10:45 to 11:15: Coffee Break
  • 11:15 to 12:00: "Finite-Cliquewidth Sets of Existential Rules" by Thomas Feller
    • Paper link
    • Abstract: In our pursuit of generic criteria for decidable ontology-based querying, we introduce finite-cliquewidth sets (fcs) of existential rules, a model-theoretically defined class of rule sets, inspired by the clique-width measure from graph theory. By a generic argument, we show that fcs ensures decidability of entailment for a sizable class of queries (dubbed DaMSOQs) subsuming conjunctive queries (CQs). The fcs class properly generalizes the class of finite-expansion sets (fes), and for signatures of arity smaller than 2, the class of bounded-treewidth sets (bts). For higher arities, bts is only indirectly subsumed by fcs by means of reification. Despite the generality of fcs, we provide a rule set with decidable CQ entailment (by virtue of first-order-rewritability) that falls outside fcs, thus demonstrating the incomparability of fcs and the class of finite-unification sets (fus). In spite of this, we show that if we restrict ourselves to single-headed rule sets over signatures of arity smaller than 2, then fcs subsumes fus.
    • Bio: Since October 2018 I am a research assistent and doctoral student at the Institute for Artificial Intelligence in the Computational Logic group. My work revolves around general model theoretic characteristics of decidable knowledge representations in the context of the ERC project "DeciGUT". My academic background is a Master of Science in mathematics with emphasise on algebra and model theory. Since December 2018 i am also associated doctoral student at the research training group "QuantLA".
  • 12:00 to 12:30: "Shortcomings of cliquewidth, a brief introduction to partitionwidth, and their discussion in the FUS/BDD class context" by Piotr Ostropolski-Nalewaja
    • Abstract: This talk will serve as an example-based complement to the previous one. During it, we will discuss particular shortcomings of cliquewidth concerning treewidth and higher-than-binary arities. Later we will briefly introduce the notion of partitionwidth to address that problem. In the end, we will discuss cliquewidth-based measures in the context of existential rules and FUS/BDD class.
    • Bio: Piotr Ostropolski-Nalewaja recently started working as a researcher in the group of Prof. Sebastian Rudolph on the ERC project DeciGUT. Before that, Piotr was doing his PhD at the University of Wrocław, where he was (mainly) focusing on existential rules.

3. Contact

David Carral (david.carral@inria.fr)

4. Slides

We will upload the slides after the presentations.

5. Acknowledgements

The pause cafe was funded by the Inria research team Boreal : )