Query entailment over ontologies is a fundamental decision problem in the field of knowledge representation and reasoning. The disjunctive (skolem) chase is a sound and complete reasoning procedure that solves this problem for boolean conjunctive queries over the powerful first-order logic fragment of disjunctive existential rules. Yet, termination of the procedure is an undecidable problem. We develop novel acyclicity and cyclicity notions for this procedure; that is, we develop suficient conditions to determine chase termination and non-termination. Our empirical evaluation on translated OWL ontologies shows that our novel notions are significantly more general than existing criteria.
We consider the problem of query entailment over ontologies, aka. knowledge bases (KBs) that are based on disjunctive existential rules. The latter form a very expressive fragment of ifrst-order logic. The problem can then be defined as follows: • Input: a set ℛ of rules, a set ℱ of facts, and a boolean conjunctive query (BCQ) . • Output: yes if is entailed by ⟨ℛ, ℱ ⟩ under standard first-order semantics.
The disjunctive skolem chase [
In this extended abstract, we briefly discuss our published paper [
We define Cons, Vars, Funs, and Preds to be mutually disjoint, finite (albeit large enough) sets of constants, variables, function symbols, and predicates, respectively, such that every ∈ Funs ∪ Preds has an arity ar() ≥ 1. The set Terms of terms includes Cons ∪ Vars and contains (1, . . . , ) for every ≥ 1, ∈ Funs with ar( ) = , and 1, . . . , ∈ Terms. A term is functional if ∈/ Cons ∪ Vars. We write lists 1, . . . , of terms as ⃗. A term is a subterm of a term if = , or is of the form (⃗) and is a subterm of some term in ⃗. A term is cyclic if it has a subterm of the form (⃗) such that ∈ Funs(⃗) where Funs(⃗) denotes the function symbols in ⃗. An atom is a first-order formula of the form (⃗) where is a |⃗|-ary predicate and ⃗ is a term list. A fact is a variable-free atom. For a formula , we write [⃗] to indicate that ⃗ is the set of all free variables in ; i.e., variables that are not explicitly quantified. Definition 1.
A (disjunctive existential) rule is a constant- and function-free formula of the form ∀⃗, ⃗.(︀ [⃗, ⃗] → ⋁︁ =1 ∃⃗. [⃗, ⃗]︀) (1) where ≥ 1; ⃗, ⃗, ⃗ are pairwise disjoint lists of variables; ⋃︀=1 ⃗ = ⃗; ⃗ are non-empty; and , are non-empty conjunctions of atoms (featuring exactly the denoted variables).
A rule as in (1) is deterministic if = 1, generating if it features at least one existential variable, and datalog if it is deterministic and not generating. We denote a skolemized rule (head) with sk( ) (sk( )), i.e. all existential variables are replaced by skolem terms.
A (boolean conjunctive) query is a first-order formula of the form ∃⃗. [⃗] with a non-empty conjunction of function-free atoms. A knowledge base (KB) is a pair ⟨ℛ, ℐ⟩ with ℛ a rule set and ℐ an instance; that is, a function-free fact set. A (ground) substitution is a partial function that maps variables to variable-free terms. We use [1/1, . . . , /] to denote the substitution that maps the variable to the term for every 1 ≤ ≤ . For a first-order formula , let be the formula that results from replacing every occurrence of every variable in the domain of in with (). A trigger is a pair ⟨, ⟩ with a rule as in (1) and a substitution with domain ⃗ ∪ ⃗. The trigger is loaded for a fact set ℱ if ⊆ ℱ ; it is active for ℱ if sk( ) ⊈ ℱ for all 1 ≤ ≤ . Let out( ) = sk( ) for 1 ≤ ≤ ; out( ) = {out( ) | 1 ≤ ≤ } be the output of . A fact set ℱ is closed under a rule if no trigger with is loaded and active for ℱ . Definition 2. A (skolem) chase tree (CT) of a KB ⟨ℛ, ℐ⟩ is a directed tree labelled with fact sets such that (1) the root label is ℐ; (2.1) for every non-leaf vertex , there is a trigger with a rule in ℛ that is loaded and active for the label of such that, for every ∈ out( ), some child of is labelled with ∪ ; (2.2) if features a non-datalog rule, then is closed under all datalog rules in ℛ; (3.1) leaf vertex labels are closed under the rules in ℛ; and (3.2) for a trigger with a rule in ℛ, there is a ≥ 1 such that is not loaded or not active for labels of vertices of depth at least .
Conditions (3.1) and (3.2) ensure fairness. A KB terminates if it only admits finite CTs. A
rule set ℛ terminates if every KB ⟨ℛ, ℐ⟩ terminates; it never-terminates if some KB ⟨ℛ, ℐ⟩ only
admits infinite CTs. It is undecidable to determine if ℛ terminates [
For detecting (never-)termination, we extend MFA [
Note that out1(⟨ ∧, ⟩) denotes the output of the first (and only) head-disjunct of ∧ with applied. Intuitively, MFA(ℛ) is an overapproximation of the facts in every possible CT of any KB with ℛ. Without cyclic terms, the number of terms and facts is finite so ℛ is terminating. MFA makes use of all triggers that are loaded without considering activeness. Indeed, deterministic triggers can always be considered active because of the following key property: Proposition 2 ([6, Lemma 15]). A deterministic trigger output occurs in a CT if it is loaded.
This holds because a loaded deterministic trigger is only not active if its exact output is already present, which is not true for disjunctive triggers. However, it is safe to ignore disjunctive triggers that are blocked [6, Definition 8], ensuring the following property [ 6, Lemma 7]: If a trigger is blocked for ℛ, then is not active whenever it is loaded in any CT of a KB with ℛ. Definition 4 ([6, Definitions 9,10]) . For a rule set ℛ, let DMFA(ℛ) be defined as MFA(ℛ) but only use of triggers that are not blocked. If no cyclic term occurs in DMFA(ℛ), then ℛ is DMFA. Theorem 1 ([6, Corollary 5, Theorem 10]). If a rule set ℛ is (D)MFA, then ℛ terminates. Example 1 ([6, Example 2]). The following rule set ℛ, which is a slightly simplified subset of rule set 00007.owl in the Oxford Ontology Repository OXFD (see Section 4), is DMFA but not MFA: (1) evidence() → ∃.Confidence(, ) (2) XRef(, ) → evidence() ∨ confidence() (3) Confidence(, ) → confidence() (4) Confidence(, ) → ∃.XRef(, ) Consider a KB ⟨ℛ, ℐ⟩ and suppose that = ⟨(2), [/(), /(())]⟩ is loaded in some CT of ⟨ℛ, ℐ⟩. Then, Confidence(, ()) occurs in since () may only be introduced via (1). Since datalog rules are prioritised (2.2 in Definition 2), confidence(()) is added by (3). But then, cannot be active, so is blocked! Hence, MFA(ℛ) features a cyclic term but DMFA(ℛ) does not.
For cyclicity, i.e. MFC membership of a rule set ℛ, we compute a fact set MFC(ℛ, ) for every generating rule ∈ ℛ. We can sometimes verify that can be applied infinitely many times when we start on the weakest instance to which this rule can be applied [6, Section 4.1]. MFC ignores disjunctive rules in the process and relies heavily on Proposition 2. To support disjunctive rules, a key aspect is to port the notion of unblockable triggers from RMFC, which ensure the property from Proposition 2 [6, Definition 17]. We obtain DMFC and prove its correctness [6, Definitions 19,20, Theorem 18]. Furthermore, checking DMFA or DMFC is 2ExpTime-complete and reasoning with DMFA rule sets is coN2ExpTime-complete [6, Theorems 12,13,19].
1–19 15 20–99 ER 100–999 O 1–999
1–19 LW 20–99 O 100–299 M 1–299 # tot. # fin.
We refine some introduced notions for the evaluation: We consider DMFA2, looking for cyclic terms of higher nesting depth, and DMFC; a simplified version of DMFC. We obtain the rule sets via normalization and translation of OWL ontologies [7, Section 6] from OXFD, ORE15, and MOWL.1 We drop OWL axioms that require equality (“at-most restrictions” and “nominals”). The tools, rule sets, and results of the evaluation are available online.2
We set a timeout of 30 minutes for each check and only consider rule sets for which all checks finished; we indicate the number of attempted (# tot.) vs finished (# fin.) rule sets. We group results by the number of generating rules (#∃). The percentage of finished rule sets that are fully classified by MFA and MFC for OXFD, ORE15, and MOWL are 70%, 58%, and 60%, respectively. With DMFA2 and DMFC, we achieve 97%, 99%, and 97%.
For future work, we would like to develop a normalisation procedure that preserves both query entailment and chase termination. As a long term goal, we would like to adapt our notions so they can be applied in other areas of knowledge representation and reasoning. For instance, we believe that we can use our ideas to (i) show if an ASP program with function symbols does or does not admit a finite solution or (ii) determine if DPLL(T) algorithms used in automated theorem proving will terminate or not for many real-world inputs.
Lukas is funded by DFG grant 389792660 (TRR 248), BMBF grant ITEA-01IS21084 (InnoSale), BMBF and DAAD grant 57616814 (SECAI), and the Center for Advancing Electronics Dresden (cfaed). David is funded by the ANR project CQFD (ANR-18-CE23-0003). 1https://www.cs.ox.ac.uk/isg/ontologies/ https://doi.org/10.5281/zenodo.18578 https://doi.org/10.5281/zenodo.16708 2https://doi.org/10.5281/zenodo.7375461