A General Sufficient Condition for Rewriting $\textit{Horn-}\mathcal{ALCHI}$ Atomic Queries into GQL

We focus on rule queries with unary facts such as the one in the previous example, with rules expressed in the positive fragment of $\textit{Horn-}\mathcal{ALCHI}$ DL, defined in Section˜2. We show that these rules can be normalised into Datalog ones, in Section˜3. We then identify a large class of rule queries that can be rewritten into GQL; we proceed in two main steps. First, in Section˜4, we turn our rule queries into equivalent automata of a new form, closely related to the usual tree automata and which we refer to as DL automata. Second, in Section˜5, we identify a class of DL automata that can be rewritten into positive two-way regular path queries (PQs), and thus into UC2RPQs which in turn fall within GQL (Section˜6). Our criteria for rewritability relies on the existence of a stratification of the DL automata, which forbids some (but not all!) cyclic dependencies within its transition function. Interestingly, rule queries based upon the DL-Lite family trivially enjoy stratified automata, and thus the class we pinpoint extends DL-Lite. Additionally, our class guarantees the rewritability of rule queries that were not covered by prior attempts at rewriting into GQL [18], such as the one from Example˜2. Section˜7 elaborates further on related work; we discuss our conclusions and future work in Section˜8. This extended version of a paper to appear at ISWC 2026 contains proofs for all results in the appendix.

We fix pairwise disjoint, countably infinite sets $\mathsf{Classes}$, $\mathsf{Roles}$, $\mathsf{Cons}$, and $\mathsf{Vars}$ of unary predicates, binary predicates, constants, and variables respectively. We often refer to unary and binary predicates as classes and roles, respectively. An inverse role is an element of $\mathsf{InvRoles}=\{\mathtt{R}^{-}\mid\mathtt{R}\in\mathsf{Roles}\}$. A role expression is an element of $\mathsf{RoleExps}=\mathsf{Roles}\cup\mathsf{InvRoles}$. A term is an element of $\mathsf{Terms}=\mathsf{Cons}\cup\mathsf{Vars}$. Lists of terms $t_{1},\ldots,t_{n}$ are written as $\vec{t}$ and are often treated as sets.

A class atom is a formula of the form $\mathtt{C}(t)$ with $\mathtt{C}\in\mathsf{Classes}$ and $t\in\mathsf{Terms}$. A role atom is a formula of the form $\mathtt{R}(t,u)$ with $\mathtt{R}\in\mathsf{Roles}$ and $t,u\in\mathsf{Terms}$. A FO atom is either a class atom or a role atom. Class facts, role facts, and FO facts are variable-free class atoms, role atoms, and FO atoms, respectively.

For an FO formula $\psi$ and a list $\vec{x}$ of variables, we write $\psi[\vec{x}]$ to indicate that $\vec{x}$ is the set of all free variables in $\psi$. An (existential) rule $\varrho$ is a FO sentence of the form $\forall\vec{x},\vec{y}.\big(\beta[\vec{x}]\rightarrow\exists\vec{z}.\eta[\vec{y},\vec{z}]\big)$ where $\vec{x}$, $\vec{y}$, and $\vec{z}$ are lists of variables such that $(\vec{x}\cup\vec{y})\cap\vec{z}=\emptyset$, and $\beta$ and $\eta$ are conjunctions of FO atoms with $\eta\neq\emptyset$.

The rule $\varrho$ is Datalog if $\vec{z}$ is the empty list. We refer to $\beta$ and $\exists\vec{z}.\eta$ as the body and the head of $\varrho$, respectively. When discussing rules, we omit universal quantifiers and often identify conjunctions of atoms such as $\beta$ and $\eta$ above with the corresponding set. We allow rules to contain unsafe variables–universally quantified variables that appear in the head but not in the body of the rule. A knowledge base (KB) is a pair consisting of a finite rule set and a finite fact set.

A (positive) $\textit{Horn-}\mathcal{ALCHI}$ rule is one of the following rules:

	$\displaystyle\mathtt{A}_{1}(x)\wedge\ldots\wedge\mathtt{A}_{n}(x)$	$\displaystyle\to\mathtt{B}(x)$	$\displaystyle\mathtt{A}_{1}\sqcap\ldots\sqcap\mathtt{A}_{n}$	$\displaystyle\sqsubseteq\mathtt{B}$		(1)
	$\displaystyle\mathtt{R}(x,y)\wedge\mathtt{A}(y)$	$\displaystyle\to\mathtt{B}(x)$	$\displaystyle\exists\mathtt{R}.\mathtt{A}$	$\displaystyle\sqsubseteq\mathtt{B}$		(2)
	$\displaystyle\mathtt{A}(x)\wedge\mathtt{R}(x,y)$	$\displaystyle\to\mathtt{B}(y)$	$\displaystyle\mathtt{A}$	$\displaystyle\sqsubseteq\forall\mathtt{R}.\mathtt{B}$		(3)
		$\displaystyle\to\mathtt{B}(x)$	$\displaystyle\top$	$\displaystyle\sqsubseteq\mathtt{B}$		(4)
	$\displaystyle\mathtt{A}(x)$	$\displaystyle\to\exists y.\mathtt{R}(x,y)\wedge\mathtt{B}(y)$	$\displaystyle\mathtt{A}$	$\displaystyle\sqsubseteq\exists\mathtt{R}.\mathtt{B}$		(5)
	$\displaystyle\mathtt{R}(x,y)$	$\displaystyle\to\mathtt{S}(x,y)$	$\displaystyle\mathtt{R}$	$\displaystyle\sqsubseteq\mathtt{S}$		(6)
	$\displaystyle\mathtt{R}(y,x)$	$\displaystyle\to\mathtt{S}(x,y)$	$\displaystyle\mathtt{R}^{-}$	$\displaystyle\sqsubseteq\mathtt{S}$		(7)

Here, $\mathtt{A}$, $\mathtt{B}$, and $\mathtt{C}$ are classes, and $\mathtt{R}$ and $\mathtt{S}$ are roles. We restrict ourselves to the positive fragment of $\textit{Horn-}\mathcal{ALCHI}$, in which the bottom class $\bot$ is not allowed; in Section˜8, we discuss how our rewriting techniques could be adapted to handle this class. We consider $\textit{Horn-}\mathcal{ALCHI}$ rules in a restricted normal form, which is without loss of generality [16]. The right-hand side shows the corresponding Description Logic syntax, included for reference only and not used further in this paper. We adopt the rule-based presentation because rules are FO logic formulas and are therefore accessible to a wider audience, and because this syntax allows us to define fact entailment for $\textit{Horn-}\mathcal{ALCHI}$ naturally via the well-known chase procedure, which we briefly present below. We consider entailment under active domain semantics as discussed later, and hence rules of type (4) are not domain-dependent. A $\textit{Horn-}\mathcal{ALCHI}$ KB is a KB whose rule set is $\textit{Horn-}\mathcal{ALCHI}$.

In this paper, a rule query is a pair consisting of a finite rule set and a class fact. A Datalog query is a rule query whose rule set is Datalog. A $\textit{Horn-}\mathcal{ALCHI}$ query is a rule query whose rule set is $\textit{Horn-}\mathcal{ALCHI}$.

A regular expression is an expression generated by the grammar

$$\mathfrak{E}::=\varepsilon\mid\mathtt{R}\mid\mathtt{R}^{-}\mid\big(\mathfrak{E}\cup\mathfrak{E}\big)\mid\big(\mathfrak{E}\cdot\mathfrak{E}\big)\mid\big(\mathfrak{E}\big)^{*},$$

where $\mathtt{R}\in\mathsf{Roles}$. For a regular expression $\mathfrak{E}$, let $\mathbf{Lang}(\mathfrak{E})$ denote the set of all words over role expressions generated by $\mathfrak{E}$. A RE atom is a formula of the form $\mathfrak{E}(t,u)$ with $\mathfrak{E}$ a regular expression and $t,u\in\mathsf{Terms}$. A RE fact is a variable-free RE atom. A positive two-way regular path query (PQ) is a formula without occurrences of free variables generated by the grammar

$$\varphi::=\top\mid\mathtt{A}(t)\mid\mathfrak{E}(t,u)\mid\big(\varphi\wedge\varphi\big)\mid\big(\varphi\vee\varphi\big)\mid\exists y.\varphi,$$

where $\mathtt{A}(t)$ is a class atom, $\mathfrak{E}(t,u)$ is a RE atom, and $y$ is a variable. Note that, under our definition, all PQs are Boolean queries since every occurrence of a variable in a PQ lies within the scope of an existential quantifier. Without loss of generality, we assume that every variable is quantified exactly once in a PQ.

Consider some FO sentence $\psi$. Given another FO sentence $\psi^{\prime}$, we write $\psi\models\psi^{\prime}$ to denote entailment under under active domain semantics, that is, standard FO semantics with quantifiers ranging over the active domain. Given a finite set $\SS$ of FO sentences, we write $\SS\models\psi$ to denote $\bigwedge_{\psi^{\prime}\in\SS}\psi^{\prime}\models\psi$. Given a KB $\langle\mathcal{R},\mathcal{F}\rangle$, we write $\langle\mathcal{R},\mathcal{F}\rangle\models\psi$ to denote $\mathcal{R}\cup\mathcal{F}\models\psi$.

A substitution is a function mapping variables to terms. For a substitution $\sigma$ and a FO formula $\psi[\vec{x}]$, let $\sigma(\psi)$ denote the formula obtained from $\psi$ by replacing all occurrences of every variable $x\in\mathbf{Domain}(\sigma)\cap\vec{x}$ with $\sigma(x)$.

Consider a fact set $\mathcal{F}$. We define $\mathbf{Inv}(\mathcal{F})=\{\mathtt{R}^{-}(c,d)\mid\mathtt{R}(d,c)\in\mathcal{F}\}$. A (possibly empty) word over role expressions $\mathtt{R_{1}}\ldots\mathtt{R_{n}}$ is a path from a constant $c$ to a constant $d$ in $\mathcal{F}$ if both $c$ and $d$ occur in $\mathcal{F}$, and there exists a list of constants $e_{0},\ldots,e_{n}$ such that $e_{0}=c$, $e_{n}=d$, and $\mathtt{R_{i}}(e_{i-1},e_{i})\in\mathcal{F}\cup\mathbf{Inv}(\mathcal{F})$ for every $1\leq i\leq n$. In particular, for $n=0$, the empty word $\varepsilon$ is a path from any constant occuring in $\mathcal{F}$ to itself. For some constants $c$ and $d$ occurring $\mathcal{F}$, we write $\mathbf{Paths}_{\mathcal{F}}(c,d)$ for the set of all paths from $c$ to $d$ in $\mathcal{F}$. Entailment of a PQ $\varphi$ by $\mathcal{F}$, written $\mathcal{F}\models\varphi$, is defined inductively as follows:

• •

  If $\varphi=\top$, then $\mathcal{F}\models\varphi$.

• •

  If $\varphi$ is a class fact, then $\mathcal{F}\models\varphi$ if $\varphi\in\mathcal{F}$.

• •

  If $\varphi$ is a RE fact $\mathfrak{E}(c,d)$, then $\mathcal{F}\models\varphi$ if $\mathbf{Paths}_{\mathcal{F}}(c,d)\cap\mathbf{Lang}(\mathfrak{E})\neq\emptyset$.

• •

  If $\varphi$ is of the form $\big(\varphi_{1}\wedge\varphi_{2}\big)$, then $\mathcal{F}\models\varphi$ if $\mathcal{F}\models\varphi_{1}$ and $\mathcal{F}\models\varphi_{2}$.

• •

  If $\varphi$ is of the form $\big(\varphi_{1}\vee\varphi_{2}\big)$, then $\mathcal{F}\models\varphi$ if $\mathcal{F}\models\varphi_{1}$ or $\mathcal{F}\models\varphi_{2}$.

• •

  If $\varphi$ is of the form $\exists x.\varphi^{\prime}$, then $\mathcal{F}\models\varphi$ if $\mathcal{F}\models\sigma(\varphi^{\prime})$ for some substitution $\sigma$ mapping $x$ to some constant in $\mathcal{F}$.

Since PQs contain no free variables, defining $\mathcal{F}\models\alpha$ for any ground atom $\alpha$ suffices to fully specify the semantics of entailment.

For a rule query $\langle\mathcal{R},\alpha\rangle$, we write $\mathbf{QM}(\langle\mathcal{R},\alpha\rangle)$ or $\mathbf{QM}(\mathcal{R},\alpha)$ to refer to the set of all finite fact sets $\mathcal{F}$ such that $\langle\mathcal{R},\mathcal{F}\rangle\models\alpha$. For a PQ $\varphi$, let $\mathbf{QM}(\varphi)$ be the set of all finite fact sets that entail $\varphi$. Here, $\mathbf{QM}$ stands for “query mapping”, since it associates every rule query or PQ with its semantic extension, namely the set of finite fact sets that satisfy it. A rule query or PQ $\gamma$ is contained in another such query $\gamma^{\prime}$ if $\mathbf{QM}(\gamma)\subseteq\mathbf{QM}(\gamma^{\prime})$; these are equivalent if $\mathbf{QM}(\gamma)=\mathbf{QM}(\gamma^{\prime})$.

The chase algorithm can be used to decide fact entailment and is defined here only for Datalog, since $\textit{Horn-}\mathcal{ALCHI}$ rules with existentially quantified variables can be normalised away, as explained in the following section. A trigger $\tau$ is a pair $\langle\varrho,\sigma\rangle$ consisting of a Datalog rule $\varrho=\beta\to\eta$ and a substitution $\sigma$ that is defined exactly on the set of all variables occurring in $\varrho$. The trigger $\tau$ is applicable to a fact set $\mathcal{F}$ if $\sigma(\beta)\subseteq\mathcal{F}$ and all constants in the range of $\sigma$ occur in $\mathcal{F}$. We define $\mathbf{Output}(\tau)=\sigma(\eta)$ and, for a fact set $\mathcal{F}$, we define $\mathbf{App}_{\varrho}(\mathcal{F})$ as the set including $\mathbf{Output}(\tau)$ for every trigger $\tau$ with $\varrho$ that is applicable to $\mathcal{F}$. For a Datalog rule set $\mathcal{R}$ and a fact set $\mathcal{F}$, let $\mathbf{App}_{\mathcal{R}}(\mathcal{F})=\bigcup_{\varrho\in\mathcal{R}}\mathbf{App}_{\varrho}(\mathcal{F})$. For a Datalog KB $\mathcal{K}=\langle\mathcal{R},\mathcal{F}\rangle$, let $\mathbf{Ch}_{1}(\mathcal{K}),\mathbf{Ch}_{2}(\mathcal{K}),\ldots$ be the sequence of fact sets such that (i) $\mathbf{Ch}_{1}(\mathcal{K})=\mathcal{F}$, and (ii) $\mathbf{Ch}_{i}(\mathcal{K})=\mathbf{Ch}_{i-1}(\mathcal{K})\cup\mathbf{App}_{\mathcal{R}}(\mathbf{Ch}_{i-1}(\mathcal{K}))$ for every $i\geq 2$. We define the chase of $\mathcal{K}$, written $\mathbf{Ch}(\mathcal{K})$, as the union of all fact sets in this sequence. By our definition of applicable triggers, the chase is always finite, and it yields a set of facts that can be used to decide fact entailment under active domain semantics [1].

For a Datalog KB $\mathcal{K}$, the chase depth of a fact $\alpha\in\mathbf{Ch}(\mathcal{K})$ with respect to $\mathcal{K}$ is the least $k\geq 1$ such that $\alpha\in\mathbf{Ch}_{k}(\mathcal{K})$.