# Extending Consequence-Based Reasoning to $\boldsymbol{\mathcal{SRIQ}}$

Andrew Bate, Boris Motik, Bernardo Cuenca Grau, František Simančík, Ian
Horrocks
Department of Computer Science, University of Oxford,
Oxford, United Kingdom
<EMAIL_ADDRESS>
###### Abstract

Consequence-based calculi are a family of reasoning algorithms for
_description logics_ (DLs), and they combine hypertableau and resolution in a
way that often achieves excellent performance in practice. Up to now, however,
they were proposed for either Horn DLs (which do not support disjunction), or
for DLs without counting quantifiers. In this paper we present a novel
consequence-based calculus for $\mathcal{SRIQ}$—a rich DL that supports both
features. This extension is non-trivial since the intermediate consequences
that need to be derived during reasoning cannot be captured using DLs
themselves. The results of our preliminary performance evaluation suggest the
feasibility of our approach in practice.

##  1 Introduction

_Description logics_ (DLs) (?) are a family of knowledge representation
formalisms with numerous applications in practice. DL-based applications model
a domain of interest by means of an _ontology_ , in which key notions in the
domain are described using _concepts_ (i.e., unary predicates), and the
relationships between concepts are described using _roles_ (i.e., binary
predicates). _Subsumption_ is the problem of determining whether each instance
of a concept $C$ is also an instance of a concept $D$ in all models of an
ontology, and it is a fundamental reasoning problem in applications of DLs.
For expressive DLs, this problem is of high worst-case complexity, ranging
from ExpTime up to N2ExpTime.

Despite these discouraging complexity bounds, highly optimised reasoners such
as FaCT++ (?), Pellet (?), HermiT (?), and Konclude (?) have proved successful
in practice. These systems are typically based on (hyper)tableau calculi,
which construct a finite representation of a canonical model of the ontology
disproving a postulated subsumption. While such calculi can handle many
ontologies, in some cases they construct very large model representations,
which is a source of performance problems; this is further exacerbated by the
large number of subsumption tests often required to classify an ontology.

A recent breakthrough in DL reasoning came in the form of _consequence-based
calculi_. The reasoning algorithm by ? (?) for the lightweight logic
$\mathcal{EL}$ can be seen as the first such calculus. It was later extended
to the more expressive DLs Horn-$\mathcal{SHIQ}$ (?) and
Horn-$\mathcal{SROIQ}$ (?)—DLs that support counting quantifiers, but not
disjunctions between concepts. Consequence-based calculi were also developed
for $\mathcal{ALCH}$ (?) and $\mathcal{ALCI}$ (?), which support concept
disjunction, but not counting quantifiers. Such calculi can be seen as
combining resolution and hypertableau (see Section 3 for details): as in
resolution, they describe ontology models by systematically deriving relevant
consequences; and as in (hyper)tableau, they are goal-directed and avoid
drawing unnecessary consequences. Additionally, they are not only
refutationally complete, but can also (dis)prove all relevant subsumptions in
a single run, which can greatly reduce the overall computational work.
Finally, unlike implemented (hyper)tableau reasoners, they are worst-case
optimal for the logic they support. ? (?) presented a way of combining a
consequence-based calculus with a traditional tableau-based prover; while such
a combination seems to perform well in practice, the saturation rules are only
known to be complete for $\mathcal{EL}$ ontologies, and the overall approach
is not worst-case optimal for $\mathcal{SRIQ}$.

Existing consequence-based algorithms cannot handle DLs such as
$\mathcal{ALCHIQ}$ that provide both disjunctions and counting quantifiers. As
we argue in Section 3, extending these algorithms to handle such DLs is
challenging: counting quantifiers require equality reasoning which, together
with disjunctions, can impose complex constraints on ontology models; and,
unlike existing consequence-based calculi, such constraints cannot be captured
using DLs themselves, which makes the reasoning process much more involved.

In Section 4 we present a consequence-based calculus for $\mathcal{ALCHIQ}$;
by using the encoding of role chains by ? (?), our calculus can also handle
$\mathcal{SRIQ}$, which covers all of OWL 2 DL except for nominals, reflexive
roles, and datatypes. Borrowing ideas from resolution theorem proving, we
encode the calculus’ consequences as first-order clauses of a specific form,
and we handle equality using a variant of _ordered paramodulation_ (?)—a state
of the art calculus for equational theorem proving used in modern theorem
provers such as E (?) and Vampire (?). Furthermore, we have carefully
constrained the inference rules so that our calculus mimics existing calculi
on $\mathcal{ELH}$ ontologies, which ensures robust performance of our
calculus on ‘mostly-$\mathcal{ELH}$’ ontologies.

We have implemented a prototype system and compared its performance with that
of well-established reasoners. Our results in Section 5 suggest that our
system can significantly outperform FaCT++, Pellet, or HermiT, and often
exhibits comparable performance to that of Konclude.

Table 1: Translating Normalised $\mathcal{ALCHIQ}$ Ontologies into DL-Clauses DL1 | $\bigsqcap\limits_{1\leq i\leq n}B_{i}\sqsubseteq$ |  $\bigsqcup\limits_{n+1\leq i\leq m}B_{i}$ |  $\rightsquigarrow$ | $\bigwedge\limits_{1\leq i\leq n}B_{i}(x)\rightarrow$ | $\bigvee\limits_{n+1\leq i\leq m}B_{i}(x)$ |
---|---|---|---|---|---|---
DL2 | $B_{1}\sqsubseteq$ |  ${\geqslant}\,n\,S.B_{2}$ |  $\rightsquigarrow$ | $B_{1}(x)\rightarrow$ | $S(x,f_{i}(x))$ | for ${1\leq i\leq n}$
$B_{1}(x)\rightarrow$ | $B_{2}(f_{i}(x))$ | for ${1\leq i\leq n}$
$B_{1}(x)\rightarrow$ | $f_{i}(x)\not\approx f_{j}(x)$ | for ${1\leq i<j\leq n}$
DL3 | $\exists S.B_{1}\sqsubseteq$ |  $B_{2}$ |  $\rightsquigarrow$ | $S(z_{1},x)\wedge B_{1}(x)\rightarrow$ | $B_{2}(z_{1})$ |
DL4 | $B_{1}\sqsubseteq$ |  ${\leqslant}\,n\,S.B_{2}$ |  $\rightsquigarrow$ | $S(z_{1},x)\wedge B_{2}(x)\rightarrow$ | $S_{B_{2}}(z_{1},x)$ | for fresh $S_{B_{2}}$
$B_{1}(x)\wedge\bigwedge\limits_{1\leq i\leq n+1}S_{B_{2}}(x,z_{i})\rightarrow$ | $\bigvee\limits_{1\leq i<j\leq n+1}z_{i}\approx z_{j}$
DL5 | $S_{1}\sqsubseteq$ |  $S_{2}$ |  $\rightsquigarrow$ | $S_{1}(z_{1},x)\rightarrow$ | $S_{2}(z_{1},x)$ |
DL6 | $S_{1}\sqsubseteq$ |  $S_{2}^{-}$ |  $\rightsquigarrow$ | $S_{1}(z_{1},x)\rightarrow$ | $S_{2}(x,z_{1})$ |

##  2 Preliminaries

First-Order Logic.  It is usual in equational theorem proving to encode atomic
formulas as terms, and to use a multi-sorted signature that prevents us from
considering malformed terms. Thus, we partition the signature into a set
$\mathcal{P}$ of _predicate symbols_ and a set $\mathcal{F}$ of _function
symbols_ ; moreover, we assume that $\mathcal{P}$ has a special constant
$\wp$. A _term_ is constructed as usual using variables and the signature
symbols, with the restriction that predicate symbols are allowed to occur only
at the outermost level; the latter terms are called $\mathcal{P}$-_terms_ ,
while all other terms are $\mathcal{F}$-_terms_. For example, for $P$ a
predicate and $f$ a function symbol, $f(P(x))$ and $P(P(x))$ are both
malformed; $P(f(x))$ is a well-formed $\mathcal{P}$-term; and $f(x)$ and $x$
are both well-formed $\mathcal{F}$-terms. Term $f(t)$ is an $f$-_successor_ of
$t$, and $t$ is an $f$-_predecessor_ of $f(t)$.

An _equality_ is a formula of the form ${s\approx t}$, where $s$ and $t$ are
either both $\mathcal{F}$\- or both $\mathcal{P}$-terms. An equality of the
form ${P(\vec{s})\approx\wp}$ is called an _atom_ and is written as just
$P(\vec{s})$ whenever it is clear from the context that the expression denotes
a formula, and not a $\mathcal{P}$-term. An _inequality_ is a negation of an
equality and is written as ${s\not\approx t}$. We assume that $\approx$ and
$\not\approx$ are implicitly symmetric—that is, ${s\bowtie t}$ and ${t\bowtie
s}$ are identical, for ${{\bowtie}\in\\{\hskip
0.29999pt{\approx},\;{\not\approx}\hskip 0.29999pt\\}}$. A _literal_ is an
equality or an inequality. A _clause_ is a formula of the form
${\forall\vec{x}.[\Gamma\rightarrow\Delta]}$ where $\Gamma$ is a conjunction
of atoms called the _body_ , $\Delta$ is a disjunction of literals called the
_head_ , and $\vec{x}$ contains all variables occurring in the clause;
quantifier $\forall\vec{x}$ is usually omitted as it is understood implicitly.
We often treat conjunctions and disjunctions as sets (i.e., they are unordered
and without repetition) and use them in standard set operations; and we write
the empty conjunction (disjunction) as $\top$ ($\bot$). For $\alpha$ a term,
literal, clause, or a set thereof, we say that $\alpha$ is _ground_ if it does
not contain a variable; $\alpha\sigma$ is the result of applying a
substitution $\sigma$ to $\alpha$; and we often write substitutions as
${\sigma=\\{{x\mapsto t_{1},\;y\mapsto t_{2},\;\dots}\\}}$. We use the
standard notion of subterm positions; $s|_{p}$ is the subterm of $s$ at
position $p$; position $p$ is _proper_ in a term $t$ if ${t|_{p}\neq t}$; and
$s[t]_{p}$ is the term obtained by replacing the subterm of $s$ at position
$p$ with $t$.

A _Herbrand equality interpretation_ is a set of ground equalities satisfying
the usual congruence properties. Satisfaction of a ground conjunction, a
ground disjunction, or a (not necessarily ground) clause $\alpha$ in an
interpretation $I$, written ${I\models\alpha}$, as well as entailment of a
clause ${\Gamma\rightarrow\Delta}$ from a set of clauses $\mathcal{O}$,
written ${\mathcal{O}\models\Gamma\rightarrow\Delta}$, are defined as usual.
Note that a ground disjunction of literals $\Delta$ may contain inequalities
so ${I\models\Delta}$ does not necessarily imply ${I\cap\Delta\neq\emptyset}$.

Unless otherwise stated, (possibly indexed) letters $x$, $y$, and $z$ denote
variables; $l$, $r$, $s$, and $t$ denote terms; $A$ denotes an atom or a
$\mathcal{P}$-term (depending on the context); $L$ denotes a literal; $f$ and
$g$ denote function symbols; $B$ denotes a unary predicate symbol; and $S$
denotes a binary predicate symbol.

Orders.  A _strict order_ $\succ$ on a universe $U$ is an irreflexive,
asymmetric, and transitive relation on $U$; and $\succeq$ is the _non-strict
order_ induced by $\succ$. Order $\succ$ is _total_ if, for all ${a,b\in U}$,
we have ${a\succ b}$, ${b\succ a}$, or ${a=b}$. Given ${{\circ}\in\\{\hskip
0.29999pt{\succ},{\succeq}\hskip 0.29999pt\\}}$, element ${b\in U}$, and
subset ${S\subseteq U}$, the notation ${S\circ b}$ abbreviates ${\exists a\in
S:a\circ b}$. The _multiset extension_ $\succ_{\mathit{mul}}$ of $\succ$
compares multisets $M$ and $N$ on $U$ such that ${M\succ_{\mathit{mul}}N}$ if
and only if ${M\neq N}$ and, for each ${n\in N\setminus M}$, some ${m\in
M\setminus N}$ exists such that ${m\succ n}$, where $\setminus$ is the
multiset difference operator.

A _term order_ $\succ$ is a _strict_ order on the set of all terms. We extend
$\succ$ to literals by identifying each ${s\not\approx t}$ with the multiset
${\\{s,s,t,t\\}}$ and each ${s\approx t}$ with the multiset ${\\{s,t\\}}$, and
by comparing the result using the multiset extension of $\succ$. We reuse the
symbol $\succ$ for the induced literal order since the intended meaning should
be clear from the context.

DL-Clauses.  Our calculus takes as input a set $\mathcal{O}$ of _DL-clauses_
—that is, clauses restricted to the following form. Let $\mathcal{P}_{1}$ and
$\mathcal{P}_{2}$ be countable sets of unary and binary predicate symbols, and
let $\mathcal{F}$ be a countable set of unary function symbols. DL-clauses are
written using the _central variable_ $x$ and variables $z_{i}$. A _DL-
$\mathcal{F}$-term_ has the form $x$, $z_{i}$, or $f(x)$ with
${f\in\mathcal{F}}$; a _DL- $\mathcal{P}$-term_ has the form $B(z_{i})$,
$B(x)$, $B(f(x))$, $S(x,z_{i})$, $S(z_{i},x)$, $S(x,f(x))$, $S(f(x),x)$ with
${B\in\mathcal{P}_{1}}$ and ${S\in\mathcal{P}_{2}}$; and a _DL-term_ is a
DL-$\mathcal{F}$-term or a DL-$\mathcal{P}$-term. A _DL-atom_ has the form
${A\approx\wp}$ with $A$ a DL-$\mathcal{P}$-term. A _DL-literal_ is a DL-atom,
or it is of the form ${f(x)\bowtie g(x)}$, ${f(x)\bowtie z_{i}}$, or
${z_{i}\bowtie z_{j}}$ with ${{\bowtie}\in\\{\hskip
0.29999pt{\approx},\;{\not\approx}\hskip 0.29999pt\\}}$. A _DL-clause_
contains only DL-atoms of the form $B(x)$, $S(x,z_{i})$, and $S(z_{i},x)$ in
the body and only DL-literals in the head, and each variable $z_{i}$ occurring
in the head also occurs in the body. An _ontology_ $\mathcal{O}$ is a finite
set of DL-clauses. A _query clause_ is a DL-clause in which all literals are
of the form $B(x)$. Given an ontology $\mathcal{O}$ and a query clause
${\Gamma\rightarrow\Delta}$, our calculus decides whether
${\mathcal{O}\models\Gamma\rightarrow\Delta}$ holds.

$\mathcal{SRIQ}$ ontologies written using the DL-style syntax can be
transformed into DL-clauses without affecting query clause entailment. First,
we _normalise_ DL axioms to the form shown on the left-hand side of Table 1:
we transform away role chains and then replace all complex concepts with fresh
atomic ones; this process is well understood (?; ?; ?), so we omit the
details. Second, using the well-known correspondence between DLs and first-
order logic (?), we translate normalised axioms to DL-clauses as shown on the
right-hand side of Table 1. The standard translation of
${B_{1}\sqsubseteq{\leqslant}\,n\,S.B_{2}}$ requires atoms $B_{2}(z_{i})$ in
clause bodies, which are not allowed in our setting. We address this issue by
introducing a fresh role $S_{B_{2}}$ that we axiomatise as ${S(y,x)\wedge
B_{2}(x)\rightarrow S_{B_{2}}(y,x)}$; this, in turn, allows us to clausify the
original axiom as if it were ${B_{1}\sqsubseteq{\leqslant}\,n\,S_{B_{2}}}$.
For an $\mathcal{ELH}$ ontology, $\mathcal{O}$ contains DL-clauses of type DL1
with ${m=n+1}$, DL2 with ${n=1}$, DL3, and DL5.

##  3 Motivation

$\begin{array}[]{r@{\;}lcr@{\;}l@{\qquad}l@{\;}l}\lx@intercol\hfil\text{Ontology
}\mathcal{O}_{1}\hfil\\\
\hline\cr\hbox{\multirowsetup$B_{i}$}&\hbox{\multirowsetup$\sqsubseteq\exists
S_{j}.B_{i+1}$}&\hbox{\multirowsetup$\rightsquigarrow$}&B_{i}(x)\rightarrow&S_{j}(x,f_{i+1,j}(x))&\eqref{ex:why:1}&\rdelim\\}{2}{4.5cm}[$\text{
for } 0 \leq i < n \text{ and } 1 \leq j \leq 2$]\\\
&&&B_{i}(x)\rightarrow&B_{i+1}(f_{i+1,j}(x))&\eqref{ex:why:2}&\\\
B_{n}&\sqsubseteq
C_{n}&\rightsquigarrow&B_{n}(x)\rightarrow&C_{n}(x)&\eqref{ex:why:3}&\\\
\exists S_{j}.C_{i+1}&\sqsubseteq C_{i}&\rightsquigarrow&S_{j}(z_{1},x)\wedge
C_{i+1}(x)\rightarrow&C_{i}(z_{1})&\eqref{ex:why:4}&\;\;\;\,\text{for }0\leq
i<n\text{ and }1\leq j\leq 2\\\ \hline\cr\end{array}$

$v_{B_{0}(x)}$$B_{0}(x)$ Initialisation: | $\top$ | $\rightarrow B_{0}(x)$ | (5)
---|---|---|---
$\mathsf{Hyper}$[1+1]: | $\top$ | $\rightarrow S_{j}(x,f_{1,j}(x))$ | (6)
$\mathsf{Hyper}$[1+1]: | $\top$ | $\rightarrow B_{1}(f_{1,j}(x))$ | (7)
$\mathsf{Pred}$[1]: | $\top$ | $\rightarrow C_{0}(x)$ | (20)
$v_{B_{1}(x)}$$B_{1}(x)$ $\mathsf{Succ}$[1+1]: | $\top$ | $\rightarrow S_{j}(y,x)$ | (10)
---|---|---|---
$\mathsf{Succ}$[1+1]: | $\top$ | $\rightarrow B_{1}(x)$ | (11)
$\mathsf{Hyper}$[1+1]: | $\top$ | $\rightarrow S_{j}(x,f_{2,j}(x))$ | (12)
$\mathsf{Hyper}$[1+1]: | $\top$ | $\rightarrow B_{2}(x,f_{2,j}(x))$ | (13)
$\mathsf{Pred}$[$\dots$]: | $\top$ | $\rightarrow C_{1}(x)$ | (18)
$\mathsf{Hyper}$[1+1+1]: | $\top$ | $\rightarrow C_{0}(y)$ | (19)
$\cdots$$v_{B_{n}(x)}$$B_{n}(x)$ $\mathsf{Succ}$[$\dots$]: | $\top$ | $\rightarrow S_{j}(y,x)$ | (14)
---|---|---|---
$\mathsf{Succ}$[$\dots$]: | $\top$ | $\rightarrow B_{n}(x)$ | (15)
$\mathsf{Hyper}$[1+1]: | $\top$ | $\rightarrow C_{n}(x)$ | (16)
$\mathsf{Hyper}$[1+1+1]: | $\top$ | $\rightarrow C_{n-1}(y)$ | (17)
$\mathsf{Succ}$[1+1]: $f_{1,1}$ (1)$\mathsf{Succ}$[1+1]: $f_{1,2}$ (1)

Figure 1: Example Motivating Consequence-Based Calculi

As motivation for our work, in Section 3.1 we discuss the drawbacks of
existing DL reasoning calculi, and then in Section 3.2 we discuss how existing
consequence-based calculi address these problems by separating clauses into
contexts in a way that considerably reduces the number of inferences. Next, in
Section 3.3 we discuss the main contribution of this paper, which lies in
extending the consequence-based framework to a DL with disjunctions and number
restrictions. Handling the latter requires equality reasoning, which requires
a more involved calculus and completeness proof.

###  3.1 Why Consequence-Based Calculi?

Consider the $\mathcal{EL}$ ontology $\mathcal{O}_{1}$ in Figure 1; one can
readily check that ${\mathcal{O}\models B_{i}(x)\rightarrow C_{i}(x)}$ holds
for ${0\leq i\leq n}$. To prove ${\mathcal{O}\models B_{0}(x)\rightarrow
C_{0}(x)}$ using the (hyper)tableau calculus, we start with $B_{0}(a)$ and
apply (1)–(1) in a forward-chaining manner. Since $\mathcal{O}$ contains (1)
for ${j\in\\{\hskip 0.29999pt1,2\hskip 0.29999pt\\}}$, this constructs a tree-
shaped model of depth $n$ and a fanout of two, where nodes at depth $i$ are
labelled by $B_{i}$ and $C_{i}$. Forward chaining ensures that reasoning is
goal-oriented; however, all nodes labelled with $B_{i}$ are of the same type
and they share the same properties, which reveals a weakness of (hyper)tableau
calculi: the constructed models can be large (exponential in our example) and
highly redundant; apart from causing problems in practice, this often prevents
(hyper)tableau calculi from being worst-case optimal. Techniques such as
_caching_ (?) or _anywhere blocking_ (?) can constrain model construction, but
their effectiveness often depends on the order of rule applications. Thus,
model size is a key limiting factor for (hyper)tableau-based reasoners (?).

In contrast, resolution describes models using (universally quantified)
clauses that ‘summarise’ the model. This eliminates redundancy and ensures
worst-case optimality of many resolution decision procedures. Many resolution
variants have been proposed (?), each restricting inferences in a specific
way. However, to ensure termination, all decision procedure for DLs we are
aware of perform inferences with the ‘deepest’ and the ‘covering’ clause
atoms, so all of them will resolve all (1) with all (1) to obtain all $2n^{2}$
clauses of the form

$\displaystyle\begin{array}[]{@{}l@{}}B_{i}(x)\wedge
C_{k+1}(f_{i+1,j}(x))\rightarrow C_{k}(x)\\\ \hskip 71.13188pt\text{for }1\leq
i,k<n\text{ and }1\leq j\leq 2.\end{array}$ (23)

Of these $2n^{2}$ clauses, only those with ${i=k}$ are relevant to proving our
goal. If we extend $\mathcal{O}$ with additional clauses that contain $B_{i}$
and $C_{i}$, each of these $2n^{2}$ clauses can participate in further
inferences and give rise to more irrelevant clauses. This problem is
particularly pronounced when $\mathcal{O}$ is satisfiable since we must then
produce all consequences of $\mathcal{O}$.

###  3.2 Basic Notions

Consequence-based calculi combine ‘summarisation’ of resolution with goal-
directed search of (hyper)tableau calculi. ? (?) presented a framework for
$\mathcal{ALCI}$ capturing the key elements of the related calculi by ? (?), ?
(?), ? (?), and ? (?). Before extending this framework to $\mathcal{ALCHIQ}$
in Section 4, we next informally recapitulate the basic notions; however, to
make this paper easier to follow, we use the same notation and terminology as
in Section 4.

Our consequence-based calculus constructs a directed graph
${\mathcal{D}=\langle\mathcal{V},\mathcal{E},\mathcal{S},\mathsf{core},\succ\rangle}$
called a _context structure_. The vertices in $\mathcal{V}$ are called
_contexts_. Let $I$ be a Herbrand model of $\mathcal{O}$; hence, the domain of
$I$ contains ground terms. Instead of representing each ground term of $I$
separately as in (hyper)tableau calculi, $\mathcal{D}$ can represent the
properties of several terms by a single context $v$. Each context
${v\in\mathcal{V}}$ is associated with a (possibly empty) conjunction
$\mathsf{core}_{v}$ of _core_ atoms that must hold for all ground terms that
$v$ represents; thus, $\mathsf{core}_{v}$ determines the ‘kind’ of context
$v$. Moreover, $v$ is associated with a set $\mathcal{S}_{v}$ of clauses that
capture the constraints that these terms must satisfy. Partitioning clauses
into sets allows us to restrict the inferences between clause sets and thus
eliminate certain irrelevant inferences. Clauses in $\mathcal{S}_{v}$ are
‘relative’ to $\mathsf{core}_{v}$: for each
${\Gamma\rightarrow\Delta\in\mathcal{S}_{v}}$, we have
${\mathcal{O}\models\mathsf{core}_{v}\wedge\Gamma\rightarrow\Delta}$—that is,
we do not include $\mathsf{core}_{v}$ in clause bodies since
$\mathsf{core}_{v}$ holds implicitly. Function $\succ$ provides each context
${v\in\mathcal{V}}$ with a concept order $\succ_{v}$ that restricts resolution
inferences in the presence of disjunctions.

Contexts are connected by directed edges labelled with function symbols. If
$u$ is connected to $v$ via an $f$-labelled edge, then the $f$-successor of
each ground term represented by $u$ is represented by $v$. Conversely, if $u$
and $v$ are _not_ connected by an $f$-edge, then each ground term represented
by $v$ is not an $f$-successor of a ground term represented by $u$, so no
inference between $\mathcal{S}_{u}$ and $\mathcal{S}_{v}$ is ever needed.

Consequence-based calculi are not just complete for refutation: they derive
the required consequences. Figure 1 demonstrates this for
${\mathcal{O}_{1}\models B_{0}(x)\rightarrow C_{0}(x)}$. The cores and the
clauses shown above and below, respectively, each context, and clause numbers
correspond to the derivation order. To prove ${B_{0}(x)\rightarrow C_{0}(x)}$,
we introduce context $v_{B_{0}(x)}$ with core ${B_{0}(x)}$ and add clause (1)
to it. The latter says that $B_{0}$ holds for $a$, and it is analogous to
initialising a (hyper)tableau calculus with $B_{0}(a)$. The calculus then
applies rules from Table 2 to derive new clauses and/or extend $\mathcal{D}$.

$\mathsf{Hyper}$ is the standard hyperresolution rule restricted to a single
context at a time. Thus, we derive (1) from (1) and (1), and (1) from (1) and
(1). Hyperresolution resolves all body atoms, which makes the resolvent
relevant for the context and prevents the derivation of irrelevant clauses
such as (23).

Context $v_{B_{0}(x)}$ contains atoms with function symbols $f_{1,1}$ and
$f_{1,2}$, so the $\mathsf{Succ}$ rule must ensure that the $f_{1,1}$\- and
$f_{1,2}$-successors of the ground terms represented by $v_{B_{0}(x)}$ are
adequately represented in $\mathcal{D}$. We can control context introduction
via a parameter called an _expansion strategy_ —a function that determines
whether to reuse an existing context or introduce a fresh one; in the latter
case, it also determines how to initialise the context’s core. We discuss
possible strategies in Section 4.1; in the rest of this example, we use the
so-called cautious strategy, where the $\mathsf{Succ}$ rule introduces context
$v_{B_{1}(x)}$ and initialises it with (1) and (1). Note that (1) represents
two clauses, both of which we satisfy (in separate applications of the
$\mathsf{Succ}$ rule) using $v_{B_{1}(x)}$.

We construct contexts ${v_{B_{2}(x)},\dots,v_{B_{n}(x)}}$ analogously, we
derive (1) by hyperresolving (1) and (1), and we derive (1) by hyperresolving
(1), (1), and (1). Clause (1) imposes a constraint on the predecessor context,
which we propagate using the $\mathsf{Pred}$ rule, deriving (1) and (1). Since
clauses of $v_{B_{0}(x)}$ are ‘relative’ to the core of $v_{B_{0}(x)}$, clause
(1) represents our query clause, as required.

###  3.3 Extending the Framework to $\boldsymbol{\mathcal{ALCHIQ}}$

$\begin{array}[]{r@{\;}lcr@{\;}ll@{\;}l}\lx@intercol\hfil\text{Ontology
}\mathcal{O}_{2}\hfil\\\
\hline\cr\hbox{\multirowsetup$B_{0}$}&\hbox{\multirowsetup$\sqsubseteq\exists
S^{-}.B_{1}$}&\hbox{\multirowsetup$\rightsquigarrow$}&B_{0}(x)&\rightarrow
S(f_{1}(x),x)&\eqref{ex:diff:1}\\\ &&&B_{0}(x)&\rightarrow
B_{1}(f_{1}(x))&\eqref{ex:diff:2}\\\
\hbox{\multirowsetup$B_{1}$}&\hbox{\multirowsetup$\sqsubseteq\exists
S.B_{i}$}&\hbox{\multirowsetup$\rightsquigarrow$}&B_{1}(x)&\rightarrow
S(x,f_{i}(x))&\eqref{ex:diff:4}&\rdelim\\}{3}{2.35cm}[$\text{ for } 2 \leq i
\leq 3$]\\\ &&&B_{1}(x)&\rightarrow B_{i}(f_{i}(x))&\eqref{ex:diff:5}\\\
B_{i}&\sqsubseteq B_{4}&\rightsquigarrow&B_{i}(x)&\rightarrow
B_{4}(x)&\eqref{ex:diff:6}\\\ B_{2}\sqcap
B_{3}&\sqsubseteq\bot&\rightsquigarrow&B_{2}(x)\wedge
B_{3}(x)&\rightarrow\bot&\eqref{ex:diff:3}\\\
B_{1}&\sqsubseteq{\leq}2.S&\rightsquigarrow&\lx@intercol
B_{1}(x)\wedge\bigwedge_{1\leq i\leq 3}S(x,z_{i})\rightarrow\bigvee_{1\leq
j<k\leq 3}z_{j}\approx z_{k}\hfil&\eqref{ex:diff:7}\\\ \hline\cr\end{array}$

$v_{0}$$B_{0}(x)$ Initialisation: | $\top$ | $\rightarrow B_{0}(x)$ | (31)
---|---|---|---
$\mathsf{Hyper}$[2+2]: | $\top$ | $\rightarrow S(f_{1}(x),x)$ | (32)
$\mathsf{Hyper}$[2+2]: | $\top$ | $\rightarrow B_{1}(f_{1}(x))$ | (33)
$\mathsf{Pred}$[2]: | $\top$ | $\rightarrow B_{2}(x)\vee B_{3}(x)$ | (54)
$\mathsf{Hyper}$[2+2]: | $\top$ | $\rightarrow B_{4}(x)\vee B_{2}(x)$ | (55)
$\mathsf{Hyper}$[2+2]: | $\top$ | $\rightarrow B_{4}(x)$ | (56)
$v_{1}$$\;\;S(x,y),B_{1}(x)$ $\mathsf{Succ}$[2+2]: | $\top$ | $\rightarrow S(x,y)$ | (35)
---|---|---|---
$\mathsf{Succ}$[2+2]: | $\top$ | $\rightarrow B_{1}(x)$ | (36)
$\mathsf{Hyper}$[2+2]: | $\top$ | $\rightarrow S(x,f_{2}(x))$ | (37)
$\mathsf{Hyper}$[2+2]: | $\top$ | $\rightarrow B_{2}(f_{2}(x))$ | (38)
$\mathsf{Hyper}$[2+2]: | $\top$ | $\rightarrow S(x,f_{3}(x))$ | (39)
$\mathsf{Hyper}$[2+2]: | $\top$ | $\rightarrow B_{3}(f_{3}(x))$ | (40)
$\mathsf{Hyper}$[2+2+2+2+2]: | $\top$ | $\rightarrow f_{2}(x)\approx y\vee f_{3}(x)\approx y\vee f_{3}(x)\approx f_{2}(x)$ | (41)
$\mathsf{Eq}$[2+2]: | $\top$ | $\rightarrow f_{2}(x)\approx y\vee f_{3}(x)\approx y\vee B_{3}(f_{2}(x))$ | (42)
$\mathsf{Pred}$[2+2]: | $\top$ | $\rightarrow f_{2}(x)\approx y\vee f_{3}(x)\approx y$ | (51)
$\mathsf{Eq}$[2+2]: | $\top$ | $\rightarrow B_{3}(y)\vee f_{2}(x)\approx y$ | (52)
$\mathsf{Eq}$[2+2]: | $\top$ | $\rightarrow B_{2}(y)\vee B_{3}(y)$ | (53)
$v_{2}$$S(y,x),B_{2}(x)$ $\mathsf{Succ}$[2+2+2]: | $\top$ | $\rightarrow S(y,x)$ | (44)
---|---|---|---
$\mathsf{Succ}$[2+2+2]: | $\top$ | $\rightarrow B_{2}(x)$ | (45)
$\mathsf{Succ}$[2+2+2]: | $B_{3}(x)$ | $\rightarrow B_{3}(x)$ | (46)
$\mathsf{Hyper}$[2+2+2]: | $B_{3}(x)$ | $\rightarrow\bot$ | (47)
$v_{3}$$S(y,x),B_{3}(x)$ $\mathsf{Succ}$[2+2]: | $\top$ | $\rightarrow S(y,x)$ | (49)
---|---|---|---
$\mathsf{Succ}$[2+2]: | $\top$ | $\rightarrow B_{3}(x)$ | (50)
$\mathsf{Succ}$[2+2]: $f_{1}$ (2)$\mathsf{Succ}$[2+2+2]: $f_{2}$
(2)$\mathsf{Succ}$[2+2]: $f_{3}$ (2)

Figure 2: Challenges in Extending the Consequence-Based Framework to
$\mathcal{ALCHIQ}$

In all consequence-based calculi presented thus far, the constraints that the
ground terms represented by a context $v$ must satisfy can be represented
using standard DL-style axioms. For example, for $\mathcal{ALCI}$, ? (?)
represented all relevant consequences using DL axioms of the following form:

$\displaystyle\bigsqcap B_{i}\sqsubseteq\bigsqcup B_{j}\sqcup\bigsqcup\exists
S_{k}.B_{k}\sqcup\bigsqcup\forall S_{\ell}.B_{\ell}$ (57)

$\mathcal{ALCHIQ}$ provides both counting quantifiers and disjunctions, the
interplay of which may impose constraints that cannot be represented in
$\mathcal{ALCHIQ}$. Let $\mathcal{O}_{2}$ be as in Figure 2. To see that
${\mathcal{O}_{2}\models B_{0}(x)\rightarrow B_{4}(x)}$ holds, we construct a
Herbrand interpretation $I$ from $B_{0}(a)$: (2) and (2) derive
$S(f_{1}(a),a)$ and $B_{1}(f_{1}(a))$; and (2) and (2) derive
$S(f_{1}(a),f_{2}(f_{1}(a)))$ and $B_{2}(f_{2}(f_{1}(a)))$, and
$S(f_{1}(a),f_{3}(f_{1}(a)))$ and $B_{3}(f_{3}(f_{1}(a)))$. Due to (2) we
derive $B_{4}(f_{2}(f_{1}(a)))$ and $B_{4}(f_{3}(f_{1}(a)))$. Finally, from
(2) we derive the following clause:

$\displaystyle\begin{array}[]{@{}l@{}}f_{2}(f_{1}(a))\approx a\vee
f_{3}(f_{1}(a))\approx a\;\vee\\\ \hskip 113.81102ptf_{3}(f_{1}(a))\approx
f_{2}(f_{1}(a))\\\ \end{array}$ (60)

Disjunct ${f_{3}(f_{1}(a))\approx f_{2}(f_{1}(a))}$ cannot be satisfied due to
(2); but then, regardless of whether we choose to satisfy
${f_{3}(f_{1}(a))\approx a}$ or ${f_{2}(f_{1}(a))\approx a}$, we derive
$B_{4}(a)$.

Our calculus must be able to capture constraint (60) and its consequences, but
standard DL axioms cannot explicitly refer to specific successors and
predecessors. Instead, we capture consequences using _context clauses_
—clauses over terms $x$, $f_{i}(x)$, and $y$, where variable $x$ represents
the ground terms that a context stands for, $f_{i}(x)$ represents
$f_{i}$-successors of $x$, and $y$ represents the predecessor of $x$. We can
thus identify the predecessor and the successors of $x$ ‘by name’, allowing us
to capture constraint (60) as

$\displaystyle f_{2}(x)\approx y\vee f_{3}(x)\approx y\vee f_{3}(x)\approx
f_{2}(x).$ (61)

Based on this idea, we adapted the rules by ? (?) to handle context clauses
correctly, and we added rules that capture the consequences of equality. The
resulting set of rules is shown in Table 2.

Figure 2 shows how to verify ${\mathcal{O}_{2}\models B_{0}(x)\rightarrow
B_{4}(x)}$ using our calculus; the maximal literal of each clause is shown on
the right. We next discuss the inferences in detail.

We first create context $v_{0}$ and initialise it with (2); this ensures that
each interpretation represented by the context structure contains a ground
term for which $B_{0}$ holds. Next, we derive (2) and (2) using
hyperresolution. At this point, we could hyperresolve (2) and (2) to obtain
${\top\rightarrow S(f_{1}(x),f_{2}(f_{1}(x)))}$; however, this could easily
lead to nontermination of the calculus due to increased term nesting.
Therefore, we require hyperresolution to map variable $x$ in the DL-clauses to
variable $x$ in the context clauses; thus, hyperresolution derives in each
context only consequences about $x$, which prevents redundant derivations.

The $\mathsf{Succ}$ rule next handles function symbol $f_{1}$ in clauses (2)
and (2). To determine which information to propagate to a successor,
Definition 2 in Section 4 introduces a set $\mathsf{Su}(\mathcal{O})$ of
_successor triggers_. In our example, DL-clause (2) contains atoms $B_{1}(x)$
and $S(x,z_{i})$ in its body, and $z_{i}$ can be mapped to a predecessor or a
successor of $x$; thus, a context in which hyperresolution is applied to (2)
will be interested in information about its predecessors, which we reflect by
adding $B_{1}(x)$ and $S(x,y)$ to $\mathsf{Su}(\mathcal{O})$. In this example
we use the so-called eager strategy (see Section 4.1), so the $\mathsf{Succ}$
rule introduces context $v_{1}$, sets its core to $B_{1}(x)$ and $S(x,y)$, and
initialises the context with (2) and (2).

We next introduce (2)–(2) using hyperresolution, at which point we have
sufficient information to apply hyperresolution to (2) to derive (2). Please
note how the presence of (2) is crucial for this inference.

We use paramodulation to deal with equality in clause (2). As is common in
resolution-based theorem proving, we order the literals in a clause and apply
inferences only to maximal literals; thus, we derive (2).

Clauses (2), (2), and (2) contain function symbol $f_{2}$, so the
$\mathsf{Succ}$ rule introduces context $v_{2}$. Due to clause (2), $B_{2}(x)$
holds for all ground terms that $v_{2}$ represents; thus, we add $B_{2}(x)$ to
$\mathsf{core}_{v_{2}}$. In contrast, atom $B_{3}(f_{2}(x))$ occurs in clause
(2) in a disjunction, which means it may not hold in $v_{2}$; hence, we add
$B_{3}(x)$ to the body of clause (2). The latter clause allows us to derive
(2) using hyperresolution.

Clause (2) essentially says ‘$B_{3}(f_{2}(x))$ should not hold in the
predecessor’, which the $\mathsf{Pred}$ rule propagates to $v_{1}$ as clause
(2); one can understand this inference as hyperresolution of (2) and (2) while
observing that term $f_{2}(x)$ in context $v_{1}$ is represented as variable
$x$ in context $v_{2}$.

After two paramodulation steps, we derive clause (2), which essentially says
‘the predecessor must satisfy $B_{2}(x)$ or $B_{3}(x)$’. The set
$\mathsf{Pr}(\mathcal{O})$ of _predecessor triggers_ from Definition 2
identifies this as relevant to $v_{0}$: the DL-clauses in (2) contain
$B_{2}(x)$ and $B_{3}(x)$ in their bodies, which are represented in $v_{1}$ as
$B_{2}(y)$ and $B_{3}(y)$. Hence $\mathsf{Pr}(\mathcal{O})$ contains
$B_{2}(y)$ and $B_{3}(y)$, allowing the $\mathsf{Pred}$ rule to derive (2).

After two more steps, we finally derive our target clause (2). We could not do
this if $B_{4}(x)$ were maximal in (2); thus, we require all atoms in the head
of a goal clause to be smallest. A similar observation applies to
$\mathsf{Pr}(\mathcal{O})$: if $B_{3}(y)$ were maximal in (2), we would not
derive (2) and propagate it to $v_{0}$; thus, all atoms in
$\mathsf{Pr}(\mathcal{O})$ must be smallest too.

##  4 Formalising the Algorithm

In this section, we first present our consequence-based algorithm for
$\mathcal{ALCHIQ}$ formally, and then we present an outline of the
completeness proof; full proofs are given in the appendix.

###  4.1 Definitions

Our calculus manipulates _context clauses_ , which are constructed from
_context terms_ and _context literals_ as described in Definition 1. Unlike in
general resolution, we restrict context clauses to contain only variables $x$
and $y$, which have a special meaning in our setting: variable $x$ represents
a ground term in a Herbrand model, and $y$ represents the predecessor of $x$;
this naming convention is important for the rules of our calculus. This is in
contrast to the DL-clauses of an ontology, which can contain variables $x$ and
$z_{i}$, and where $z_{i}$ refer to either the predecessor or a successor of
$x$.

######  Definition 1.

A _context $\mathcal{F}$-term_ is a term of the form $x$, $y$, or $f(x)$ for
${f\in\mathcal{F}}$; a _context $\mathcal{P}$-term_ is a term of the form
$B(y)$, $B(x)$, $B(f(x))$, $S(x,y)$, $S(y,x)$, $S(x,f(x))$, or $S(f(x),x)$ for
${B,R\in\mathcal{P}}$ and ${f\in\mathcal{F}}$; and a _context term_ is an
$\mathcal{F}$-term or a $\mathcal{P}$-term. A _context literal_ is a literal
of the form ${A\approx\wp}$ (called a _context atom_), ${f(x)\bowtie g(x)}$,
or ${f(x)\bowtie y}$, ${y\bowtie y}$, for $A$ a context $\mathcal{P}$-term and
${{\bowtie}\in\\{\hskip 0.29999pt{\approx},\;{\not\approx}\hskip
0.29999pt\\}}$. A _context clause_ is a clause with only function-free context
atoms in the body, and only context literals in the head.

Definition 2 introduces sets $\mathsf{Su}(\mathcal{O})$ and
$\mathsf{Pr}(\mathcal{O})$, that identify the information that must be
exchanged between adjacent contexts. Intuitively, $\mathsf{Su}(\mathcal{O})$
contains atoms that are of interest to a context’s successor, and it guides
the $\mathsf{Succ}$ rule whereas $\mathsf{Pr}(\mathcal{O})$ contains atoms
that are of interest to a context’s predecessor and it guides the
$\mathsf{Pred}$ rule.

######  Definition 2.

The set $\mathsf{Su}(\mathcal{O})$ of _successor triggers_ of an ontology
$\mathcal{O}$ is the smallest set of atoms such that, for each clause
${\Gamma\rightarrow\Delta\in\mathcal{O}}$,

  * •

${B(x)\in\Gamma}$ implies ${B(x)\in\mathsf{Su}(\mathcal{O})}$,

  * •

${S(x,z_{i})\in\Gamma}$ implies ${S(x,y)\in\mathsf{Su}(\mathcal{O})}$, and

  * •

${S(z_{i},x)\in\Gamma}$ implies ${S(y,x)\in\mathsf{Su}(\mathcal{O})}$.

The set $\mathsf{Pr}(\mathcal{O})$ of _predecessor triggers_ of $\mathcal{O}$
is defined as

$\begin{array}[]{@{}r@{\;}l@{}}\mathsf{Pr}(\mathcal{O})=&\\{\,A\\{{x\mapsto
y,\;y\mapsto x}\\}\mid A\in\mathsf{Su}(\mathcal{O})\,\\}\;\cup\\\
&\\{\,B(y)\mid B\text{ occurs in }\mathcal{O}\,\\}.\end{array}$

As in resolution, we restrict the inferences using a term order $\succ$.
Definition 3 specifies the conditions that the order must satisfy. Items 1 and
2 ensure that $\mathcal{F}$-terms are compared uniformly across contexts;
however, $\mathcal{P}$-terms can be compared in different ways in different
contexts. Items 1, 2, 3 and 4 ensure that, if we ground the order by mapping
$x$ to a term $t$ and $y$ to the predecessor of $t$, we obtain a
_simplification order_ (?)—a kind of term order commonly used in equational
theorem proving. Finally, Item 5 ensures that atoms that might be propagated
to a context’s predecessor via the $\mathsf{Pred}$ rule are smallest, which is
important for completeness.

######  Definition 3.

Let $\gtrdot$ be a total, well-founded order on function symbols. A _context
term order_ $\succ$ is an order on context terms satisfying the following
conditions:

  1. 1.

for each ${f\in\mathcal{F}}$, we have ${f(x)\succ x\succ y}$;

  2. 2.

for all ${f,g\in\mathcal{F}}$ with ${f\gtrdot g}$, we have ${f(x)\succ g(x)}$;

  3. 3.

for all terms $s_{1}$, $s_{2}$, and $t$ and each position $p$ in $t$, if
${s_{1}\succ s_{2}}$, then ${t[s_{1}]_{p}\succ t[s_{2}]_{p}}$;

  4. 4.

for each term $s$ and each proper position $p$ in $s$, we have ${s\succ
s|_{p}}$; and

  5. 5.

for each atom ${A\approx\wp\in\mathsf{Pr}(\mathcal{O})}$ and each context term
${s\not\in\\{\hskip 0.29999ptx,y\hskip 0.29999pt\\}}$, we have ${A\not\succ
s}$.

Each term order is extended to a literal order, also written $\succ$, as
described in Section 2.

A lexicographic path order (LPO) (?) over context $\mathcal{F}$-terms and
context $\mathcal{P}$-terms, in which $x$ and $y$ are treated as constants
such that ${x\succ y}$, satisfies Items 1, 2, 3 and 4. Furthermore,
$\mathsf{Pr}(\mathcal{O})$ contains only atoms of the form $B(y)$, $S(x,y)$,
and $S(y,x)$, which we can always make smallest in the ordering; thus, Item 5
does not contradict the other conditions. Hence, an LPO that is relaxed for
Item 5 satisfies Definition 3, and thus, for any given $\gtrdot$, at least one
context term order exists.

Apart from orders, effective redundancy elimination techniques are critical to
efficiency of resolution calculi. Definition 4 defines a notion compatible
with our setting.

######  Definition 4.

A set of clauses $U$ _contains a clause_ ${\Gamma\rightarrow\Delta}$ _up to
redundancy_ , written ${\Gamma\rightarrow\Delta\mathrel{\hat{\in}}U}$, if

  1. 1.

${\\{s\approx s^{\prime},\;s\not\approx s^{\prime}\\}\subseteq\Delta}$ or
${s\approx s\in\Delta}$ for some terms $s$ and $s^{\prime}$, or

  2. 2.

${\Gamma^{\prime}\subseteq\Gamma}$ and ${\Delta^{\prime}\subseteq\Delta}$ for
some clause ${\Gamma^{\prime}\rightarrow\Delta^{\prime}\in U}$.

Intuitively, if $U$ contains ${\Gamma\rightarrow\Delta}$ up to redundancy,
then adding ${\Gamma\rightarrow\Delta}$ to $U$ will not modify the constraints
that $U$ represents because either ${\Gamma\rightarrow\Delta}$ is a tautology
or $U$ contains a stronger clause. Note that tautologies of the form
${A\rightarrow A}$ are _not_ redundant in our setting as they are used to
initialise contexts; however, whenever our calculus derives a clause
${A\rightarrow A\vee A^{\prime}}$, the set of clauses will have been
initialised with ${A\rightarrow A}$, which makes the former clause redundant
by Item 2 of Definition 4. Moreover, clause heads are subjected to the usual
tautology elimination rules; thus, clauses ${\gamma\rightarrow\Delta\vee
s\approx s}$ and ${\Gamma\rightarrow\Delta\vee s\approx t\vee s\not\approx t}$
can be eliminated. Proposition 1 shows that we can remove from $U$ each clause
$C$ that is contained in ${U\setminus\\{\hskip 0.29999ptC\hskip 0.29999pt\\}}$
up to redundancy; the $\mathsf{Elim}$ uses this to support clause subsumption.

######  Proposition 1.

For $U$ a set of clauses and $C$ and $C^{\prime}$ clauses with
${C\mathrel{\hat{\in}}U\setminus\\{\hskip 0.29999ptC\hskip 0.29999pt\\}}$ and
${C^{\prime}\mathrel{\hat{\in}}U}$, we have
${C^{\prime}\mathrel{\hat{\in}}U\setminus\\{\hskip 0.29999ptC\hskip
0.29999pt\\}}$.

We are finally ready to formalise the notion of a context structure, as well
as a notion of context structure soundness. The latter captures the fact that
context clauses from a set $\mathcal{S}_{v}$ do not contain
$\mathsf{core}_{v}$ in their bodies. We shall later show that our inference
rules preserve context structure soundness, which essentially proves that all
clauses derived by our calculus are indeed conclusions of the ontology in
question.

######  Definition 5.

A _context structure_ for an ontology $\mathcal{O}$ is a tuple
${\mathcal{D}=\langle\mathcal{V},\mathcal{E},\mathcal{S},\mathsf{core},\succ\rangle}$,
where $\mathcal{V}$ is a finite set of _contexts_ ,
${\mathcal{E}\subseteq\mathcal{V}\times\mathcal{V}\times\mathcal{F}}$ is a
finite set of edges each labelled with a function symbol, function
$\mathsf{core}$ assigns to each context $v$ a conjunction $\mathsf{core}_{v}$
of atoms over the $\mathcal{P}$-terms from $\mathsf{Su}(\mathcal{O})$,
function $\mathcal{S}$ assigns to each context $v$ a finite set
$\mathcal{S}_{v}$ of context clauses, and function $\succ$ assigns to each
context $v$ a context term order $\succ_{v}$. A context structure
$\mathcal{D}$ is _sound_ for $\mathcal{O}$ if the following conditions both
hold.

  1. S1.

For each context ${v\in\mathcal{V}}$ and each clause
${\Gamma\rightarrow\Delta\in\mathcal{S}_{v}}$, we have
${\mathcal{O}\models\mathsf{core}_{v}\wedge\Gamma\rightarrow\Delta}$.

  2. S2.

For each edge ${\langle u,v,f\rangle\in\mathcal{E}}$, we have

$\mathcal{O}\models\mathsf{core}_{u}\rightarrow\mathsf{core}_{v}\\{{x\mapsto
f(x),y\mapsto x}\\}.$

Table 2: Rules of the Consequence-Based Calculus $\mathsf{Core}$ rule
---
If |  $A\in\mathsf{core}_{v}$,
| and $\top\rightarrow A\notin\mathcal{S}_{v}$,
then | add $\top\rightarrow A$ to $\mathcal{S}_{v}$.
$\mathsf{Hyper}$ rule
If |  $\bigwedge_{i=1}^{n}A_{i}\rightarrow\Delta\in\mathcal{O}$,
|  $\sigma$ is a substitution such that $\sigma(x)=x$,
|  $\Gamma_{i}\rightarrow\Delta_{i}\vee A_{i}\sigma\in\mathcal{S}_{v}$ s.t.
$\Delta_{i}\not\succeq_{v}A_{i}\sigma$ for $1\leq i\leq n$,
| and
$\bigwedge_{i=1}^{n}\Gamma_{i}\rightarrow\Delta\sigma\vee\bigvee_{i=1}^{n}\Delta_{i}\not\mathrel{\hat{\in}}\mathcal{S}_{v}$,
then | add $\bigwedge_{i=1}^{n}\Gamma_{i}\rightarrow\Delta\sigma\vee\bigvee_{i=1}^{n}\Delta_{i}$ to $\mathcal{S}_{v}$.
$\mathsf{Eq}$ rule
If |  $\Gamma_{1}\rightarrow\Delta_{1}\vee s_{1}\approx t_{1}\in\mathcal{S}_{v}$,
|  $s_{1}\succ_{v}t_{1}$ and $\Delta_{1}\not\succeq_{v}s_{1}\approx t_{1}$,
|  $\Gamma_{2}\rightarrow\Delta_{2}\vee s_{2}\bowtie t_{2}\in\mathcal{S}_{v}$
with ${\bowtie}\in\\{\hskip 0.29999pt\approx,\not\approx\hskip 0.29999pt\\}$,
|  $s_{2}\succ_{v}t_{2}$ and $\Delta_{2}\not\succeq_{v}s_{2}\bowtie t_{2}$,
|  $s_{2}|_{p}=s_{1}$,
| and $\Gamma_{1}\wedge\Gamma_{2}\rightarrow\Delta_{1}\vee\Delta_{2}\vee
s_{2}[t_{1}]_{p}\bowtie t_{2}\not\mathrel{\hat{\in}}\mathcal{S}_{v}$,
then | add $\Gamma_{1}\wedge\Gamma_{2}\rightarrow\Delta_{1}\vee\Delta_{2}\vee s_{2}[t_{1}]_{p}\bowtie t_{2}$ to $\mathcal{S}_{v}$.
$\mathsf{Ineq}$ rule
If | $\Gamma\rightarrow\Delta\vee t\not\approx t\in\mathcal{S}_{v}$
| and $\Gamma\rightarrow\Delta\not\mathrel{\hat{\in}}\mathcal{S}_{v}$,
then | add $\Gamma\rightarrow\Delta$ to $\mathcal{S}_{v}$.
$\mathsf{Factor}$ rule
If |  $\Gamma\rightarrow\Delta\vee s\approx t\vee s\approx t^{\prime}\in\mathcal{S}_{v}$,
|  $\Delta\cup\\{\hskip 0.29999pts\approx t\hskip
0.29999pt\\}\not\succeq_{v}s\approx t^{\prime}$ and $s\succ_{v}t^{\prime}$
| and $\Gamma\rightarrow\Delta\vee t\not\approx t^{\prime}\vee s\approx
t^{\prime}\not\mathrel{\hat{\in}}\mathcal{S}_{v}$,
then | add $\Gamma\rightarrow\Delta\vee t\not\approx t^{\prime}\vee s\approx t^{\prime}$ to $\mathcal{S}_{v}$.
$\mathsf{Elim}$ rule
If |  $\Gamma\rightarrow\Delta\in\mathcal{S}_{v}$ and
| $\Gamma\rightarrow\Delta\mathrel{\hat{\in}}\mathcal{S}_{v}\setminus\\{\hskip
0.29999pt\Gamma\rightarrow\Delta\hskip 0.29999pt\\}$
then | remove $\Gamma\rightarrow\Delta$ from $\mathcal{S}_{v}$.
$\mathsf{Pred}$ rule
If |  $\langle u,v,f\rangle\in\mathcal{E}$,
|
$\bigwedge_{i=1}^{l}A_{i}\rightarrow\bigvee_{i=l+1}^{l+n}A_{i}\in\mathcal{S}_{v}$,
|  $\Gamma_{i}\rightarrow\Delta_{i}\vee A_{i}\sigma\in\mathcal{S}_{u}$ s.t.
$\Delta_{i}\not\succeq_{u}A_{i}\sigma$ for $1\leq i\leq l$,
|  $A_{i}\in\mathsf{Pr}(\mathcal{O})$ for each $l+1\leq i\leq l+n$,
| and
$\bigwedge_{i=1}^{l}\Gamma_{i}\rightarrow\bigvee_{i=1}^{l}\Delta_{i}\vee\bigvee_{i=l+1}^{l+n}A_{i}\sigma\not\mathrel{\hat{\in}}\mathcal{S}_{u}$,
then | add $\bigwedge_{i=1}^{l}\Gamma_{i}\rightarrow\bigvee_{i=1}^{l}\Delta_{i}\vee\bigvee_{i=l+1}^{l+n}A_{i}\sigma$ to $\mathcal{S}_{u}$,
where |  $\sigma=\\{{x\mapsto f(x),y\mapsto x}\\}$.
$\mathsf{Succ}$ rule
If |  $\Gamma\rightarrow\Delta\vee A\in\mathcal{S}_{u}$ s.t. $\Delta\not\succeq_{u}A$ and $A$ contains $f(x)$,
| and, for each $A^{\prime}\in K_{2}\setminus\mathsf{core}_{v}$, no edge
$\langle u,v,f\rangle\in\mathcal{E}$
| exists such that $A^{\prime}\rightarrow
A^{\prime}\mathrel{\hat{\in}}\mathcal{S}_{v}$,
then | let $\langle v,\mathsf{core}^{\prime},\succ^{\prime}\rangle:=\mathsf{strategy}(f,K_{1},\mathcal{D})$;
| if $v\in\mathcal{V}$, then let
${\succ_{v}}:={\succ_{v}}\cap{\succ^{\prime}}$, and
| otherwise let $\mathcal{V}:=\mathcal{V}\cup\\{\hskip 0.29999ptv\hskip
0.29999pt\\}$, ${\succ_{v}}:={\succ^{\prime}}$,
|  otherwise let $\mathsf{core}_{v}:={\mathsf{core}^{\prime}}$, and
$\mathcal{S}_{v}:=\emptyset$;
| add the edge $\langle u,v,f\rangle$ to $\mathcal{E}$; and
| add $A^{\prime}\rightarrow A^{\prime}$ to $\mathcal{S}_{v}$ for each
$A^{\prime}\in K_{2}\setminus\mathsf{core}_{v}$;
where |  $\sigma=\\{{x\mapsto f(x),y\mapsto x}\\}$,
|  $K_{1}=\\{\,A^{\prime}\in\mathsf{Su}(\mathcal{O})\mid\top\rightarrow
A^{\prime}\sigma\in\mathcal{S}_{u}\,\\}$, and
|
$K_{2}=\\{\,A^{\prime}\in\mathsf{Su}(\mathcal{O})\mid\Gamma^{\prime}\rightarrow\Delta^{\prime}\vee
A^{\prime}\sigma\in\mathcal{S}_{u}$ and
|  $\Delta^{\prime}\not\succeq_{u}A^{\prime}\sigma\,\\}$.

Definition 6 introduces an expansion strategy—a parameter of our calculus that
determines when and how to reuse contexts in order to satisfy existential
restrictions.

######  Definition 6.

An _expansion strategy_ is a function $\mathsf{strategy}$ that takes a
function symbol $f$, a set of atoms $K$, and a context structure
${\mathcal{D}=\langle\mathcal{V},\mathcal{E},\mathcal{S},\mathsf{core},\succ\rangle}$.
The result of $\mathsf{strategy}(f,K,\mathcal{D})$ is computable in polynomial
time and it is a triple $\langle
v,\mathsf{core}^{\prime},\succ^{\prime}\rangle$ where $\mathsf{core}^{\prime}$
is a subset of $K$; either ${v\notin\mathcal{V}}$ is a fresh context, or
${v\in\mathcal{V}}$ is an existing context in $\mathcal{D}$ such that
${\mathsf{core}_{v}=\mathsf{core}^{\prime}}$; and $\succ^{\prime}$ is a
context term order.

? (?) presented two basic strategies, which we can adapt to our setting as
follows.

  * •

The _eager_ strategy returns for each $K_{1}$ the context $v_{K_{1}}$ with
core $K_{1}$. The ‘kind’ of ground terms that $v_{K_{1}}$ represents is then
very specific so the set $\mathcal{S}_{v_{K_{1}}}$ is likely to be smaller,
but the number of contexts can be exponential.

  * •

The _cautious_ strategy examines the function symbol $f$: if $f$ occurs in
$\mathcal{O}$ in exactly one atom of the form $B(f(x))$ and if ${B(x)\in
K_{1}}$, then the result is the context $v_{B(x)}$ with core $B(x)$;
otherwise, the result is the ‘trivial’ context $v_{\top}$ with the empty core.
Context $v_{B(x)}$ is then less constrained, but the number of contexts is at
most linear.

? (?) discuss extensively the differences between and the relative merits of
the two strategies; although their discussion deals with $\mathcal{ALCI}$
only, their conclusions apply to $\mathcal{SRIQ}$ as well.

We are now ready to show soundness and completeness.

######  Theorem 1 (Soundness).

For any expansion strategy, applying an inference rule from Table 2 to an
ontology $\mathcal{O}$ and a context structure $\mathcal{D}$ that is sound for
$\mathcal{O}$ produces a context structure that is sound for $\mathcal{O}$.

######  Theorem 2 (Completeness).

Let $\mathcal{O}$ be an ontology, and let
${\mathcal{D}=\langle\mathcal{V},\mathcal{E},\mathcal{S},\mathsf{core},\succ\rangle}$
be a context structure such that no inference rule from Table 2 is applicable
to $\mathcal{O}$ and $\mathcal{D}$. Then,
${\Gamma_{Q}\rightarrow\Delta_{Q}\mathrel{\hat{\in}}\mathcal{S}_{q}}$ holds
for each query clause ${\Gamma_{Q}\rightarrow\Delta_{Q}}$ and each context
${q\in\mathcal{V}}$ that satisfy conditions C1–C3.

  1. C1.

${\mathcal{O}\models\Gamma_{Q}\rightarrow\Delta_{Q}}$.

  2. C2.

For each atom ${A\approx\wp\in\Delta_{Q}}$ and each context term
${s\not\in\\{\hskip 0.29999ptx,y\hskip 0.29999pt\\}}$, if ${A\succ_{q}s}$,
then ${s\approx\wp\in\Delta_{Q}\cup\mathsf{Pr}(\mathcal{O})}$.

  3. C3.

For each ${A\in\Gamma_{Q}}$, we have ${\Gamma_{Q}\rightarrow
A\mathrel{\hat{\in}}\mathcal{S}_{q}}$.

Conditions C2 and C3 can be satisfied by appropriately initialising the
corresponding context. Hence, Theorems 1 and 2 show that the following
algorithm is sound and complete for deciding
${\mathcal{O}\models\Gamma_{Q}\rightarrow\Delta_{Q}}$.

  1. A1.

Create an empty context structure $\mathcal{D}$ and select an expansion
strategy.

  2. A2.

Introduce a context $q$ into $\mathcal{D}$; set
${\mathsf{core}_{q}=\Gamma_{Q}}$; for each ${A\in\Gamma_{Q}}$, add
${\top\rightarrow A}$ to $\mathcal{S}_{q}$ to satisfy condition C3; and
initialise $\succ_{q}$ in a way that satisfies condition C2.

  3. A3.

Apply the inference rules from Table 2 to $\mathcal{D}$ and $\mathcal{O}$.

  4. A4.

${\Gamma_{Q}\rightarrow\Delta_{Q}}$ holds if and only if
${\Gamma_{Q}\rightarrow\Delta_{Q}\mathrel{\hat{\in}}\mathcal{S}_{v}}$.

Propositions 2 and 3 show that our calculus is worst-case optimal for both
$\mathcal{ALCHIQ}$ and $\mathcal{ELH}$.

######  Proposition 2.

For each expansion strategy that introduces at most exponentially many
contexts, algorithm A1–A4 runs in worst-case exponential time.

######  Proposition 3.

For $\mathcal{ELH}$ ontologies and queries of the form ${B_{1}(x)\rightarrow
B_{2}(x)}$, algorithm A1–A4 runs in polynomial time with either the cautious
or the eager strategy; and with the cautious strategy and the $\mathsf{Hyper}$
rule applied eagerly, the inferences in step A3 correspond directly to the
inferences of the $\mathcal{ELH}$ calculus by ? (?).

###  4.2 An Outline of the Completeness Proof

To prove Theorem 2, we fix an ontology $\mathcal{O}$, a context structure
$\mathcal{D}$, a query clause ${\Gamma_{Q}\rightarrow\Delta_{Q}}$, and a
context $q$ such that properties C2 and C3 of Theorem 2 are satisfied and
${\Gamma_{Q}\rightarrow\Delta_{Q}\not\mathrel{\hat{\in}}\mathcal{S}_{q}}$
holds, and we construct a Herbrand interpretation that satisfies $\mathcal{O}$
but refutes ${\Gamma_{Q}\rightarrow\Delta_{Q}}$. We reuse techniques from
equational theorem proving (?) and represent this interpretation by a _rewrite
system_ $R$—a finite set of rules of the form ${l\Rightarrow r}$. Intuitively,
such a rule says that that any two terms of the form ${f_{1}(\dots
f_{n}(l)\dots)}$ and ${f_{1}(\dots f_{n}(r)\dots)}$ with ${n\geq 0}$ are
equal, and that we can prove this equality in one step by rewriting (i.e.,
replacing) $l$ with $r$. Rewrite system $R$ induces a Herbrand equality
interpretation $R^{*}$ that contains each ${l\approx r}$ for which the
equality between $l$ and $r$ can be verified using a finite number of such
rewrite steps. The universe of $R^{*}$ consists of $\mathcal{F}$\- and
$\mathcal{P}$-terms constructed using the symbols in $\mathcal{F}$ and
$\mathcal{P}$, and a special constant $c$; for convenience, let $\mathcal{T}$
be the set of all $\mathcal{F}$-terms from this universe.

We obtain $R$ by unfolding the context structure $\mathcal{D}$ starting from
context $q$: we map each $\mathcal{F}$-term ${t\in\mathcal{T}}$ to a context
$X_{t}$ in $\mathcal{D}$, and we use the clauses in $\mathcal{S}_{X_{t}}$ to
construct a model fragment $R_{t}$—the part of $R$ that satisfies the DL-
clauses of $\mathcal{O}$ when $x$ is mapped to $t$. The key issue is to ensure
compatibility between adjacent model fragments: when moving from a
_predecessor_ term $t^{\prime}$ to a _successor_ term ${t=f(t^{\prime})}$, we
must ensure that adding $R_{t}$ to $R_{t^{\prime}}$ does not affect the truth
of the DL-clauses of $\mathcal{O}$ at term $t^{\prime}$; in other words, the
model fragment constructed at $t$ must respect the choices made at
$t^{\prime}$. We represent these choices by a ground clause
${\Gamma_{t}\rightarrow\Delta_{t}}$: conjunction $\Gamma_{t}$ contains atoms
that are ‘inherited’ from $t^{\prime}$ and so must hold at $t$, and
disjunction $\Delta_{t}$ contains atoms that must not hold at $t$ because
$t^{\prime}$ relies on their absence.

The model fragment construction takes as parameters a term $t$, a context
${v=X_{t}}$, and a clause ${\Gamma_{t}\rightarrow\Delta_{t}}$. Let $N_{t}$ be
the set of ground clauses obtained from $\mathcal{S}_{v}$ by mapping $x$ to
$t$ and $y$ to the predecessor of $t$ (if it exists), and whose body is
contained in $\Gamma_{t}$. Moreover, let $\mathsf{Su}_{t}$ and
$\mathsf{Pr}_{t}$ be obtained from $\mathsf{Su}(\mathcal{O})$ and
$\mathsf{Pr}(\mathcal{O})$ by mapping $x$ to $t$ and $y$ to the predecessor of
$t$ if one exists; thus, $\mathsf{Su}_{t}$ contains the ground atoms of
interest to the successors of $t$, and $\mathsf{Pr}_{t}$ contains the ground
atoms of interest to the predecessor of $t$. The model fragment for $t$ can be
constructed if properties L1–L3 hold:

  1. L1.

${\Gamma_{t}\rightarrow\Delta_{t}\not\mathrel{\hat{\in}}N_{t}}$.

  2. L2.

If ${t=c}$, then ${\Delta_{t}=\Delta_{Q}}$; and if ${t\neq c}$, then
${\Delta_{t}\subseteq\mathsf{Pr}_{t}}$.

  3. L3.

For each ${A\in\Gamma_{t}}$, we have ${\Gamma_{t}\rightarrow
A\mathrel{\hat{\in}}N_{t}}$.

The construction produces a rewrite system $R_{t}$ such that

  1. F1.

${R_{t}^{*}\\!\models N_{t}}$, and

  2. F2.

${R_{t}^{*}\\!\not\models\Gamma_{t}\rightarrow\Delta_{t}}$—that is, all of
$\Gamma_{t}$, but none of $\Delta_{t}$ hold in $R_{t}^{*}$, and so the model
fragment at $t$ is compatible with the ‘inherited’ constraints.

We construct rewrite system $R_{t}$ by adapting the techniques from
paramodulation-based theorem proving. First, we order all clauses in $N_{t}$
into a sequence ${C^{i}=\Gamma^{i}\rightarrow\Delta^{i}\vee L^{i}}$, ${1\leq
i\leq n}$, that is compatible with the context ordering $\succ_{v}$ in a
particular way. Next, we initialise $R_{t}$ to $\emptyset$, and then we
examine each clause $C^{i}$ in this sequence; if $C^{i}$ does not hold in the
model constructed thus far, we make the clause true by adding $L^{i}$ to
$R_{t}$. To prove Item F1, we assume for the sake of a contradiction that a
clause $C^{i}$ with smallest $i$ exists such that ${R_{t}^{*}\\!\not\models
C^{i}}$, and we show that an application of the $\mathsf{Eq}$,
$\mathsf{Ineq}$, or $\mathsf{Factor}$ rule to $C^{i}$ necessarily produces a
clause $C^{j}$ such that ${R_{t}^{*}\\!\not\models C^{j}}$ and ${j<i}$. Items
L1, L2 and L3 allow us to satisfy Item F2. Due to Item L2 and Item 5 of
Definition 3, we can order the clauses in the sequence such that each clause
$C^{i}$ capable of producing an atom from $\Delta_{t}$ comes before any other
clause in the sequence; and then we use Item L1 to show that no such clause
actually exists. Moreover, Item L3 ensures that all atoms in $\Gamma_{t}$ are
actually produced in $R_{t}^{*}$.

To obtain $R$, we inductively unfold $\mathcal{D}$, and at each step we apply
the model fragment construction to the appropriate parameters. For the base
case, we map constant $c$ to context ${X_{c}=q}$, and we define
${\Gamma_{c}=\Gamma_{Q}}$ and ${\Delta_{c}=\Delta_{Q}}$; then, Items L1 and L2
hold by definition, and Item L3 holds by property C3 of Theorem 2. For the
induction step, we assume that we have already mapped some term $t^{\prime}$
to a context ${u=X_{t^{\prime}}}$, and we consider term $t=f(t^{\prime})$ for
each ${f\in\mathcal{F}}$.

  * •

If $t$ does not occur in an atom in $R_{t^{\prime}}$, we let ${R_{t}=\\{\hskip
0.29999ptt\Rightarrow c\hskip 0.29999pt\\}}$ and thus make $t$ equal to $c$.
Term $t$ is thus interpreted in exactly the same way as $c$, so we stop the
unfolding.

  * •

If $R_{t^{\prime}}$ contains a rule ${t\Rightarrow s}$, then $t$ and $s$ are
equal, and so we interpret $t$ exactly as $s$; hence, we stop the unfolding.

  * •

In all other cases, the $\mathsf{Succ}$ rule ensures that $\mathcal{D}$
contains an edge ${\langle u,v,f\rangle}$ such that $v$ satisfies all
preconditions of the rule, so we define ${X_{t}=v}$. Moreover, we let
${\Gamma_{t}=R_{t^{\prime}}^{*}\cap\mathsf{Su}_{t}}$ be the set of atoms that
hold at $t^{\prime}$ and are relevant to $t$ , and we let
${\Delta_{t}=\mathsf{Pr}_{t}\setminus R_{t^{\prime}}^{*}}$ be the set of atoms
that do not hold at $t^{\prime}$ and are relevant to $t$. We finally show that
such $\Gamma_{t}$ and $\Delta_{t}$ satisfy Item L1: otherwise, the
$\mathsf{Pred}$ rule derives a clause in $N_{t^{\prime}}$ that is not true in
$R_{t^{\prime}}^{*}$.

After processing all relevant terms, we let $R$ be the union of all $R_{t}$
from the above construction. To show that $R^{*}$ satisfies $\mathcal{O}$, we
consider a DL-clause ${\Gamma\rightarrow\Delta\in\mathcal{O}}$ and a
substitution $\tau$ that makes the clause ground. W.l.o.g. we can assume that
$\tau$ is irreducible by $R$—that is, it does not contain terms that can we
rewritten using the rules in $R$. Since each model fragment satisfies Item F2,
we can evaluate ${\Gamma\tau\rightarrow\Delta\tau}$ in $R_{\tau(x)}^{*}$
instead of $R^{*}$. Moreover, we show that
${R_{\tau(x)}^{*}\\!\models\Gamma\tau\rightarrow\Delta\tau}$ holds: if that
were not the case, the $\mathsf{Hyper}$ rule derives a clause in $N_{\tau(x)}$
that violates Item F1. Finally, we show that the same holds for the query
clause ${\Gamma_{Q}\rightarrow\Delta_{Q}}$, which completes our proof.

##  5 Evaluation

$100$$200$$300$$400$$500$$600$$700$$10^{2}$$10^{3}$$10^{4}$$10^{5}$Classification
time (ms).HermiTPelletFaCT++KoncludeSequoia Figure 3: Classification Times for
All Ontologies HPFKSHPFKSHPFKSHPFKS$0$%$25$%$50$%$75$%$100$%ProfileHornNo
EqualityWith EqualityEasy categoryMedium categoryHard category Figure 4:
Percentage of Easy, Medium and Hard Ontologies per Ontology Group for HermiT
(H), Pellet (P), FaCT++ (F), Konclude (K), and Sequoia (S)

We have implemented our calculus in a prototype system called Sequoia. The
calculus was implemented exactly as presented in this paper, with no
optimisation other than a suitable indexing scheme for clauses. The system is
written in Scala, and it can be used via the command line or the OWL API. It
currently handles the $\mathcal{SRIQ}$ subset of OWL 2 DL (i.e., it does not
support datatypes, nominals, or reflexive roles), for which it supports
ontology classification and concept satisfiability; other standard services
such as ABox realisation are currently not supported.

We have evaluated our system using the methodology by ? (?) by comparing
Sequoia with HermiT 1.3.8, Pellet 2.3.1, FaCT++ 1.6.4, and Konclude 1.6.1. We
used all reasoners in single-threaded mode in order to compare the underlying
calculi; moreover, Sequoia was configured to use the cautious strategy. All
systems, ontologies, and test results are available online.111http://krr-
nas.cs.ox.ac.uk/2015/KR/cr/

We used the Oxford Ontology
Repository222http://www.cs.ox.ac.uk/isg/ontologies/ from which we excluded 7
ontologies with irregular RBoxes. Since Sequoia does not support datatypes or
nominals, we have systematically replaced datatypes and nominals with fresh
classes and data properties with object properties, and we have removed ABox
assertions. We thus obtained a corpus of 777 ontologies on which we tested all
reasoners.

We run our experiments on a Dell workstation with two Intel Xeon E5-2643 v3
3.4 GHz processors with 6 cores per processor and 128 GB of RAM running
Windows Server 2012 R2. We used Java 8 update 66 with 15 GB of heap memory
allocated to each Java reasoner, and a maximum private working set size of 15
GB for each reasoner in native code. In each test, we measured the wall-clock
classification time; this excludes parsing time for reasoners based on the OWL
API (i.e., HermiT, Pellet, FaCT++, and Sequoia). Each test was given a timeout
of 5 minutes. We report the average time over three runs, unless an exception
or timeout occurred in one of the three runs, in which case we report failure.

Figure 3 shows an overview of the classification times for the entire corpus.
The $y$-axis shows the classification times in logarithmic scale, and timeouts
are shown as infinity. A number $n$ on the $x$-axis represents the $n$-th
easiest ontology for a reasoner with ontologies sorted (for that reasoner) in
the ascending order of classification time. For example, a point (50, 100) on
a reasoner’s curve means that the 50th easiest ontology for that reasoner took
100 ms to classify.

Sequoia could process most ontologies (733 out of 784) in under 10s, which is
consistent with the other reasoners. The system was fairly robust, failing on
only 22 ontologies; in contrast, HermiT failed on 42, Pellet on 138, FaCT++ on
132, and Konclude on 8 ontologies. Moreover, Sequoia succeeded on 21
ontologies on which all of HermiT, Pellet and FaCT++ failed. Finally, there
was one ontology where Sequoia succeeded and all other reasoners failed; this
was a hard version of FMA (ID $00285$) that uses both disjunctions and number
restrictions.

Figure 4 shows an overview of how each reasoner performed on each type of
ontology. We partitioned the ontologies in the following four groups: within a
profile of OWL 2 DL (i.e., captured by OWL 2 EL, QL, or RL); Horn but not in a
profile; disjunctive but without number restrictions; and disjunctive and with
number restrictions. We used the OWL API to determine profile membership, and
we identified the remaining three groups after structural transformation. In
addition, for each reasoner, we categorise each ontology as either ‘easy’
($<10$s), ‘medium’ ($10$s to $5$min), and ‘hard’ (timeout or exception). The
figure depicts a bar for each reasoner and group, where each bar is divided
into blocks representing the percentage of ontologies in each of the
aforementioned categories of difficulty. For Sequoia, over $98\%$ of profile
ontologies and over $91\%$ of out-of-profile Horn ontologies are easy, with
the remainder being of medium difficulty. Sequoia timed out largely on
ontologies containing both disjunctions and equality, and even in this case
only Konclude timed out in fewer cases.

In summary, although only an early prototype, Sequoia is a competitive
reasoner that comfortably outperforms HermiT, Pellet, and FaCT++, and which
exhibits a nice pay-as-you-go behaviour. Furthermore, problematic ontologies
seem to mostly contain complex RBoxes or large numbers in cardinality
restrictions, which suggests promising directions for future optimisation.

##  6 Conclusion and Future Work

We have presented the first consequence based calculus for $\mathcal{SRIQ}$—a
DL that includes both disjunction and counting quantifiers. Our calculus
combines ideas from state of the art resolution and (hyper)tableau calculi,
including the use of ordered paramodulation for equality reasoning. Despite
its increased complexity, the calculus mimics existing calculi on
$\mathcal{ELH}$ ontologies. Although it is an early prototype with plenty of
room for optimisation, our system Sequoia is competitive with well-established
reasoners and it exhibits nice pay-as-you-go behaviour in practice.

For future work, we are confident that we can extend the calculus to support
role reflexivity and datatypes, thus handling all of OWL 2 DL except nominals.
In contrast, handling nominals seems to be much more involved. In fact, adding
nominals to $\mathcal{ALCHIQ}$ raises the complexity of reasoning to NExpTime
so a worst-case optimal calculus must be nondeterministic, which is quite
different from all consequence-based calculi we are aware of. Moreover, a
further challenge is to modify the calculus so that it can effectively deal
with large numbers in number restrictions.

## References

  * [1998] Baader, F., and Nipkow, T.  1998\.  Term Rewriting and All That.  Cambridge University Press.
  * [2003] Baader, F.; Calvanese, D.; McGuinness, D.; Nardi, D.; and Patel-Schneider, P. F., eds.  2003\.  The Description Logic Handbook: Theory, Implementation and Applications.  Cambridge University Press.
  * [2005] Baader, F.; Brandt, S.; and Lutz, C.  2005\.  Pushing the $\mathcal{EL}$ Envelope.  In Kaelbling, L. P., and Saffiotti, A., eds., Proc. of the 19th Int. Joint Conference on Artificial Intelligence (IJCAI 2005), 364–369.  Edinburgh, UK: Morgan Kaufmann Publishers.
  * [2001] Bachmair, L., and Ganzinger, H.  2001\.  Resolution Theorem Proving.  In Robinson, A., and Voronkov, A., eds., Handbook of Automated Reasoning, volume I. Elsevier Science.  chapter 2, 19–99.
  * [2014] Glimm, B.; Horrocks, I.; Motik, B.; Stoilos, G.; and Wang, Z.  2014\.  HermiT: An OWL 2 Reasoner.  Journal of Automated Reasoning 53(3):245–269.
  * [2007] Goré, R., and Nguyen, L. A.  2007\.  EXPTIME Tableaux with Global Caching for Description Logics with Transitive Roles, Inverse Roles and Role Hierarchies.  In Olivetti, N., ed., Proc. of the 16th Int. Conf. on Automated Reasoning with Tableaux and Related Methods (TABLEAUX 2007), volume 4548 of LNCS, 133–148.  Aix en Provence, France: Springer.
  * [2008] Kazakov, Y.  2008\.  $\mathcal{RIQ}$ and $\mathcal{SROIQ}$ are Harder than $\mathcal{SHOIQ}$.  In Brewka, G., and Lang, J., eds., Proc. of the 11th Int. Joint Conf. on Principles of Knowledge Representation and Reasoning (KR 2008), 274–284.  Sydney, NSW, Australia: AAAI Press.
  * [2009] Kazakov, Y.  2009\.  Consequence-Driven Reasoning for Horn SHIQ Ontologies.  In Boutilier, C., ed., Proc. of the 21st Int. Joint Conf. on Artificial Intelligence (IJCAI 2009), 2040–2045.
  * [2009] Motik, B.; Shearer, R.; and Horrocks, I.  2009\.  Hypertableau Reasoning for Description Logics.  Journal of Artificial Intelligence Research 36:165–228.
  * [1995] Nieuwenhuis, R., and Rubio, A.  1995\.  Theorem Proving with Ordering and Equality Constrained Clauses.  Journal of Symbolic Computation 19(4):312–351.
  * [2010] Ortiz, M.; Rudolph, S.; and Simkus, M.  2010\.  Worst-Case Optimal Reasoning for the Horn-DL Fragments of OWL 1 and 2\.  In Lin, F.; Sattler, U.; and Truszczynski, M., eds., Proc. of the 12th Int. Conf. on Knowledge Representation and Reasoning (KR 2010), 269–279.  Toronto, ON, Canada: AAAI Press.
  * [2002] Riazanov, A., and Voronkov, A.  2002\.  The design and implementation of VAMPIRE.  AI Communications 15(2–3):91–110.
  * [2002] Schulz, S.  2002\.  E—A Brainiac Theorem Prover.  AI Communications 15(2–3):111–126.
  * [2011] Simančík, F.; Kazakov, Y.; and Horrocks, I.  2011\.  Consequence-Based Reasoning beyond Horn Ontologies.  In Walsh, T., ed., Proc. of the 22nd Int. Joint Conf. on Artificial Intelligence (IJCAI 2011), 1093–1098.
  * [2014] Simančík, F.; Motik, B.; and Horrocks, I.  2014\.  Consequence-Based and Fixed-Parameter Tractable Reasoning in Description Logics.  Artificial Intelligence 209:29–77.
  * [2007] Sirin, E.; Parsia, B.; Cuenca Grau, B.; Kalyanpur, A.; and Katz, Y.  2007\.  Pellet: A practical OWL-DL reasoner.  Journal of Web Semantics 5(2):51–53.
  * [2014] Steigmiller, A.; Glimm, B.; and Liebig, T.  2014\.  Coupling Tableau Algorithms for Expressive Description Logics with Completion-Based Saturation Procedures.  In Demri, S.; Kapur, D.; and Weidenbach, C., eds., Proc. of the 7th Int. Joint Conf. on Automated Reasoning (IJCAR 2014), volume 8562 of LNCS, 449–463.  Vienna, Austria: Springer.
  * [2014] Steigmiller, A.; Liebig, T.; and Glimm, B.  2014\.  Konclude: System description.  Journal of Web Semantics 27:78–85.
  * [2006] Tsarkov, D., and Horrocks, I.  2006\.  FaCT++ Description Logic Reasoner: System Description.  In Proc. of the 3rd Int. Joint Conf. on Automated Reasoning (IJCAR 2006), volume 4130 of LNAI, 292–297.  Seattle, WA, USA: Springer.

##  Appendix A Proof of Theorem 1

In this chapter, we show that our calculus is sound, as stated in Theorem 1.
The proof is analogous to the soundness proof of ordered superposition (?).

See 1

###### Proof.

Let $\mathcal{O}$ be an ontology, let
${\mathcal{D}=\langle\mathcal{V},\mathcal{E},\mathcal{S},\mathsf{core},\succ\rangle}$
be a context structure that is sound for $\mathcal{O}$, and consider an
application of an inference rule from Table 2 to $\mathcal{D}$ and
$\mathcal{O}$. We show that each clause produced by the rule is a context
clause and that it satisfies Items S1 and S2 of Definition 5. Item S1 holds
obviously for the rules different from $\mathsf{Hyper}$, $\mathsf{Eq}$, and
$\mathsf{Pred}$. For Item S2, we rely on soundness of hyperresolution: for
arbitrary formulas $\omega$, $\phi_{i}$, $\psi_{i}$, and $\gamma_{i}$, ${1\leq
i\leq n}$, we have

$\\{\bigwedge_{j=1}^{n}\phi_{j}\rightarrow\omega\\}\cup\bigcup_{1\leq i\leq
n}\\{\gamma_{i}\rightarrow\psi_{i}\vee\phi_{i}\\}\models\bigwedge_{i=1}^{n}\gamma_{i}\rightarrow\bigvee_{i=1}^{n}\psi_{i}\vee\omega.$
(62)

To prove the claim, we consider each rule from Table 2 and assume that the
rule is applied to clauses, contexts, and edges as shown in the table; then,
we show that the clause produced by the rule satisfies Item S1 of Definition
5; moreover, for the $\mathsf{Succ}$ rule, we show in addition that the edge
introduced by the rule satisfies Item S2.

($\mathsf{Core}$) For each ${A\in\mathsf{core}_{v}}$, we clearly have
${\mathcal{O}\models\mathsf{core}_{v}\rightarrow A}$.

($\mathsf{Hyper}$) Since $\mathcal{D}$ is sound for $\mathcal{O}$, we have
${\mathcal{O}\models\mathsf{core}_{v}\wedge\Gamma_{i}\rightarrow\Delta_{i}\vee
A_{i}\sigma}$ for each $i$ with ${1\leq i\leq n}$. By 62, we have
${\mathcal{O}\models\mathsf{core}_{v}\wedge\bigwedge_{i=1}^{n}\Gamma_{i}\rightarrow\bigvee_{i=1}^{n}\Delta_{i}\vee\Delta\sigma}$.
Moreover, substitution $\sigma$ satisfies ${\sigma(x)=x}$, all premises are
context clauses, and $\mathcal{O}$ contains only DL-clauses; thus, the
inference rule can only match an atom $S(x,z_{i})$ or $S(z_{i},x)$ in an
ontology clause to atoms $S(y,x)$, $S(x,y)$, $S(f(x),x)$ or $S(x,f(x))$ in the
context clause, and so $\sigma(z_{i})$ is either $y$ or $f(x)$; thus, the
result is a context clause.

($\mathsf{Eq}$) Since $\mathcal{D}$ is sound for $\mathcal{O}$, properties 63
and 64 hold. Moreover, clause in 65 is a logical consequence of the clauses in
63 and 64, so property 65 holds, as required.

$\displaystyle\mathcal{O}$
$\displaystyle\models\mathsf{core}_{v}\wedge\Gamma_{1}\rightarrow\Delta_{1}\vee
s_{1}\approx t_{1}$ (63) $\displaystyle\mathcal{O}$
$\displaystyle\models\mathsf{core}_{v}\wedge\Gamma_{2}\rightarrow\Delta_{2}\vee
s_{2}\bowtie t_{2}$ (64) $\displaystyle\mathcal{O}$
$\displaystyle\models\mathsf{core}_{v}\wedge\Gamma_{1}\wedge\Gamma_{2}\rightarrow\Delta_{1}\vee\Delta_{2}\vee
s_{2}[t_{1}]_{p}\bowtie t_{2}$ (65)

Finally, term $s_{1}$ is always of the form $g(f(x))$, term $t_{1}$ is of the
form $h(f(x))$ or $y$, and term $s_{2}$ is of the form $g(f(x))$,
$B(g(f(x)))$, $S(f(x),g(f(x)))$, or $S(g(f(x)),f(x))$; thus,
$s_{2}[t_{1}]_{p}$ is a context term, and so the result is a context clause.

($\mathsf{Ineq}$) Since $\mathcal{D}$ is sound for $\mathcal{O}$, we have
${\mathcal{O}\models\mathsf{core}_{v}\wedge\Gamma\rightarrow\Delta\vee
t\not\approx t}$; but then, we clearly have
${\mathcal{O}\models\mathsf{core}_{v}\wedge\Gamma\rightarrow\Delta}$, as
required.

($\mathsf{Factor}$) Since $\mathcal{D}$ is sound for $\mathcal{O}$, property
66 holds. Moreover, clause in 67 is a logical consequence of the clause in 66,
so property 67 holds, as required.

$\displaystyle\mathcal{O}$
$\displaystyle\models\mathsf{core}_{v}\wedge\Gamma\rightarrow\Delta\vee
s\approx t\vee s\approx t^{\prime}$ (66) $\displaystyle\mathcal{O}$
$\displaystyle\models\mathsf{core}_{v}\wedge\Gamma\rightarrow\Delta\vee
t\not\approx t^{\prime}\vee s\approx t^{\prime}$ (67)

($\mathsf{Elim}$) The resulting context structure contains a subset of the
clauses from $\mathcal{D}$, so it is clearly sound for $\mathcal{O}$.

($\mathsf{Pred}$) Let ${\sigma=\\{{x\mapsto f(x),y\mapsto x}\\}}$. Since
$\mathcal{D}$ is sound for $\mathcal{O}$, properties 68–70 hold. Now clause in
71 is an instance of the clause in 68, so property 71 holds. But then, by 62,
properties 68 and 69 imply property 72. Finally, properties 70 and 72 imply
property 73, as required.

$\displaystyle\mathcal{O}$
$\displaystyle\textstyle\models\mathsf{core}_{v}\wedge\bigwedge_{i=1}^{m}A_{i}\rightarrow\bigvee_{j=m+1}^{m+n}A_{j}$
(68) $\displaystyle\mathcal{O}$
$\displaystyle\models\mathsf{core}_{u}\wedge\Gamma_{i}\rightarrow\Delta_{i}\vee
A_{i}\sigma$ $\displaystyle\text{for }1\leq i\leq m$ (69)
$\displaystyle\mathcal{O}$
$\displaystyle\models\mathsf{core}_{u}\rightarrow\mathsf{core}_{v}\sigma$ (70)
$\displaystyle\mathcal{O}$
$\displaystyle\textstyle\models\mathsf{core}_{v}\sigma\wedge\bigwedge_{i=1}^{m}A_{i}\sigma\rightarrow\bigvee_{j=m+1}^{m+n}A_{j}\sigma$
(71) $\displaystyle\mathcal{O}$
$\displaystyle\textstyle\models\mathsf{core}_{v}\sigma\wedge\mathsf{core}_{v}\wedge\bigwedge_{i=1}^{m}\Gamma_{i}\rightarrow\bigvee_{j=m+1}^{m+n}A_{j}\sigma$
(72) $\displaystyle\mathcal{O}$
$\displaystyle\textstyle\models\mathsf{core}_{u}\wedge\bigwedge_{i=1}^{m}\Gamma_{i}\rightarrow\bigvee_{j=m+1}^{m+n}A_{j}\sigma$
(73)

For each ${m+1\leq i\leq m+n}$, we have ${A_{i}\in\mathsf{Pr}(\mathcal{O})}$,
so $A_{i}$ is of the form $B(y)$, $S(x,y)$, or $S(y,x)$; but then, the
definition of $\sigma$ ensures that $A_{i}\sigma$ is a context atom, as
required.

($\mathsf{Succ}$) Let ${\sigma=\\{{x\mapsto f(x),y\mapsto x}\\}}$. For each
clause ${A\rightarrow A}$ added to $\mathcal{S}_{v}$, we clearly have
${\mathcal{O}\models\mathsf{core}_{v}\wedge A\rightarrow A}$, as required for
Item S1 of Definition 5. Moreover, assume that the inference rule adds an edge
$\langle u,v,f_{k}\rangle$ to $\mathcal{E}$; since $\mathcal{D}$ is sound for
$\mathcal{O}$, we have 74; by Definition 6, we have
${\mathsf{core}_{v}\subseteq K_{1}}$.

$\displaystyle\mathcal{O}$ $\displaystyle\models\mathsf{core}_{u}\rightarrow
A\sigma$ $\displaystyle\text{for each }A\in K_{1}$ (74)
$\displaystyle\mathcal{O}$
$\displaystyle\models\mathsf{core}_{u}\rightarrow\mathsf{core}_{v}\sigma$ (75)

But then, property 75 holds, as required for Item S2 of Definition 5. ∎

##  Appendix B Preliminaries: Rewrite Systems

In the proof of Theorem 2 we construct a model of an ontology, which, as is
common in equational theorem proving, we represent using a ground _rewrite
system_. We next recapitulate the definitions of rewrite systems, following
the presentation by ? (?).

Let $\mathcal{T}$ be the set of all ground terms constructed using a
distinguished constant $c$ (of sort $\mathcal{F}$), the function symbols from
$\mathcal{F}$, and the predicate symbols from $\mathcal{P}$. A (ground)
_rewrite system_ $R$ is a binary relation on $\mathcal{T}$. Each pair
${(s,t)\in{R}}$ is called a _rewrite rule_ and is commonly written as
${s\Rightarrow t}$. The _rewrite relation_ $\mathrel{\rightarrow_{R}}$ for $R$
is the smallest binary relation on $\mathcal{T}$ such that, for all terms
${s_{1},s_{2},t\in\mathcal{T}}$ and each (not necessarily proper) position $p$
in $t$, if $s_{1}\Rightarrow s_{2}\in R$, then
$t[s_{1}]_{p}\mathrel{\rightarrow_{R}}t[s_{2}]_{p}$. Moreover,
$\mathrel{\overset{*}{\rightarrow}_{R}}$ is the reflexive–transitive closure
of $\mathrel{\rightarrow_{R}}$, and
$\mathrel{\overset{*}{\leftrightarrow}_{R}}$ is the
reflexive–symmetric–transitive closure of $\mathrel{\rightarrow_{R}}$. A term
$s$ is _irreducible by_ $R$ if no term $t$ exists such that
$s\mathrel{\rightarrow_{R}}t$; and a literal, clause, or substitution $\alpha$
is _irreducible by_ $R$ if no term occurring in $\alpha$ is irreducible by
$R$. Moreover, term $t$ is a _normal form_ of $s$ w.r.t. $R$ if
${s\mathrel{\overset{*}{\leftrightarrow}_{R}}t}$ and $t$ is irreducible by
$R$. We consider the following properties of rewrite systems.

  * •

$R$ is _terminating_ if no infinite sequence ${s_{1},s_{2},\dots}$ of terms
exists such that, for each $i$, we have
${s_{i}\mathrel{\rightarrow_{R}}s_{i+1}}$.

  * •

$R$ is _left-reduced_ if, for each ${s\Rightarrow t\in R}$, the term $s$ is
irreducible by ${R\setminus\\{\hskip 0.29999pts\Rightarrow t\hskip
0.29999pt\\}}$.

  * •

$R$ is _Church-Rosser_ if, for all terms $t_{1}$ and $t_{2}$ such that
${t_{1}\mathrel{\overset{*}{\leftrightarrow}_{R}}t_{2}}$, a term $z$ exists
such that ${t_{1}\mathrel{\overset{*}{\rightarrow}_{R}}z}$ and
${t_{2}\mathrel{\overset{*}{\rightarrow}_{R}}z}$.

If $R$ is terminating and left-reduced, then $R$ is Church-Rosser (?, Theorem
2.1.5 and Exercise 6.7). If $R$ is Church-Rosser, then each term $s$ has a
unique normal form $t$ such that ${s\mathrel{\overset{*}{\rightarrow}_{R}}t}$
holds. The _Herbrand interpretation induced by_ a Church-Rosser system $R$ is
the set $R^{*}$ such that, for all ${s,t\in\mathcal{T}}$, we have ${s\approx
t\in R^{*}}$ if and only if $s\mathrel{\overset{*}{\leftrightarrow}_{R}}t$.

Term orders can be used to prove termination of rewrite systems. A term order
$\succ$ is a _simplification order_ if the following conditions hold:

  * •

for all terms $s_{1}$, $s_{2}$, and $t$, all positions $p$ in $t$, and all
substitutions $\sigma$, we have that ${s_{1}\succ s_{2}}$ implies
${t[s_{1}\sigma]_{p}\succ t[s_{2}\sigma]_{p}}$; and

  * •

for each term $s$ and each proper position $p$ in $s$, we have ${s\succ
s|_{p}}$.

Given a rewrite system $R$, if a simplification order $\succ$ exists such that
${s\Rightarrow t\in R}$ implies ${s\succ t}$, then $R$ is terminating (?,
Theorems 5.2.3 and 5.4.8), and ${s\mathrel{\rightarrow_{R}}t}$ implies
${s\succ t}$.

##  Appendix C Proof of Theorem 2

See 2

In this section, we fix an ontology $\mathcal{O}$, a context structure
${\mathcal{D}=\langle\mathcal{V},\mathcal{E},\mathcal{S},\mathsf{core},\succ\rangle}$,
a context ${q\in\mathcal{V}}$, and a query clause
${\Gamma_{Q}\rightarrow\Delta_{Q}}$ such that conditions C3 and C2 of Theorem
2 are satisfied, and we show the contrapositive of condition C1: if
${\Gamma_{Q}\rightarrow\Delta_{Q}\not\mathrel{\hat{\in}}\mathcal{S}_{q}}$,
then ${\mathcal{O}\not\models\Gamma_{Q}\rightarrow\Delta_{Q}}$. To this end,
we construct a rewrite system $R$ such that the induced Herbrand model $R^{*}$
satisfies all clauses in $\mathcal{O}$, but not
${\Gamma_{Q}\rightarrow\Delta_{Q}}$. We construct the model using a
distinguished constant $c$, the unary function symbols from $\mathcal{F}$, and
the unary and binary predicate symbols from $\mathcal{P}_{1}$ and
$\mathcal{P}_{2}$, respectively.

Let $t$ be a term. If $t$ is of the form ${t=f(s)}$, then $s$ is the
_predecessor_ of $t$, and $t$ is a _successor_ of $s$; by these definitions, a
constant has no predecessor. The $\mathcal{F}$-_neighbourhood_ of $t$ is the
set of $\mathcal{F}$-terms containing $t$, $f(t)$ with ${f\in\mathcal{F}}$,
and the predecessor $t^{\prime}$ of $t$ if one exists; the
$\mathcal{P}$-_neighbourhood_ of $t$ contains $\mathcal{P}$-terms $B(t)$,
$S(t,f(t))$, $S(f(t),t)$, $B(f(t))$, and, if $t$ has the predecessor
$t^{\prime}$, also $\mathcal{P}$-terms $S(t^{\prime},t)$, $S(t,t^{\prime})$,
and $B(t^{\prime})$, for all ${B\in\mathcal{P}_{1}}$ and
${S\in\mathcal{P}_{2}}$. Let $\sigma_{\\!{}t}$ be the substitution such that
${\sigma_{\\!{}t}(x)=t}$ and, if $t$ has the predecessor $t^{\prime}$, then
${\sigma_{\\!{}t}(y)=t^{\prime}}$. Finally, for each term $t$, we define sets
of atoms $\mathsf{Pr}_{t}$ and $\mathsf{Su}_{t}$ as follows:

$\displaystyle\mathsf{Su}_{t}$ $\displaystyle=\\{\,A\sigma_{\\!{}t}\mid
A\in\mathsf{Su}(\mathcal{O})\text{ and }A\sigma_{\\!{}t}\text{ is
ground}\,\\}$ (76) $\displaystyle\mathsf{Pr}_{t}$
$\displaystyle=\\{\,A\sigma_{\\!{}t}\mid A\in\mathsf{Pr}(\mathcal{O})\text{
and }A\sigma_{\\!{}t}\text{ is ground}\,\\}$ (77)

###  C.1 Constructing a Model Fragment

In this section, we show how, given a term $t$, we can generate a part of the
model of $\mathcal{O}$ that covers the neighbourhood of $t$. In the rest of
Section C.1, we fix the following parameters to the model fragment generation
process:

  * •

$t$ is a ground $\mathcal{F}$-term,

  * •

$v$ is a context in $\mathcal{D}$,

  * •

$\Gamma_{t}$ is a conjunction of atoms, and

  * •

$\Delta_{t}$ is a disjunction of atoms.

Let $N_{t}$ be the set of ground clauses obtained from $\mathcal{S}_{v}$ as
follows:

$N_{t}=\\{\Gamma\sigma_{\\!{}t}\rightarrow\Delta\sigma_{\\!{}t}\mid\Gamma\rightarrow\Delta\in\mathcal{S}_{v},\text{
both }\Gamma\sigma_{\\!{}t}\text{ and }\Delta\sigma_{\\!{}t}\text{ are ground,
and }\Gamma\sigma_{\\!{}t}\subseteq\Gamma_{t}\\}$

We assume that the following conditions hold.

  1. L1.

${\Gamma_{t}\rightarrow\Delta_{t}\not\mathrel{\hat{\in}}N_{t}}$.

  2. L2.

If ${t=c}$, then ${\Delta_{t}=\Delta_{Q}}$; and if ${t\neq c}$, then
${\Delta_{t}\subseteq\mathsf{Pr}_{t}}$.

  3. L3.

For each ${A\in\Gamma_{t}}$, we have ${\Gamma_{t}\rightarrow
A\mathrel{\hat{\in}}N_{t}}$.

We next construct a rewrite system $R_{t}$ such that ${R_{t}^{*}\models
N_{t}}$ and ${R_{t}^{*}\not\models\Gamma_{t}\rightarrow\Delta_{t}}$ holds.
Throughout Section C.1, we treat the terms in the $\mathcal{F}$-neighbourhood
of $t$ as if they were constants. Thus, even though the rewrite system $R$
will contain terms $t$ and $f(t)$, we will not consider terms with further
nesting.

####  C.1.1 Grounding the Context Order

To construct $R_{t}$, we need an order on the terms in the neighbourhood of
$t$ that is compatible with $\succ_{v}$. To this end, let $>_{t}$ be a total,
strict, simplification order on the set of ground terms constructed using the
$\mathcal{F}$-neighbourhood of $t$ and the predicate symbols in $\mathcal{P}$
that satisfies the following conditions for all context terms $s_{1}$ and
$s_{2}$ such that $s_{1}\sigma_{\\!{}t}$ and $s_{2}\sigma_{\\!{}t}$ are both
ground, and where $t^{\prime}$ is the predecessor of $t$ if it exists.

  1. O1.

${s_{1}\succ_{v}s_{2}}$ implies
${s_{1}\sigma_{\\!{}t}>_{t}s_{2}\sigma_{\\!{}t}}$.

  2. O2.

${s_{1}\sigma_{\\!{}t}\approx\wp\in\Delta_{t}}$ and
${s_{1}\sigma_{\\!{}t}>_{t}s_{2}\sigma_{\\!{}t}}$ and
${s_{2}\sigma_{\\!{}t}\not\in\\{\hskip 0.29999ptt,t^{\prime}\hskip
0.29999pt\\}}$ imply ${s_{2}\sigma_{\\!{}t}\approx\wp\in\Delta_{t}}$.

Condition C2 of Theorem 2 and Item 5 of Definition 3 ensure that the order
$\succ_{v}$ on (nonground) context terms can be grounded in a way compatible
with Item L2. Moreover, since in this section we treat all $\mathcal{F}$-terms
as constants, we can make the $\mathcal{P}$-terms of the form $B(t^{\prime})$,
$S(t^{\prime},t)$, and $S(t,t^{\prime})$ smaller than other $\mathcal{F}$\-
and $\mathcal{P}$-terms (i.e., we do not need to worry about defining the
order on the predecessor of $t^{\prime}$ or on the ancestors of $f(t)$). Thus,
at least one such order exists, so in the rest of this section we fix an
arbitrary such order $>_{t}$. We extend $>_{t}$ to ground literals (also
written $>_{t}$) by identifying each ${s\not\approx t}$ with the multiset
${\\{s,s,t,t\\}}$ and each ${s\approx t}$ with the multiset ${\\{s,t\\}}$, and
then comparing the result using the multiset extension of the term order (as
defined in Section 2). Finally, we further extend $>_{t}$ to disjunctions of
ground literals (also written $>_{t}$) by identifying each disjunction
$\bigvee_{i=1}^{n}L_{i}$ with the multiset ${\\{L_{1},\ldots,L_{n}\\}}$ and
then comparing the result using the multiset extension of the literal order.

####  C.1.2 Constructing the Rewrite System $R_{t}$

We arrange all clauses in $N_{t}$ into a sequence ${C^{1},\dots,C^{n}}$. Since
the body of each $C^{i}$ is a subset of $\Gamma_{t}$, no $C^{i}$ can contain
$\bot$ in its head as that would contradict Item L1; thus, we can assume that
each $C^{i}$ is of the form ${C^{i}=\Gamma^{i}\rightarrow\Delta^{i}\vee
L^{i}}$ where ${L^{i}>_{t}\Delta^{i}}$, literal $L^{i}$ is of the form
${L^{i}=l^{i}\bowtie r^{i}}$ with ${{\bowtie}\in\\{\hskip
0.29999pt{\approx},{\not\approx}\hskip 0.29999pt\\}}$, and
${l^{i}\geq_{t}r^{i}}$. For the rest of Section C.1, we reserve $C^{i}$,
$\Gamma^{i}$, $\Delta^{i}$, $L^{i}$, $l^{i}$, and $r^{i}$ for referring to the
(parts of) the clauses in this sequence. Finally, we assume that, for all
${1\leq i<j\leq n}$, we have ${\Delta^{j}\vee L^{j}\geq_{t}\Delta^{i}\vee
L^{i}}$.

We next define the sequence ${R_{t}^{0},\dots,R_{t}^{n}}$ of rewrite systems
by setting ${R_{t}^{0}=\emptyset}$ and defining each $R_{t}^{i}$ with ${1\leq
i\leq n}$ inductively as follows:

  * •

$R_{t}^{i}=R_{t}^{i-1}\cup\\{\hskip 0.29999ptl^{i}\Rightarrow r^{i}\hskip
0.29999pt\\}$ if $L^{i}$ is of the form $l^{i}\approx r^{i}$ such that

    1. R1.

$(R_{t}^{i-1})^{*}\\!\not\models\Delta^{i}\vee l^{i}\approx r^{i}$,

    2. R2.

$l^{i}>_{t}r^{i}$,

    3. R3.

$l^{i}$ is irreducible by $R_{t}^{i-1}$, and

    4. R4.

$s\approx r^{i}\not\in(R_{t}^{i-1})^{*}$ for each $l^{i}\approx
s\in\Delta^{i}$;

  * •

$R_{t}^{i}=R_{t}^{i-1}$ in all other cases.

Finally, let ${R_{t}=R_{t}^{n}}$; we call $R_{t}$ the _model fragment for_
$t$, $v$, $\Gamma_{t}$, and $\Delta_{t}$. Each clause
${C^{i}=\Gamma^{i}\rightarrow\Delta^{i}\vee l^{i}\approx r^{i}}$ that
satisfies the first condition in the above construction is called _generative_
, and the clause is said to _generate_ the rule ${l^{i}\Rightarrow r^{i}}$ in
$R_{t}$.

####  C.1.3 The Properties of the Model Fragment $R_{t}$

######  Lemma 1.

The rewrite system $R_{t}$ is Church-Rosser.

###### Proof.

To see that $R_{t}$ is terminating, simply note that, for each rule
${l\Rightarrow r\in R_{t}}$, Item R2 ensures ${l>_{t}r}$, and that $>_{t}$ is
a simplification order.

To see that $R_{t}$ is left-reduced, consider an arbitrary rule ${l\Rightarrow
r\in R_{t}}$ that is added to $R_{t}$ in step $i$ of the clause sequence. By
Item R3, ${l\Rightarrow r}$ is irreducible by $R_{t}^{i}$. Now consider an
arbitrary rule ${l^{\prime}\Rightarrow r^{\prime}\in R_{t}}$ that is added to
$R_{t}$ at any step $j$ of the construction where ${j>i}$. The definition of
the clause order implies ${l^{\prime}\approx r^{\prime}\geq_{t}l\approx r}$;
since ${l^{\prime}>_{t}r^{\prime}}$ and ${l>_{t}r}$ by Item R2, by the
definition of the literal order we have ${l^{\prime}\geq_{t}l}$. Since
${l\Rightarrow r\in R_{t}^{j-1}}$, Item R3 ensures ${l\neq l^{\prime}}$, and
so we have ${l^{\prime}>_{t}l}$; consequently, $l^{\prime}$ is not a subterm
of $l$, and thus $l$ is irreducible by $R_{t}^{j}$. ∎

######  Lemma 2.

For each ${1\leq i\leq n}$ and each ${l\not\approx r\in\Delta^{i}\vee L^{i}}$,
we have ${(R_{t}^{i-1})^{*}\\!\models l\approx r}$ if and only if
${R_{t}^{*}\\!\models l\approx r}$.

###### Proof.

Consider an arbitrary clause ${C^{i}=\Gamma^{i}\rightarrow\Delta^{i}\vee
L^{i}}$ and an arbitrary inequality ${l\not\approx r\in\Delta^{i}\vee L^{i}}$.
If ${l\approx r\in(R_{t}^{i-1})^{*}}$, then ${R_{t}^{i-1}\subseteq R_{t}}$
implies ${l\approx r\in R_{t}^{*}}$, and so we have ${R_{t}^{*}\\!\models
l\approx r}$, as required. Now assume that ${l\approx
r\not\in(R_{t}^{i-1})^{*}}$. Let $l^{\prime}$ and $r^{\prime}$ be the normal
forms of $l$ and $r$, respectively, w.r.t. $R_{t}^{i-1}$. Now consider an
arbitrary $j$ with ${i\leq j\leq n}$ such that ${l^{j}\Rightarrow r^{j}}$ is
generated by $C^{j}$. We then have ${l^{j}\approx r^{j}>_{t}l\not\approx r}$,
which by the definition of literal order implies
${l^{j}>_{t}l\geq_{t}l^{\prime}}$ and ${l^{j}>_{t}r\geq_{t}r^{\prime}}$; since
$>_{t}$ is a simplification order, $l^{j}$ is a subterm of neither
$l^{\prime}$ nor $r^{\prime}$. Thus, $l^{\prime}$ and $r^{\prime}$ are the
normal forms of $l$ and $r$, respectively, w.r.t. $R_{t}^{j}$, and so we have
${l^{\prime}\approx r^{\prime}\not\in(R_{t}^{j})^{*}}$; but then, we have
${l\approx r\not\in(R_{t}^{j})^{*}}$, as required. ∎

######  Lemma 3.

For each generative clause ${\Gamma^{i}\rightarrow\Delta^{i}\vee l^{i}\approx
r^{i}}$, we have ${R_{t}^{*}\\!\not\models\Delta^{i}}$.

###### Proof.

Consider a generative clause ${C^{i}=\Gamma^{i}\rightarrow\Delta^{i}\vee
l^{i}\approx r^{i}}$ and a literal ${L\in\Delta^{i}}$; Item R1 ensures that
${(R_{t}^{i-1})^{*}\\!\not\models L}$. We next show that
${(R_{t}^{i-1})^{*}\\!\not\models L}$.

Assume that $L$ is of the form ${l\not\approx r}$. Since ${l\not\approx
r\in\Delta^{i}\vee l^{i}\approx r^{i}}$, by Lemma 2 we have
${R_{t}^{*}\\!\not\models L}$, as required.

Assume that $L$ is of the form ${l\approx r}$ with ${l>_{t}r}$. We show by
induction that, for each $j$ with ${i\leq j\leq n}$, we have
${(R_{t}^{j})^{*}\\!\not\models L}$. To this end, we assume that
${(R_{t}^{j-1})^{*}\\!\not\models L}$. If $C^{j}$ is not generational, then
${R_{t}^{j}=R_{t}^{j-1}}$, and so ${(R_{t}^{j})^{*}\\!\not\models L}$. Thus,
assume that $C^{j}$ is generational. We consider the following two cases.

  * •

${l^{j}=l}$. We have the following two subcases.

    * –

${j=i}$. Item R4 then ensures ${r\approx r^{i}\not\in(R_{t}^{i-1})^{*}}$. Let
$r^{\prime}$ and $r^{\prime\prime}$ be the normal forms of $r$ and $r^{i}$,
respectively, w.r.t. $R_{t}^{i-1}$; we have ${r^{\prime}\approx
r^{\prime\prime}\not\in(R_{t}^{i-1})^{*}}$. Moreover,
${l>_{t}r\geq_{t}r^{\prime}}$ and ${l>_{t}r^{i}\geq_{t}r^{\prime\prime}}$
hold; since $>_{t}$ is a simplification order, $l$ is a subterm of neither
$r^{\prime}$ nor $r^{\prime\prime}$; therefore, $r^{\prime}$ and
$r^{\prime\prime}$ are the normal forms of $r$ and $r^{i}$, respectively,
w.r.t. $R_{t}^{i}$, and therefore ${r^{\prime}\approx
r^{\prime\prime}\not\in(R_{t}^{i})^{*}}$. Finally, since ${l\Rightarrow
r^{i}\in R_{t}^{i}}$, term $r^{\prime\prime}$ is the normal form of $l$ w.r.t.
$R_{t}^{i}$, and so ${l\approx r\not\in(R_{t}^{i})^{*}}$.

    * –

${j>i}$. But then, ${l^{j}\approx r^{j}\geq_{t}l^{i}\approx r^{i}>_{t}l\approx
r}$ implies ${l^{j}=l^{i}=l}$. Furthermore, $C^{i}$ is generational, so we
have ${l^{i}\Rightarrow r^{i}\in R_{t}^{j-1}}$. But then, $l^{j}$ is not
irreducible by $R_{t}^{j-1}$, which contradicts Item R3.

  * •

${l^{j}>_{t}l}$. Let $l^{\prime}$ and $r^{\prime}$ be the normal forms of $l$
and $r$, respectively, w.r.t. $R_{t}^{j-1}$. Then, we have
${l^{j}>_{t}l\geq_{t}l^{\prime}}$ and ${l^{j}>_{t}r\geq_{t}r^{\prime}}$; since
$>_{t}$ is a simplification order, $l^{j}$ is a subterm of neither
$l^{\prime}$ nor $r^{\prime}$. Thus, $l^{\prime}$ and $r^{\prime}$ are the
normal forms of $l$ and $r$, respectively, w.r.t. $R_{t}^{j}$, and so
${l^{\prime}\approx r^{\prime}\not\in(R_{t}^{j})^{*}}$; hence, ${l\approx
r\not\in(R_{t}^{j})^{*}}$ holds. ∎

######  Lemma 4.

Let ${\Gamma\rightarrow\Delta}$ be a clause with
${\Gamma\rightarrow\Delta\mathrel{\hat{\in}}N_{t}}$. Then
${R_{t}^{*}\\!\models\Delta}$ holds if $i$ with ${1\leq i\leq n+1}$ exists
such that

  1. 1.

for each ${1\leq j<i}$, we have ${R_{t}^{*}\\!\models\Delta^{j}\vee L^{j}}$,
and

  2. 2.

if ${i\leq n}$ (i.e., $i$ is an index of a clause from $N_{t}$), then
${\Delta^{i}\vee L^{i}>_{t}\Delta}$.

###### Proof.

Assume that ${\Gamma\rightarrow\Delta\mathrel{\hat{\in}}N_{t}}$ holds. If
${\Gamma\rightarrow\Delta}$ satisfies Item 1 of Definition 4, then we clearly
have ${R_{t}^{*}\\!\models\Delta}$. Assume that ${\Gamma\rightarrow\Delta}$
satisfies Item 2 of Definition 4 due to some clause
${\Gamma^{j}\rightarrow\Delta^{j}\vee L^{j}\in N_{t}}$ such that
${\Gamma^{j}\subseteq\Gamma}$ and ${\Delta^{j}\cup\\{\hskip
0.29999ptL^{j}\hskip 0.29999pt\\}\subseteq\Delta}$ hold; the latter clearly
implies ${\Delta\geq_{t}\Delta^{j}\vee L^{j}}$. Let $i$ be an integer
satisfying this lemma’s assumption. If ${i=n+1}$, then we clearly have
${j<i}$; otherwise, ${\Delta^{i}\vee L^{i}>_{t}\Delta}$ implies
${\Delta^{i}\vee L^{i}>_{t}\Delta^{j}\vee L^{j}}$, and so we also have
${j<i}$. But then, by the lemma assumption we have
${R_{t}^{*}\\!\models\Delta^{j}\vee L^{j}}$, which implies
${R_{t}^{*}\\!\models\Delta}$, as required. ∎

######  Lemma 5.

For each clause ${\Gamma\rightarrow\Delta}$ such that
${\Gamma\rightarrow\Delta\mathrel{\hat{\in}}\mathcal{S}_{v}}$ and
${\Gamma\sigma_{\\!{}t}\subseteq\Gamma_{t}}$ hold, we have
${\Gamma\sigma_{\\!{}t}\rightarrow\Delta\sigma_{\\!{}t}\mathrel{\hat{\in}}N_{t}}$.

###### Proof.

Assume that ${\Gamma\rightarrow\Delta\mathrel{\hat{\in}}\mathcal{S}_{v}}$
holds. If ${\Gamma\rightarrow\Delta}$ satisfies Item 1 of Definition 4, then
terms $s$ and $s^{\prime}$ exist such that ${s\approx s\in\Delta}$ or
${\\{s\approx s^{\prime},\;s\not\approx s^{\prime}\\}\subseteq\Delta}$; but
then, ${s\sigma_{\\!{}t}\approx
s^{\prime}\sigma_{\\!{}t}\in\Delta\sigma_{\\!{}t}}$ or
${\\{s\sigma_{\\!{}t}\approx
s^{\prime}\sigma_{\\!{}t},\;s\sigma_{\\!{}t}\not\approx
s^{\prime}\sigma_{\\!{}t}\\}\subseteq\Delta\sigma_{\\!{}t}}$, so
${\Gamma\sigma_{\\!{}t}\rightarrow\Delta\sigma_{\\!{}t}\mathrel{\hat{\in}}N_{t}}$
holds. Furthermore, if ${\Gamma\rightarrow\Delta}$ satisfies Item 2 of
Definition 4, then clause
${\Gamma^{\prime}\rightarrow\Delta^{\prime}\in\mathcal{S}_{v}}$ exists such
that ${\Gamma^{\prime}\subseteq\Gamma}$ and
${\Delta^{\prime}\subseteq\Delta}$; but then, due to
${\Gamma^{\prime}\sigma_{\\!{}t}\subseteq\Gamma\sigma_{\\!{}t}\subseteq\Gamma_{t}}$,
we have that
${\Gamma^{\prime}\sigma_{\\!{}t}\rightarrow\Delta^{\prime}\sigma_{\\!{}t}\in
N_{t}}$ holds, and so
${\Gamma\sigma_{\\!{}t}\rightarrow\Delta\sigma_{\\!{}t}\mathrel{\hat{\in}}N_{t}}$
holds as well. ∎

######  Lemma 6.

For each ${\Gamma\rightarrow\Delta\in N_{t}}$, we have
${R_{t}^{*}\\!\models\Delta}$.

###### Proof.

For the sake of a contraction, choose
${C^{i}=\Gamma^{i}\rightarrow\Delta^{i}\vee L^{i}}$ as the clause in the
sequence of clauses from Section C.1.2 with the smallest $i$ such that
${R_{t}^{*}\\!\not\models\Delta^{i}\vee L^{i}}$; please recall that
${L^{i}>_{t}\Delta^{i}}$ and that ${L^{i}=l^{i}\bowtie r^{i}}$ with
${\bowtie}\in\\{{\approx},{\not\approx}\\}$. Due to our choice of $i$, Item 1
of Lemma 4 holds for $C^{i}$ and $i$. By the definition of $N_{t}$, a clause
${\Gamma\rightarrow\Delta\vee L\in\mathcal{S}_{v}}$ exists such that

$\displaystyle\Gamma\sigma_{\\!{}t}=\Gamma^{i}\subseteq\Gamma_{t},\quad\Delta\sigma_{\\!{}t}=\Delta^{i},\quad
L\sigma_{\\!{}t}=L^{i},\quad\text{and}\quad\Delta\not\succeq_{v}L.$ (78)

We next prove the claim of this lemma by considering the possible forms of
$L^{i}$.

Assume ${L^{i}=l^{i}\approx r^{i}}$ with ${l^{i}=r^{i}}$. But then, we have
${R_{t}^{*}\\!\models L^{i}}$, which contradicts our assumption that
${R_{t}^{*}\\!\not\models\Delta^{i}\vee L^{i}}$.

Assume ${L^{i}=l^{i}\approx r^{i}}$ with ${l^{i}>_{t}r^{i}}$. Then, literal
$L$ is of the form ${l\approx r}$ such that ${l\sigma_{\\!{}t}\approx
r\sigma_{\\!{}t}=l^{i}\approx r^{i}}$. By the definition of $>_{t}$, we have
${l\succ_{v}r}$. We first show that
${(R_{t}^{i-1})^{*}\\!\not\models\Delta^{i}\vee L^{i}}$ holds; towards this
goal, note that, for each equality ${s_{1}\approx s_{2}\in\Delta^{i}\vee
L^{i}}$, properties ${R_{t}^{*}\\!\not\models s_{1}\approx s_{2}}$ and
${R_{t}^{i-1}\subseteq R_{t}}$ imply ${(R_{t}^{i-1})^{*}\\!\not\models
s_{1}\approx s_{2}}$; and for each inequality ${s_{1}\not\approx
s_{2}\in\Delta^{i}}$, Lemma 2 and ${R_{t}^{*}\\!\not\models s_{1}\not\approx
s_{2}}$ imply ${(R_{t}^{i-1})^{*}\\!\not\models s_{1}\not\approx s_{2}}$.
Thus, clause $C^{i}$ satisfies Items R1 and R2; however, since
${R_{t}^{*}\\!\not\models l^{i}\approx r^{i}}$, clause $C^{i}$ is not
generational and thus either Item R3 or Item R4 are not satisfied. We next
consider both of these possibilities.

  * •

Item R3 does not hold—that is, $l^{i}$ is reducible by $R_{t}^{i-1}$. By the
definition of reducibility, a position $p$ and a clause
${C^{j}=\Gamma^{j}\rightarrow\Delta^{j}\vee l^{j}\approx r^{j}}$ generating
the rule ${l^{j}\Rightarrow r^{j}}$ exist such that ${j<i}$ and
${l^{i}|_{p}=l^{j}}$. Due to ${j<i}$, we have ${l^{i}\approx
r^{i}\geq_{t}l^{j}\approx r^{j}}$; together with ${l^{j}\approx
r^{j}>_{t}\Delta^{j}}$, we have ${l^{i}\approx r^{i}>_{t}\Delta^{j}}$. Lemma 3
ensures ${R_{t}^{*}\\!\not\models\Delta^{j}}$, and the definition of $N_{t}$
ensures that a clause ${\Gamma^{\prime}\rightarrow\Delta^{\prime}\vee
l^{\prime}\approx r^{\prime}\in\mathcal{S}_{v}}$ exists such that

$\displaystyle\Gamma^{\prime}\sigma_{\\!{}t}=\Gamma^{j}\subseteq\Gamma_{t},\quad\Delta^{\prime}\sigma_{\\!{}t}=\Delta^{j},\quad
l^{\prime}\sigma_{\\!{}t}=l^{j},\quad
r^{\prime}\sigma_{\\!{}t}=r^{j},\quad\Delta^{\prime}\not\succeq_{v}l^{\prime}\approx
r^{\prime},\quad\text{and}\quad l^{\prime}\succ_{v}r^{\prime}.$ (79)

By the assumption of Theorem 2, the $\mathsf{Eq}$ rule is not applicable to 78
and 79, and so
${\Gamma\wedge\Gamma^{\prime}\rightarrow\Delta\vee\Delta^{\prime}\vee
l[r^{\prime}]_{p}\approx r\mathrel{\hat{\in}}\mathcal{S}_{v}}$. Let
${\Delta^{\prime\prime}=\Delta^{i}\vee\Delta^{j}\vee l^{i}[r^{j}]_{p}\approx
r^{i}}$. Then clearly
${\Gamma\sigma_{\\!{}t}\cup\Gamma^{\prime}\sigma_{\\!{}t}\subseteq\Gamma_{t}}$,
so Lemma 5 ensures that
${\Gamma^{i}\wedge\Gamma^{j}\rightarrow\Delta^{\prime\prime}\mathrel{\hat{\in}}N_{t}}$
holds. Set $R_{t}^{*}$ is a congruence, so ${l^{i}[r^{j}]_{p}\approx
r^{i}\not\in R_{t}^{*}}$ holds, and therefore
${R_{t}^{*}\\!\not\models\Delta^{\prime\prime}}$ holds. Finally, $>_{t}$ is a
simplification order, which ensures ${l^{i}\approx
r^{i}>_{t}l^{i}[r^{j}]_{p}\approx r^{i}}$; together with ${l^{i}\approx
r^{i}>_{t}\Delta^{i}}$ and ${l^{i}\approx r^{i}>_{t}\Delta^{j}}$, we have
${l^{i}\approx r^{i}>_{t}\Delta^{\prime\prime}}$. But then, Lemma 4 implies
${R_{t}^{*}\\!\models\Delta^{\prime\prime}}$, which is a contradiction.

  * •

Item R4 does not hold. Then, some term $s$ exists such that ${l^{i}\approx
s\in\Delta^{i}}$ and ${s\approx r^{i}\in(R_{t}^{i-1})^{*}}$. Due to
${R_{t}^{i-1}\subseteq R_{t}}$, we have ${s\approx r^{i}\in R_{t}^{*}}$, and
so ${R_{t}^{*}\\!\not\models s\not\approx r^{i}}$. Furthermore, ${\Delta\vee
L}$ is of the form ${\Delta^{\prime}\vee l\approx r\vee l^{\prime}\approx
r^{\prime}}$ such that

$\displaystyle l\sigma_{\\!{}t}=l^{i},\quad r\sigma_{\\!{}t}=s,\quad
l^{\prime}\sigma_{\\!{}t}=l^{i},\quad\text{and}\quad
r^{\prime}\sigma_{\\!{}t}=r^{i}.$ (80)

But then, we clearly have ${l^{\prime}=l}$. By the assumption of Theorem 2,
the $\mathsf{Factor}$ rule is not applicable to ${\Gamma\rightarrow\Delta\vee
L}$, and so we have ${\Gamma\rightarrow\Delta^{\prime}\vee r\not\approx
r^{\prime}\vee l^{\prime}\approx
r^{\prime}\mathrel{\hat{\in}}\mathcal{S}_{v}}$. Let
${\Delta^{\prime\prime}=\Delta^{\prime}\sigma_{\\!{}t}\vee s\not\approx
r^{i}\vee l^{i}\approx r^{i}}$. But then,
${\Gamma\sigma_{\\!{}t}\subseteq\Gamma_{t}}$ and Lemma 5 ensure that
${\Gamma^{i}\rightarrow\Delta^{\prime\prime}\mathrel{\hat{\in}}N_{t}}$ holds.
By all the previous observations, we have
${R_{t}^{*}\\!\not\models\Delta^{\prime\prime}}$. Moreover,
${l^{i}>_{t}r^{i}}$ and ${l^{i}>_{t}s}$ imply ${l^{i}\approx
r^{i}>_{t}s\approx r^{i}}$; thus, ${\Delta^{i}\vee l^{i}\approx
r^{i}>_{t}\Delta^{\prime\prime}}$ holds. But then, Lemma 4 implies
${R_{t}^{*}\\!\models\Delta^{\prime\prime}}$, which is a contradiction.

Assume ${L^{i}=l^{i}\not\approx r^{i}}$ with ${l^{i}=r^{i}}$. Then, literal
$L$ is of the form ${l\not\approx r}$ such that ${l\sigma_{\\!{}t}\not\approx
r\sigma_{\\!{}t}=l^{i}\not\approx r^{i}}$. But then, ${l^{i}=r^{i}}$ implies
${l=r}$. By the assumption of Theorem 2, the $\mathsf{Ineq}$ rule is not
applicable to clause ${\Gamma\rightarrow\Delta\vee L}$, and so we have
${\Gamma\rightarrow\Delta\mathrel{\hat{\in}}\mathcal{S}_{v}}$. Since
${\Gamma\sigma_{\\!{}t}\subseteq\Gamma_{t}}$, by Lemma 5 we have
${\Gamma^{i}\rightarrow\Delta^{i}\mathrel{\hat{\in}}N_{t}}$. Clearly,
${\Delta^{i}\vee l^{i}\not\approx r^{i}>_{t}\Delta^{i}}$, and so Lemma 4
implies ${R_{t}^{*}\\!\models\Delta^{i}}$, which is a contradiction.

Assume ${L^{i}=l^{i}\not\approx r^{i}}$ with ${l^{i}>_{t}r^{i}}$. Lemma 2
ensures ${(R_{t}^{i-1})^{*}\\!\not\models l^{i}\not\approx r^{i}}$; hence,
$l^{i}$ is reducible by $R_{t}^{i-1}$ so, by the definition of reducibility, a
position $p$ and a generative clause
${C^{j}=\Gamma^{j}\rightarrow\Delta^{j}\vee l^{j}\approx r^{j}}$ exist such
that ${j<i}$ and ${l^{i}|_{p}=l^{j}}$. Due to ${j<i}$, we have
${l^{i}\not\approx r^{i}>_{t}l^{j}\approx r^{j}>_{t}\Delta^{j}}$. Lemma 3
ensures ${R_{t}^{*}\\!\not\models\Delta^{j}}$, and the definition of $N_{t}$
ensures that a clause ${\Gamma^{\prime}\rightarrow\Delta^{\prime}\vee
l^{\prime}\approx r^{\prime}\in\mathcal{S}_{v}}$ exists satisfying 79, as in
the first case. By the assumption of Theorem 2, the $\mathsf{Eq}$ rule is not
applicable to clauses 78 and 79, and so
${\Gamma\wedge\Gamma^{\prime}\rightarrow\Delta\vee\Delta^{\prime}\vee
l[r^{\prime}]_{p}\not\approx r\mathrel{\hat{\in}}\mathcal{S}_{v}}$ holds. Let
${\Delta^{\prime\prime}=\Delta^{i}\vee\Delta^{j}\vee
l^{i}[r^{j}]_{p}\not\approx r^{i}}$. We clearly have
${\Gamma\sigma_{\\!{}t}\cup\Gamma^{\prime}\sigma_{\\!{}t}\subseteq\Gamma_{t}}$,
so by Lemma 5 we have
${\Gamma^{i}\wedge\Gamma^{j}\rightarrow\Delta^{\prime\prime}\mathrel{\hat{\in}}N_{t}}$.
Since $R_{t}^{*}$ is a congruence, we have ${R_{t}^{*}\\!\not\models
l^{i}[l^{j}]_{p}\not\approx r^{i}}$, and therefore
${R_{t}^{*}\\!\not\models\Delta^{\prime\prime}}$ holds. Finally, $>_{t}$ is a
simplification order, so ${l^{i}\not\approx r^{i}>_{t}l^{i}[l^{j}]_{p}}$;
together with ${l^{i}\approx r^{i}>_{t}\Delta^{i}}$ and ${l^{i}\approx
r^{i}>_{t}\Delta^{j}}$, we have ${l^{i}\approx
r^{i}>_{t}\Delta^{\prime\prime}}$. But then, Lemma 4 implies
${R_{t}^{*}\\!\models\Delta^{\prime\prime}}$, which is a contradiction. ∎

######  Lemma 7.

For each clause ${\Gamma\rightarrow\Delta}$ with
${\Gamma\rightarrow\Delta\mathrel{\hat{\in}}N_{t}}$, we have
${R_{t}^{*}\\!\models\Delta}$.

###### Proof.

Apply Lemma 4 for ${i=n+1}$ and Lemma 6. ∎

######  Lemma 8.

For each generative clause ${\Gamma^{i}\rightarrow\Delta^{i}\vee l^{i}\approx
r^{i}}$, disjunction $\Delta^{i}$ does not contain a literal of the form
${s\not\approx s}$.

###### Proof.

For the sake of a contradiction, let us assume that clause
${C^{i}=\Gamma^{i}\rightarrow\Delta^{i}\vee l^{i}\approx r^{i}\in N_{t}}$ is
generative and that ${s\not\approx s\in\Delta^{i}}$ holds for some term $s$.
By the definition of $N_{t}$, a clause
${\Gamma^{\prime}\rightarrow\Delta^{\prime}\vee s^{\prime}\not\approx
s^{\prime}\vee l^{\prime}\approx r^{\prime}\in\mathcal{S}_{v}}$ exists such
that

$\displaystyle\Gamma^{\prime}\sigma_{\\!{}t}=\Gamma^{i}\subseteq\Gamma_{t},\quad\Delta^{\prime}\sigma_{\\!{}t}\cup\\{\hskip
0.29999pts^{\prime}\sigma_{\\!{}t}\not\approx s^{\prime}\sigma_{\\!{}t}\hskip
0.29999pt\\}=\Delta^{i},\quad s^{\prime}\sigma_{\\!{}t}=s,\quad
l^{\prime}\sigma_{\\!{}t}=l^{i},\quad\text{and}\quad
r^{\prime}\sigma_{\\!{}t}=r^{i}.$ (81)

By assumption of Theorem 2, the $\mathsf{Ineq}$ rule is not applicable to this
clause, and so we have ${\Gamma^{\prime}\rightarrow\Delta^{\prime}\vee
l^{\prime}\approx r^{\prime}\mathrel{\hat{\in}}\mathcal{S}_{v}}$. Thus, we
have ${\Gamma^{i}\rightarrow\Delta^{\prime}\sigma_{\\!{}t}\vee l^{i}\approx
r^{i}\mathrel{\hat{\in}}N_{t}}$, and so ${\Gamma\rightarrow\Delta\in N_{t}}$
holds for some ${\Gamma\subseteq\Gamma^{i}}$ and some
${\Delta\subsetneq\Delta^{i}\cup\\{\hskip 0.29999ptl^{i}\approx r^{i}\hskip
0.29999pt\\}}$. Now Lemma 3 implies ${R_{t}^{*}\\!\not\models\Delta^{i}}$;
moreover, by Item R1, we have ${(R_{t}^{i-1})^{*}\\!\not\models\Delta^{i}\vee
l^{i}\approx r^{i}}$. However, by Lemma 6 we have
${R_{t}^{*}\\!\models\Gamma\rightarrow\Delta}$. Now let $j$ be the index of
clause ${\Gamma\rightarrow\Delta}$ in the sequence of clauses from Section
C.1.2; due to ${(R_{t}^{j})^{*}\subseteq(R_{t}^{i-1})^{*}}$ and Lemma 2, we
have ${(R_{t}^{j})^{*}\\!\models\Gamma\rightarrow\Delta}$. Since ${j<i}$, by
the same argument we have
${(R_{t}^{i-1})^{*}\\!\models\Gamma\rightarrow\Delta}$. But then,
${\Delta\subseteq\Delta^{i}\vee l^{i}\approx r^{i}}$ implies
${(R_{t}^{i-1})^{*}\\!\models\Delta^{i}\vee l^{i}\approx r^{i}}$, which is a
contradiction. ∎

######  Lemma 9.

${R_{t}^{*}\\!\not\models\Gamma_{t}\rightarrow\Delta_{t}}$.

###### Proof.

For ${R_{t}^{*}\\!\models\Gamma_{t}}$, note that Item L2 ensures
${\Gamma_{t}\rightarrow A\mathrel{\hat{\in}}N_{t}}$, and so Lemma 7 ensures
${R_{t}^{*}\\!\models A}$ for each atom ${A\in\Gamma_{t}}$.

For ${R_{t}^{*}\\!\not\models\Delta_{t}}$, assume for the sake of a
contradiction that an atom ${A\in\Delta_{t}}$ exists such that
${R_{t}^{*}\\!\models A}$. Then, a generative clause
${C^{i}=\Gamma^{i}\rightarrow\Delta^{i}\vee l^{i}\approx r^{i}\in N_{t}}$ and
a position $p$ exist such that ${A|_{p}=l^{i}}$; let ${\Delta=\Delta^{i}\vee
l^{i}\approx r^{i}}$. Since $>_{t}$ is a simplification order and
${l^{i}>_{t}r^{i}}$, we have ${A\geq_{t}l^{i}\approx r^{i}}$; but then, since
${l^{i}\approx r^{i}>_{t}\Delta^{i}}$, we have ${A\geq_{t}\Delta}$. We next
consider an arbitrary literal ${l\bowtie r\in\Delta}$ with
${{\bowtie}\in\\{\hskip 0.29999pt{\approx},{\not\approx}\hskip 0.29999pt\\}}$
and ${l\geq_{t}r}$; by the observations made thus far, ${A\geq_{t}l\bowtie r}$
holds. By Item O2, one of the following holds.

  1. 1.

${l\in\\{\hskip 0.29999ptt,t^{\prime}\hskip 0.29999pt\\}}$. Moreover, since
${l\bowtie r}$ is obtained by grounding a context literal, both $l$ and $r$
can be of the form $f(t)$ or $t^{\prime}$. Together with ${l\geq_{t}r}$, we
have ${l=r=t^{\prime}}$. Now if ${l\bowtie r}$ is ${t^{\prime}\approx
t^{\prime}}$, then clause $C^{i}$ is not generative due to Item R1. Hence, the
only remaining possibility is for ${l\bowtie r}$ to be of the form
${t^{\prime}\not\approx t^{\prime}}$; but then, clause $C^{i}$ is not
generative by Lemma 8. Consequently, in either case we get a contradiction.

  2. 2.

${l\approx r\in\Delta_{t}}$ where ${r=\wp}$.

Thus, the second point above holds for arbitrary ${l\bowtie r\in\Delta}$, and
therefore we have ${\Delta\subseteq\Delta_{t}}$. But then,
${\Gamma^{i}\subseteq\Gamma_{t}}$ implies that
${\Gamma_{t}\rightarrow\Delta_{t}\mathrel{\hat{\in}}N_{t}}$ holds, which
contradicts Item L1. ∎

###  C.2 Interpreting the Ontology $\mathcal{O}$

We now combine the rewrite systems $R_{t}$ constructed in Section C.1 into a
single rewrite system $R$, and we then show that $R^{*}$ satisfies
${R^{*}\\!\models\mathcal{O}}$ and
${R^{*}\\!\not\models\Gamma_{Q}\rightarrow\Delta_{Q}}$.

####  C.2.1 Unfolding the Context Structure

We construct $R$ by a partial induction over the terms in $\mathcal{T}$. We
define several partial functions: function $X$ maps a term $t$ to a context
${X_{t}\in\mathcal{V}}$; functions $\Gamma$ and $\Delta$ assign to a term $t$
a conjunction $\Gamma_{t}$ and a disjunction $\Delta_{t}$, respectively, of
atoms; and function $R$ maps each term into a model fragment $R_{t}$ for $t$,
$X_{t}$, $\Gamma_{t}$, and $\Delta_{t}$.

  1. M1.

For the base case, we consider the constant $c$.

$\displaystyle X_{c}$ $\displaystyle=q$ (82) $\displaystyle\Gamma_{c}$
$\displaystyle=\Gamma_{Q}\sigma_{\\!{}c}$ (83) $\displaystyle\Delta_{c}$
$\displaystyle=\Delta_{Q}\sigma_{\\!{}c}$ (84) $\displaystyle R_{c}$
$\displaystyle=\text{the model fragment for }c,q,\Gamma_{c},\text{ and
}\Delta_{c}$ (85)

  2. M2.

For the inductive step, assume that $X_{t^{\prime}}$ has already been defined,
and consider an arbitrary function symbol ${f\in\mathcal{F}}$ such that
$f(t^{\prime})$ is irreducible by $R_{t^{\prime}}$. Let ${u=X_{t^{\prime}}}$
and ${t=f(t^{\prime})}$. We have two possibilities.

    1. M2.a.

Term $t$ occurs in $R_{t^{\prime}}$. Then, term ${t=f(t^{\prime})}$ was
generated in $R_{t^{\prime}}$ by some ground clause
${C=\Gamma\rightarrow\Delta\vee L\in N_{t^{\prime}}}$ such that
${L>_{t}\Delta}$ and $f(t^{\prime})$ occurs in $L$. By the definition of
$N_{t}$, then a clause
${C^{\prime}=\Gamma^{\prime}\rightarrow\Delta^{\prime}\vee
L^{\prime}\in\mathcal{S}_{u}}$ exists such that
${C=C^{\prime}\sigma_{\\!{}t^{\prime}}}$ and $L^{\prime}$ contains $f(x)$;
moreover, ${L>_{t^{\prime}}\Delta}$ implies
${\Delta^{\prime}\not\succeq_{u}L^{\prime}}$. The $\mathsf{Succ}$ and
$\mathsf{Core}$ rules are not applicable to $\mathcal{D}$, so we can choose a
context ${v\in\mathcal{V}}$ such that ${\langle u,v,f\rangle\in\mathcal{E}}$
and ${A\rightarrow A\mathrel{\hat{\in}}\mathcal{S}_{v}}$ for each ${A\in
K_{2}}$, where $K_{2}$ is as in the $\mathsf{Succ}$ rule. We define the
following:

$\displaystyle X_{t}$ $\displaystyle=v$ (86) $\displaystyle\Gamma_{t}$
$\displaystyle=R_{t^{\prime}}^{*}\cap\mathsf{Su}_{t}$ (87)
$\displaystyle\Delta_{t}$ $\displaystyle=\mathsf{Pr}_{t}\setminus
R_{t^{\prime}}^{*}$ (88) $\displaystyle R_{t}$ $\displaystyle=\text{the model
fragment for }t,v,\Gamma_{t},\text{ and }\Delta_{t}$ (89)

    2. M2.b.

Term $t$ does not occur in $R_{t^{\prime}}$. Then, let ${R_{t}=\\{\hskip
0.29999ptt\Rightarrow c\hskip 0.29999pt\\}}$, and we do not define any other
functions for $t$.

Finally, let $R$ be the rewrite system defined by ${R=\bigcup_{t}R_{t}}$.

######  Lemma 10.

The model fragments $R_{c}$ and $R_{t}$ constructed in lines 85 and 89 satisfy
Items L1, L3 and L2 in Section C.1.

###### Proof.

The proof is by induction on the structure of terms ${t\in\mathsf{dom}(X)}$.
For ${t=c}$, Items L1, L3 and L2 hold directly from conditions C1 through C3
of Theorem 2. We next assume that the lemma holds for some term
${t^{\prime}\in\mathsf{dom}(X)}$, and we consider an arbitrary term $t$ of the
form ${t=f(t^{\prime})}$; let ${u=X_{t^{\prime}}}$ and ${v=X_{t}}$. Item L2
holds because ${\Delta_{t}=\mathsf{Pr}_{t}\setminus R_{t^{\prime}}^{*}}$ due
to 88, and hence ${\Delta_{t}\subseteq\mathsf{Pr}_{t}}$. Before proceeding,
note that terms $t$ and $t^{\prime}$ are irreducible by $R_{t^{\prime}}$ due
to Item M2; but then, since ${\Gamma_{t}\subseteq R_{t^{\prime}}^{*}}$ holds
by 87, each each atom ${A_{i}\in R_{t^{\prime}}}$ is generated by clause
satisfying 90 (where subscript $i$ does not necessarily indicate the position
of the clause in sequence of clauses from Section C.1.2). By the definition of
$N_{t^{\prime}}$, then there exists a clause satisfying 91.

$\displaystyle\Gamma_{i}\rightarrow\Delta_{i}\vee A_{i}$ $\displaystyle\in
N_{t^{\prime}}$ $\displaystyle\text{with}\quad A_{i}>_{t}\Delta_{i}$ (90)
$\displaystyle\Gamma_{i}^{\prime}\rightarrow\Delta_{i}^{\prime}\vee
A_{i}^{\prime}$ $\displaystyle\in\mathcal{S}_{u}$
$\displaystyle\Gamma_{i}=\Gamma_{i}^{\prime}\sigma_{\\!{}t^{\prime}},\quad\Delta_{i}=\Delta_{i}^{\prime}\sigma_{\\!{}t^{\prime}},\quad
A_{i}=A_{i}^{\prime}\sigma_{\\!{}t^{\prime}},\quad\text{and}\quad\Delta_{i}^{\prime}\not\succeq_{u}A_{i}^{\prime}$
(91)

For Item L3, consider an arbitrary atom ${A_{i}\in\Gamma_{t}}$, let 90 be the
clause that generates $A_{i}$ in $R_{t^{\prime}}$, and let 91 be the
corresponding nonground clause. Since ${A_{i}\in\mathsf{Su}_{t}}$, atom
$A_{i}^{\prime}$ is of the form $A_{i}^{\prime\prime}\sigma$, where $\sigma$
is the substitution from the $\mathsf{Succ}$ rule; but then,
${A_{i}^{\prime\prime}\in K_{2}}$, where $K_{2}$ is as specified in the
$\mathsf{Succ}$ rule. In M2M2.a we chose $v$ so that the $\mathsf{Succ}$ rule
is satisfied, and therefore ${A_{i}^{\prime\prime}\rightarrow
A_{i}^{\prime\prime}\mathrel{\hat{\in}}\mathcal{S}_{v}}$; but then, since
${A_{i}^{\prime\prime}\sigma_{\\!{}t}=A_{i}}$, we have ${A_{i}\rightarrow
A_{i}\mathrel{\hat{\in}}N_{t}}$, as required for Item L3.

To prove that Item L1 holds as well, assume for the sake of a contradiction
that ${\Gamma_{t}\rightarrow\Delta_{t}\mathrel{\hat{\in}}N_{t}}$ holds. We
have ${\Delta_{t}\subseteq\mathsf{Pr}_{t}}$ due to 88. Therefore, due to Item
2 of Definition 4, set $N_{t}$ contains a clause

$\displaystyle\bigwedge_{i=1}^{m}A_{i}\rightarrow\bigvee_{i=m+1}^{m+n}A_{i}\quad\text{with}\quad\\{\,A_{i}\mid
1\leq i\leq m\,\\}\subseteq\Gamma_{t}\quad\text{and}\quad\\{\,A_{i}\mid
m+1\leq i\leq m+n\,\\}\subseteq\Delta_{t}\subseteq\mathsf{Pr}_{t}.$ (92)

By the definition of $N_{t}$, set $\mathcal{S}_{v}$ contains a clause

$\displaystyle\bigwedge_{i=1}^{m}A_{i}^{\prime}\rightarrow\bigvee_{i=m+1}^{m+n}A_{i}^{\prime}\quad\text{where}\quad
A_{i}=A_{i}^{\prime}\sigma_{\\!{}t}\text{ for }1\leq i\leq
m+n\quad\text{and}\quad A_{i}^{\prime}\in\mathsf{Pr}(\mathcal{O})\text{ for
}m+1\leq i\leq m+n.$ (93)

Now each $A_{i}$ with ${1\leq i\leq m}$ is generated by a ground clause 90,
and the latter is obtained from the corresponding nonground clause 91. The
$\mathsf{Pred}$ rule is not applicable to 93 and 91 so 94 holds; together with
Lemma 5, this ensures 95.

$\displaystyle\bigwedge_{i=1}^{m}\Gamma_{i}^{\prime}\rightarrow\bigvee_{i=1}^{m}\Delta_{i}^{\prime}\vee\bigvee_{i=m+1}^{m+n}A_{i}^{\prime}\sigma$
$\displaystyle\mathrel{\hat{\in}}\mathcal{S}_{u}\quad\text{for
}\sigma=\\{{x\mapsto f(x),\;y\mapsto x}\\}$ (94)
$\displaystyle\bigwedge_{i=1}^{m}\Gamma_{i}\rightarrow\bigvee_{i=1}^{m}\Delta_{i}\vee\bigvee_{i=m+1}^{m+n}A_{i}$
$\displaystyle\mathrel{\hat{\in}}N_{t^{\prime}}$ (95)

By Lemma 3, we have ${R_{t^{\prime}}^{*}\\!\not\models\Delta_{i}}$; and 88
ensures that ${R_{t^{\prime}}^{*}\\!\not\models\Delta_{t}}$, and so
${R_{t^{\prime}}^{*}\\!\not\models A_{i}}$ for each ${m+1\leq i\leq m+n}$;
however, this contradicts 95 and Lemma 7. ∎

####  C.2.2 Termination, Confluence, and Compatibility

######  Lemma 11.

The rewrite system $R$ is Church-Rosser.

###### Proof.

We show that $R$ is terminating and left-reduced, and thus Church-Rosser. In
the proof of the former, we use a total simplification order $\rhd$ on all
ground $\mathcal{F}$\- and $\mathcal{P}$-terms defined as follows. We extend
the precedence $\gtrdot$ from Definition 3 to all $\mathcal{F}$\- and
$\mathcal{P}$-symbols in an arbitrary way, but ensuring that constant $\wp$ is
smallest in the order; then, let $\rhd$ be a _lexicographic path order_ (?)
over such $\gtrdot$. It is well known that such $\rhd$ is a simplification
order, and that it satisfies the following properties for each
$\mathcal{F}$-term $t$ with predecessor $t^{\prime}$ (if one exists), all
function symbols ${f,g\in\mathcal{F}}$, and each $\mathcal{P}$-term $A$:

  * •

${f(t)\rhd t\rhd t^{\prime}}$,

  * •

${f\gtrdot g}$ implies ${f(t)\rhd g(t)}$, and

  * •

${A\rhd\wp}$.

Thus, Items 1 and 2 of Definition 3 and the manner in which context orders are
grounded in Section C.1.1 clearly ensure that, for each $\mathcal{F}$-term
${t\in\mathsf{dom}(X)}$ and for all terms $s_{1}$ and $s_{2}$ from the
$\mathcal{F}$-neighbourhood of $t$ with ${s_{1}>_{t}s_{2}}$, we have
${s_{1}\rhd s_{2}}$.

We next show that $R$ is terminating by arguing that each rule in $R$ is
embedded in $\rhd$. To this end, consider an arbitrary rule ${l\Rightarrow
r\in R}$. Clearly, a term ${t\in\mathsf{dom}(R)}$ exists such that
${l\Rightarrow r\in R_{t}}$. This rule is obtained from a head ${l\approx r}$
of a clause in $N_{t}$, and Item R2 of the definition of $R_{t}$ ensures that
${l>_{t}r}$. Moreover, ${l\approx r}$ is obtained by grounding a context
literal with $\sigma_{\\!{}t}$, so we have the following possible forms of
${l\approx r}$.

  * •

Terms $l$ and $r$ are both from the $\mathcal{F}$-neighbourhood of $t$. Then,
${l>_{t}r}$ implies ${l\rhd r}$.

  * •

We have ${l\approx r=A\approx\wp}$ for $A$ a $\mathcal{P}$-term. Then,
${A\rhd\wp}$ since $\wp$ is smallest in $\gtrdot$.

We next show that $R$ is left-reduced. For the sake of a contradiction, assume
that a rule ${l\Rightarrow r\in R}$ exists such that $l$ is reducible by
${R^{\prime}=R\setminus\\{\hskip 0.29999ptl\Rightarrow r\hskip 0.29999pt\\}}$.
Let $p$ be the ‘deepest’ position at which some rule in $R^{\prime}$ reduces
$l$ (i.e., no rule in $R^{\prime}$ reduces $l$ at position below $p$), and let
${l^{\prime}\Rightarrow r^{\prime}\in R^{\prime}}$ be the rule that reduces
$l$ at position $p$; thus, ${l^{\prime}=l|_{p}}$. By the definition of $R$, we
have ${l^{\prime}\Rightarrow r^{\prime}\in R_{t}}$ where $t$ can be as
follows.

  * •

Term $t$ is handled in M2M2.a. Then ${l^{\prime}\Rightarrow r^{\prime}}$ is
generated by an equality ${l^{\prime}\approx r^{\prime}}$ in the head of a
generative clause, and so $l^{\prime}$ is of the form $f(t)$. Thus, $f(t)$ is
reducible by $R_{t}$, which contradicts Item M2 from the construction of $R$.

  * •

Term $t$ is handled in M2M2.b. Then ${l^{\prime}=t}$; moreover, $R^{\prime}$
does not contain $t$ by the construction of $R$, which contradicts the
assumption that ${l^{\prime}\Rightarrow r^{\prime}\in R^{\prime}}$. ∎

######  Lemma 12.

For each term $t$, each ${f\in\mathcal{F}}$, and each atom
${A\in\mathsf{Su}_{t}\cup\mathsf{Pr}_{f(t)}}$ such that ${A\in R^{*}}$ and all
$\mathcal{F}$-terms in $A$ are irreducible by $R$, we have ${A\in R_{t}^{*}}$.

###### Proof.

Let $t$ be a term, let ${f\in\mathcal{F}}$ be a function symbol, and let
${A\in\mathsf{Su}_{t}\cup\mathsf{Pr}_{f(t)}}$ be an atom such that all
$\mathcal{F}$-terms in $A$ are irreducible by $R$; the latter ensures
${A\Rightarrow\wp\in R}$. We next consider the possible forms of $A$.

Assume ${A\in\mathsf{Su}_{t}}$. By the definition of $\mathsf{Su}_{t}$ in 76
and the fact that $\mathsf{Su}(\mathcal{O})$ contains only atoms of the form
$B(x)$, $S(x,y)$, and $S(y,x)$, atom $A$ can be of the form $B(t)$,
$S(t,t^{\prime})$, or $S(t^{\prime},t)$, for $t^{\prime}$ the predecessor of
$t$ (if one exists). By the form of the generative clauses, we clearly have
${A\in R_{t}^{*}}$ or ${A\in R_{t^{\prime}}^{*}}$. Now assume ${A\in
R_{t^{\prime}}^{*}}$. Due to ${A\in\mathsf{Su}_{t}}$ and the definition of
$\Gamma_{t}$ in 87, we have ${A\in\Gamma_{t}}$. Lemma 9 ensures that
${R_{t}^{*}\\!\not\models\Gamma_{t}\rightarrow\Delta_{t}}$. But then, we have
${A\in R_{t}^{*}}$, as required.

Assume ${A\in\mathsf{Pr}_{f(t)}}$. By the definition of $\mathsf{Pr}_{f(t)}$
in 77 and the fact that $\mathsf{Pr}(\mathcal{O})$ contains only atoms of the
form $B(y)$, $S(y,x)$, and $S(x,y)$, atom $A$ can be of the form $B(t)$,
$S(t,f(t))$, or $S(f(t),t)$. By the form of the generative clauses, we clearly
have ${A\in R_{t}^{*}}$ or ${A\in R_{f(t)}^{*}}$. Assume for the sake of a
contradiction that ${A\not\in R_{t}^{*}}$, but ${A\in R_{f(t)}^{*}}$. Due to
${A\in\mathsf{Pr}_{f(t)}}$ and the definition of $\Delta_{f(t)}$ in 88, we
have ${A\in\Delta_{f(t)}}$; due to Lemma 9, we have
${R_{f(t)}^{*}\\!\not\models\Gamma_{f(t)}\rightarrow\Delta_{f(t)}}$;
therefore, we have ${A\not\in R_{f(t)}^{*}}$, which is a contradiction. ∎

######  Lemma 13.

Let $s_{1}$ and $s_{2}$ be DL-terms, and let $\tau$ be a substitution
irreducible by $R$ such that $s_{1}\tau$ and $s_{2}\tau$ are ground and each
$\tau(z_{i})$ (if defined) is in the $\mathcal{F}$-neighbourhood of $\tau(x)$.
Then, for ${{\bowtie}\in\\{\hskip 0.29999pt{\approx},\;{\not\approx}\hskip
0.29999pt\\}}$, if ${R_{\tau(x)}^{*}\\!\models s_{1}\tau\bowtie s_{2}\tau}$,
then ${R^{*}\\!\models s_{1}\tau\bowtie s_{2}\tau}$.

###### Proof.

Let $s_{1}$ and $s_{2}$ and $\tau$ be as stated above, let ${t=\tau(x)}$, and
let $t^{\prime}$ be the predecessor of $t$ (if one exists). Since $t$ is
irreducible by $R$, rewrite system $R_{t}$ has been defined in Section C.2.1.
We next consider the possible forms of $\bowtie$.

  * •

Assume ${{\bowtie}={\approx}}$. But then, ${R_{t}\subseteq R}$ and
${R_{t}^{*}\\!\models s_{1}\tau\approx s_{2}\tau}$ imply ${R^{*}\\!\models
s_{1}\tau\approx s_{2}\tau}$.

  * •

Assume ${{\bowtie}={\not\approx}}$. Let $s_{1}^{\prime}$ and $s_{2}^{\prime}$
be the normal forms of $s_{1}\tau$ and $s_{2}\tau$, respectively, w.r.t.
$R_{t}$. Due to the shape of DL-literals, $s_{1}$ and $s_{2}$ can be of the
form $f(x)$ or $z_{i}$; therefore, $s_{1}\tau$ and $s_{2}\tau$ are of the form
$f(t)$ or $t^{\prime}$. Term $t$ is irreducible by $R$, and thus $t^{\prime}$
is irreducible by $R$ as well. Furthermore, due to the shape of context terms,
the only rewrite system where $f(t)$ could occur on the left-hand side of a
rewrite rule is $R_{t}$. Consequently, $f(t)$ is irreducible by $R$ as well.
But then, $s_{1}^{\prime}$ and $s_{2}^{\prime}$ are the normal forms of
$s_{1}\tau$ and $s_{2}\tau$, respectively, w.r.t. $R$; thus, ${R^{*}\\!\models
s_{1}^{\prime}\not\approx s_{2}^{\prime}}$, and thus ${R^{*}\\!\models
s_{1}\tau\not\approx s_{2}\tau}$ holds, as required. ∎

####  C.2.3 The Completeness Claim

######  Lemma 14.

For each DL-clause ${\Gamma\rightarrow\Delta\in\mathcal{O}}$, we have
${R^{*}\\!\models\Gamma\rightarrow\Delta}$.

###### Proof.

Consider an arbitrary DL-clause ${\Gamma\rightarrow\Delta\in\mathcal{O}}$ of
the following form:

$\displaystyle\textstyle\bigwedge_{i=1}^{n}A_{i}\rightarrow\Delta$ (96)

Let $\tau^{\prime}$ be an arbitrary substitution such that
${\Gamma\tau^{\prime}\rightarrow\Delta\tau^{\prime}}$ is ground, and let
$\tau$ be the substitution obtained from $\tau^{\prime}$ by replacing each
ground term with its normal form w.r.t. $R$. Since $R^{*}$ is a congruence, we
have ${R^{*}\\!\models\Gamma\tau^{\prime}\rightarrow\Delta\tau^{\prime}}$ if
and only if ${R^{*}\\!\models\Gamma\tau\rightarrow\Delta\tau}$. We next assume
that ${R^{*}\\!\models\Gamma\tau}$, and we show that
${R^{*}\\!\models\Delta\tau}$ holds as well.

Consider an arbitrary atom ${A_{i}\in\Gamma}$. By the definition of DL-
clauses, $A_{i}$ is of the form $B(x)$, $S(x,z_{j})$, or $S(z_{j},x)$.
Substitution $\tau$ is irreducible by $R$, and so all $\mathcal{F}$-terms in
$A_{i}\tau$ are irreducible by $R$; but then, ${A_{i}\tau\in R^{*}}$ clearly
implies ${A_{i}\tau\Rightarrow\wp\in R}$. Each such rule is obtained from a
generative clause so $A_{i}\tau$ is of the form $B(t)$, $S(t,f(t))$,
$S(f(t),t)$, $S(t,t^{\prime})$, or $S(t^{\prime},t)$, where ${t=\tau(x)}$ and
$t^{\prime}$ is the predecessor of $t$ (if it exists). We next prove that
${A_{i}\tau\in\mathsf{Su}_{t}\cup\mathsf{Pr}_{f(t)}}$ holds by considering the
possible forms of $A_{i}$.

  * •

${A_{i}=B(x)}$, so ${A_{i}\tau=B(t)}$. Then, we have
${B(x)\in\mathsf{Su}(\mathcal{O})}$, which implies that
${B(t)\in\mathsf{Su}_{t}}$ holds.

  * •

${A_{i}=S(x,z_{j})}$, so ${A_{i}\tau}$ is of the form $S(t,t^{\prime})$ or
$S(t,f(t))$. Then, we have ${S(x,y)\in\mathsf{Su}(\mathcal{O})}$, which
implies that ${S(t,t^{\prime})\in\mathsf{Su}_{t}}$ holds; moreover, we have
${S(y,x)\in\mathsf{Pr}(\mathcal{O})}$, which implies that
${S(t,f(t))\in\mathsf{Pr}_{f(t)}}$ holds.

  * •

${A_{i}=S(z_{j},x)}$, so ${A_{i}\tau}$ is of the form $S(t^{\prime},t)$ or
$S(f(t),t)$. Then, we have ${S(y,x)\in\mathsf{Su}(\mathcal{O})}$, which
implies that ${S(t^{\prime},t)\in\mathsf{Su}_{t}}$ holds; moreover, we have
${S(x,y)\in\mathsf{Pr}(\mathcal{O})}$, which implies that
${S(f(t),t)\in\mathsf{Pr}_{f(t)}}$ holds.

Lemma 12 then implies ${A_{i}\tau\in R_{t}}$, and so $N_{t}$ contains a
generative clause of the form 97. Now let ${v=X_{t}}$; by the definition of
$N_{t}$, set $\mathcal{S}_{v}$ contains a clause of the form 98.

$\displaystyle\Gamma_{i}\rightarrow\Delta_{i}\vee A_{i}$ $\displaystyle\text{
with }A_{i}>_{t}\Delta_{i}\text{ and }\Gamma_{i}\subseteq\Gamma_{t}$ (97)
$\displaystyle\Gamma_{i}^{\prime}\rightarrow\Delta_{i}^{\prime}\vee
A_{i}^{\prime}$ $\displaystyle\text{ with
}\Delta_{i}^{\prime}\not\nsucceq{v}A_{i}^{\prime}\text{ and
}\Gamma_{i}^{\prime}\sigma_{\\!{}t}=\Gamma_{i},\;\Delta_{i}^{\prime}\sigma_{\\!{}t}=\Delta_{i},\text{
and }A_{i}^{\prime}\sigma_{\\!{}t}=A_{i}$ (98)

The $\mathsf{Hyper}$ rule is not applicable to 96 and 98, and therefore 99
holds, where $\sigma$ is the substitution obtained from $\tau$ by replacing
each occurrence of $t$ (possibly nested in another term) with $x$. Finally,
Lemma 5 ensures that 100 holds as well.

$\displaystyle\bigwedge_{i=1}^{n}\Gamma_{i}^{\prime}\rightarrow\Delta\sigma\vee\bigvee_{i=1}^{n}\Delta_{i}^{\prime}$
$\displaystyle\mathrel{\hat{\in}}\mathcal{S}_{v}$ (99)
$\displaystyle\bigwedge_{i=1}^{n}\Gamma_{i}\rightarrow\Delta\tau\vee\bigvee_{i=1}^{n}\Delta_{i}$
$\displaystyle\mathrel{\hat{\in}}N_{t}$ (100)

Now 100 and Lemma 7 imply
${R_{t}^{*}\\!\models\Delta\tau\vee\bigvee_{i=1}^{n}\Delta_{i}}$, but Lemma 3
implies ${R_{t}^{*}\\!\not\models\Delta_{i}}$; therefore, we have
${R_{t}^{*}\\!\models\Delta\tau}$. Finally, Lemma 13 ensures
${R^{*}\\!\models\Delta\tau}$, as required. ∎

######  Lemma 15.

${R^{*}\\!\not\models\Gamma_{Q}\rightarrow\Delta_{Q}}$.

###### Proof.

The claim clearly follows from
${R^{*}\\!\not\models\Gamma_{c}\rightarrow\Delta_{c}}$. Note that Lemma 9
ensures ${R_{c}^{*}\\!\not\models\Gamma_{c}\rightarrow\Delta_{c}}$; thus,
${R_{c}^{*}\\!\models\Gamma_{c}}$ and ${R_{c}^{*}\\!\not\models\Delta_{c}}$.
The former observation and Lemma 13 ensure that ${R^{*}\\!\models\Gamma_{c}}$
holds. Moreover, for each atom ${B(x)\in\Delta_{Q}}$, Definition 2 ensures
${B(y)\in\mathsf{Pr}(\mathcal{O})}$; thus, for each ${f\in\mathcal{F}}$, we
have ${B(c)\in\mathsf{Pr}_{f(c)}}$, and so the contrapositive of Lemma 12
ensures ${R^{*}\\!\not\models B(c)}$. Thus, ${R^{*}\\!\not\models\Delta_{c}}$
holds, as required. ∎

##  Appendix D Proof of Proposition 2

See 2

###### Proof.

The number $\wp$ of context clauses that can be generated using the symbols in
$\mathcal{O}$ is at most exponential in the size of $\mathcal{O}$, and the
number $m$ of clauses participating in each inference is linear in the size of
$\mathcal{O}$. Hence, with $k$ contexts, the number of inferences is bounded
by ${(k\cdot\wp)^{m}}$; if $k$ is at most exponential in the size of
$\mathcal{O}$, the number of inferences is exponential as well. Thus, if at
most exponentially many contexts are introduced, our algorithm runs in
exponential time. ∎

##  Appendix E Proof of Proposition 3

See 3

###### Proof.

Consider an $\mathcal{ELH}$ ontology that is transformed into a set
$\mathcal{O}$ of DL-clauses as specified in Section 2, and consider a query of
the form ${B_{1}(x)\rightarrow B_{2}(x)}$. Due to the form of the query, the
core of $q$ is initialised to $B_{1}(x)$.

We first consider applying algorithm A1–A4 to $\mathcal{O}$ with the cautious
strategy and the eager application of the $\mathsf{Hyper}$ rule. By induction
on the application of the rules from Table 2, we next show that each context
clause derived by the rules is of the form 101–105 and that the core of each
context is of the form $B(x)$.

$\displaystyle\top$ $\displaystyle\rightarrow B(x)$ (101) $\displaystyle\top$
$\displaystyle\rightarrow S(x,f(x))$ (102) $\displaystyle\top$
$\displaystyle\rightarrow B(f(x))$ (103) $\displaystyle S(y,x)$
$\displaystyle\rightarrow B(y)$ (104) $\displaystyle S_{1}(y,x)$
$\displaystyle\rightarrow S_{2}(y,x)$ (105)

In particular, in step A3 we can perform the following inferences, with the
specified correspondence to the completion rules CR1–CR4 and CR10 by ? (?).

  * •

The core of each context is of the form $B(x)$, so the $\mathsf{Core}$ rule
introduces a clause of the form form (101). This corresponds to way in which ?