Chase-Based Computation of Cores for Existential Rules

Diplomarbeit von Lukas Gerlach

Betreuer Markus Krötzsch
Wissensbasierte Systeme
01. April 2021 – 29. August 2021
Download

The chase is a well studied sound and complete algorithm for computing universal models of knowledge bases that consist of an existential rule set and a set of facts. Since universal models can be used to solve generally undecidable reasoning tasks like BCQ entailment, it is no surprise that termination of the chase is undecidable as well. While conditions for termination and non-termination of variants like the skolem- or restricted-chase have been studied extensively, similar conditions for the core chase rarely exist. In practice, the core chase does not seem to be feasible. Still, compared to the other chase variants, the core chase not only yields a universal model but even a core, which intuitively is the smallest universal model that exists (up to isomorphism). Thus, the core chase terminates if and only if the given knowledge base has a finite universal model. In recent work, it has been shown that for rule sets that are “core-stratified”, the restricted chase also yields universal models that are cores if it terminates.

In our work, we strengthen the existing result and proof that restricted and core chase termination exactly coincide for core-stratified rule sets. This also implies that we can use sufficient conditions for restricted chase non-termination as sufficient conditions for the non-existence of finite universal models. We also find a new fragment of existential rules for which core chase termination is decidable based on an existing result that shows decidability of restricted chase termination for the same fragment and we conjecture that this even holds for a slightly larger fragment by generalizing the so-called Fairness Theorem, which is a key part of the decidability proof. For non-core-stratified rule sets, we investigate a possible heuristic for core computation and introduce the hybrid chase as a mixture of restricted and core chase as a new chase variant equivalent to the core chase.