Bounded Treewidth and the Infinite Core Chase – Complications and Workarounds toward Decidable Querying

Jean-François BagetJean-François Baget, Marie-Laure MugnierMarie-Laure Mugnier, Sebastian RudolphSebastian Rudolph

Jean-François Baget, Marie-Laure Mugnier, Sebastian Rudolph
Bounded Treewidth and the Infinite Core Chase – Complications and Workarounds toward Decidable Querying
In Floris Geerts, Hung Q. Ngo, Stavros Sintos, eds., Proceedings of the 42nd Symposium on Principles of Database Systems (PODS'23), 291-302, 2023. ACM

Details
Bibtex

KurzfassungAbstract
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 starts out from the – desirable and prima facie plausible – conjecture 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 conjectured 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.
Weitere Informationen unter:Further Information: Link
Projekt:Project: DeciGUT
Forschungsgruppe:Research Group: Computational LogicComputational Logic

@inproceedings{BMR2023,
  author    = {Jean-Fran{\c{c}}ois Baget and Marie-Laure Mugnier and Sebastian
               Rudolph},
  title     = {Bounded Treewidth and the Infinite Core Chase {\textendash}
               Complications and Workarounds toward Decidable Querying},
  editor    = {Floris Geerts and Hung Q. Ngo and Stavros Sintos},
  booktitle = {Proceedings of the 42nd Symposium on Principles of Database
               Systems (PODS'23)},
  publisher = {ACM},
  year      = {2023},
  pages     = {291-302},
  doi       = {10.1145/3584372.3588659}
}