Consequence-based Reasoning for Description Logics with Disjunction, Inverse Roles, Number Restrictions, and Nominals

1 Introduction

Description logics (DLs) [Baader et al., 2003] are a family of knowledge representation formalisms which are widely used in applications. Although the basic DL reasoning problems, such as concept satisfiability and subsumption, are of high worst-case complexity for expressive DLs, different calculi have been developed and implemented in practical systems. Tableau and hyper-tableau calculi [Baader and Sattler, 2001; Motik et al., 2009] are a prominent reasoning technique underpinning many DL reasoners [Sirin et al., 2007; Tsarkov and Horrocks, 2006; Haarslev et al., 2012; Glimm et al., 2014; Steigmiller et al., 2014]. To check whether a concept subsumption relationship holds, (hyper-)tableau calculi attempt to construct a finite representation of an ontology model disproving the given subsumption. The constructed models can, however, be large-a common source of performance issues; this problem is exacerbated in classification

tasks due to the large number of subsumptions to be tested.

Another major category of DL reasoning calculi comprises methods based on first-order logic resolution [Bachmair and Ganzinger, 2001]. A common approach to ensure both termination and worst-case optimal running time is to parametrise resolution to ensure that the calculus only derives a bounded number of clauses [Nivelle et al., 2000; Hustadt and Schmidt, 2002; Schmidt and Hustadt, 2013; Hustadt et al., 2008; Ganzinger and De Nivelle, 1999; Kazakov and Motik, 2006; Hustadt et al., 2004]. This technique has been implemented for instance, in the KAON2 reasoner for SHIQ. Resolution can also be used to simulate model-building (hyper)tableau techniques [Hustadt and Schmidt, 1999], including blocking methods which ensure termination [Georgieva et al., 2003].

Consequence-based (CB) calculi have emerged as a promising approach to DL reasoning combining features of (hyper)tableau and resolution [Baader et al., 2005; Kazakov, 2009; Kazakov et al., 2012; Bate et al., 2016]. On the one hand, similarly to resolution, they derive formulae entailed by the ontology (thus avoiding the explicit construction of large models), and they are typically worst-case optimal. On the other hand, clauses are organised into contexts arranged as a graph structure reminiscent to that used for model construction in (hyper)tableau; this prevents CB calculi from drawing many unnecessary inferences and yields a nice goal-oriented behaviour. Furthermore, in contrast to both resolution and (hyper)tableau, CB calculi can verify a large number of subsumptions in a single execution, allowing for one-pass classification. Finally, CB calculi are very practical and systems based on them have shown outstanding performance.

CB calculi were first proposed for the EL family of DLs [Baader et al., 2005; Kazakov et al., 2012], and later extended to more expressive logics like Horn-SHIQ [Kazakov, 2009], Horn-SROIQ [Ortiz et al., 2010], and ALCH [Simanˇc´ık et al., 2011]. A unifying framework for CB reasoning was developed in [Simanˇc´ık et al., 2014] for ALCHI, introducing the notion of contexts as a mechanism for constraining resolution inferences and making them goal-directed. The framework has been extended to the DLs ALCHIQ, which supports number restrictions and inverse roles [Bate et al., 2016]; ALCHIO, which supports inverse roles and nominals [Tena Cucala et al., 2017], and ALCHOQ, supporting nominals and number restrictions [Karahroodi and Haarslev, 2017].

To the best of our knowledge, however, no CB calculus can handle DLs supporting simultaneously all Boolean connectives, inverse roles, number restrictions, and nominals. Such DLs, which underpin the standard ontology languages, pose significant challenges for consequence-based reasoning. Indeed, DLs lacking inverse roles, number restrictions, or nominals enjoy a variant of the forest model property, which is exploited by reasoning algorithms. However, no such property holds when a DL simultaneously supports all the aforementioned features; for non-Horn DLs, this results in a complexity jump from ExpTime to NExpTime, and complicates the design of reasoning calculi [Horrocks and Sattler, 2005].

In this paper we present the first consequence-based calculus for the DL ALCHOIQ, which supports all Boolean connectives, role hierarchies, inverse roles, number restrictions, and nominals. By using well-known transformations, our calculus extends to SROIQ, which covers OWL 2 DL except for datatypes [Horrocks et al., 2006]. Following Bate et al. [2016], we encode derived consequences as first-order clauses of a specific form and handle equality reasoning using a variant of ordered paramodulation. To account for nominals we allow for ground atoms in derived clauses and group consequences about named individuals into a root context. We have carefully crafted the rules of our calculus so that it exhibits worst-case optimal performance for the known proper fragments of ALCHOIQ. In particular, it works in deterministic exponential time for all of ALCHOI, ALCHOQ, ALCHIQ and Horn-ALCHOIQ, and in polynomial time for the lightweight DL ELHO. Our calculus is, however, not worst-case optimal for the full logic ALCHOIQ, exhibiting similar worst-case running time as other well-known calculi for expressive DLs [Motik et al., 2009; Kazakov and Motik, 2006]. Nevertheless, the source of additional complexity is very localised and only manifests when disjunction, nominals, number restrictions and inverse roles interact simultaneously-a rare situation in practice. Although our results are theoretical, we believe that our calculus can be seamlessly implemented as an extension of the SRIQ reasoner Sequoia [Bate et al., 2016]. All proofs are presented in an extended version of the paper [Tena Cucala et al., 2018].

2 Preliminaries

Many-sorted clausal equational logic. We use standard terminology for many-sorted first-order logic with equality (≈) as the only predicate. This is w.lo.g. since predicates other than equality can be encoded by means of an entailment-preserving transformation [Nieuwenhuis and Rubio, 2001].

A many-sorted signature Σ is a pair 〈ΣS , ΣF 〉 with ΣS a non-empty set of sorts, and ΣF a countable set of function symbols. Each f ∈ ΣF is associated to a symbol type, which is an n + 1-tuple 〈s1, . . . , sn+1〉 with each si ∈ ΣS . The sort of f is sn+1 and its arity is n; if n = 0, then f is a constant. For each s ∈ ΣS , let Xs be a disjoint, countable set of variables. The set of terms is the smallest set containing all variables in Xs as terms of sort s, and all expressions f(t1, . . . , tn) as terms of sort sn+1, where each ti is a term of sort si. A term is ground if it has no variables. We use the standard definition of a position p of a term t as an integer string identifying an occurrence of a subterm t|p, as well as the standard notion of a substitution, represented as an expression {x1 ↦→ t1, . . . , xn ↦→ tn} containing all non-identity mappings. We represent by t[r]p the result of replacing the subterm in position p of t by a term r of the same sort.

An equality is an expression s ≈ t with s and t terms of the same sort. An inequality is of the form ¬(s ≈ t), and is written as s ̸≈ t. A literal is an equality or an inequality. A clause is a sentence ∀⃗x (Γ → ∆), with the body Γ a conjunction of equalities, the head ∆ a disjunction of literals, and ⃗x the variables occurring in the clause. The quantifier is often omitted, conjunctions and disjunctions are treated as sets, and the empty conjunction (disjunction) is written as ⊤ (⊥).

Let HU s be the set of ground terms of sort s. A Herbrand equality interpretation I is a set of ground equalities satisfying the usual properties of equality: (i) reflexivity, (ii) symmetry, (iii) transitivity, and (iv) t[s]p ≈ t ∈ I whenever t|p ≈ s ∈ I, for each ground term t, position p, and ground term s. For any ground conjunction, ground disjunction, (not necessarily ground) clause, or a set thereof; an interpretation I satisfies it according to the usual criteria, with the difference that each quantified variable of sort s ranges only over HU s . We write I |= α if I satisfies α, and say that I is a model of α. Entailment is defined as usual.

Orders A strict (non-total) order ≻on a non-empty set S is a binary, irreflexive, and transitive relation between elements of S. A strict order induces a non-strict order ⪰ by taking the reflexive closure of ≻. A total order > is a strict order such that for any a, b ∈ S, either a > b or b > a. For any of these orders ◦, we write a ◦ N, if a ◦ b for each b ∈ N, where a ∈ S, N ⊆ S. The multiset extension of ◦ is defined as follows: for S-multisets M and N, we have M ◦ N iff for each a ∈ N\M, there is b ∈ M\N such that b ◦ a, where \ is the multiset difference operator. Order ◦ induces an order between literals by treating each equality s ≈ t as the multiset {s, t}, and each inequality s ̸≈ t as the multiset {s, s, t, t}.

Description Logics DL expressions can be transformed into clauses of many-sorted equational logic in a way that preserves satisfiability and entailment [Schmidt and Hustadt, 2007]. Following standard practice, we use a two-sorted signature with a sort a representing standard FOL terms, and a sort p for standard FOL atoms. The set of function symbols is the disjoint union of a set ΣB of atomic concepts Bi of type 〈a, p〉, a set ΣS of atomic roles Si of type 〈a, a, p〉, a set Σf of functions fj of type 〈a, a〉, and a set Σo of named individuals o of type 〈a〉. A term of the form fj(t) is an fj successor of t, and t is its predecessor. Our signature uses variables {x} ∪ {zi}i≥1 of sort a, where x is called a central variable, and each zi is a neighbour variable. A DL-a-term is a term of the form zi, x, fi(x), or o. A DL-p-term is of the form Bi(zj), Bi(x), Bi(fj(x)), Bi(o), Si(zj, x), Si(x, zj), Si(x, fj(x)), Si(fj(x), x), Si(o, x) or Si(x, o). A DL-literal is either an equality of the form A ≈ true (or just A) with A a DL-p-term, or an (in)equality between DL-a-terms. A DLclause contains only body atoms of the form Bi(x), Si(zj , x), or Si(x, zj), and only DL-literals in the head. To ensure completeness and termination of our calculus, we require that each zj in the head occurs also in the body and that if the body contains two or more neighbour variables zj, then the clause is of the form DL4 in Table 1. An ontology is a finite set of DL-clauses.

An ontology is ALCHOIQ if each DL-clause is of the form given in Table 1. An ALCHOIQ ontology is ALCHOI if it does not contain axioms DL4 and all axioms DL2 satisfy n = 1; it is ALCHOQ if it does not contain axioms DL6; it is ALCHIQ if it does not contain axioms DL7-DL8. Furthermore, it is Horn if each axiom DL1 satisfies n ≤ m ≤ n + 1 and each axiom DL4 satisfies n = 1.

Table 1: DL axioms as clauses. Roles SB2 in DL4 are fresh.

Finally, it is in ELHO if it is Horn and contains only axioms DL1, DL2 with n = 1, DL3, DL5, DL7, or DL8.

3 ACB Algorithm for ALCHOIQ

Consequence-based reasoning combines features of both (hyper-)tableau calculi and resolution. Although the presentation of CB calculi varies in the literature, all CB calculi that we know of share certain core characteristics. First, they derive in a single run all consequences of a certain form (typically subsumptions between atomic concepts, ⊤ and ⊥) and hence they are not just refutationally complete. Second, like resolution, they compute a saturated set of clausesrepresented either as DL-style axioms [Baader et al., 2005; Kazakov, 2009; Simanˇc´ık et al., 2011; 2014] or using firstorder notation [Bate et al., 2016; Tena Cucala et al., 2017; Karahroodi and Haarslev, 2017]-the shape of which is restricted to ensure termination. Third, unlike resolution, where all clauses are kept in a single set, CB calculi construct a graph-like context structure where clauses can only interact with other clauses in the same context or in neighbouring contexts, thus guiding the reasoning process in a way that is reminiscent of (hyper-)tableau calculi. Fourth, the expansion of the context structure during a run of the algorithm is determined by an expansion strategy, which controls when and how to create or reuse contexts.

In the remainder of this section we define our CB calculus, and specify a reasoning algorithm based on it. We then establish its key correctness and complexity properties.

3.1 Definition of the Calculus

Throughout this section we fix an arbitrary ontology O, and we let ΣOf , ΣOB and ΣOS be the sets of functions, atomic concepts and atomic roles in O, respectively; all our definitions and theorems are implicitly relative to O.

The set of nominal labels Π for O is the smallest set containing the empty string and every string ρ of the form Sj1 1 ·...· Sjn n , with jk ∈ N, and Si ∈ ΣS. The set of named individuals ΣOo for O is then defined as {oρ | o individual in O, ρ ∈ Π}. Intuitively, the set ΣOo consists of the individuals occurring explicitly in O plus a set of additional nominals, the introduction of which is reminiscent of existing (hyper-)tableau calculi [Horrocks and Sattler, 2005; Motik et al., 2007].

Following Bate et al. [2016], our calculus for ALCHOIQ represents all derived consequences in contexts as context clauses in many-sorted equational logic, rather than DL-style axioms. Context clauses use only variables x and y, which carry a special meaning. Intuitively, a context represents a set of similar elements in a model of the ontology; when variable x corresponds to such an element, y corresponds to its predecessor, if it exists. This naming convention determines rule application in the calculus, and should be distinguished from variables x and zi in DL-clauses, where the latter can map to both predecessors and successors of the elements assigned to x. Context clauses are defined analogously to [Bate et al., 2016], where the main difference is that we allow context literals mentioning named individuals; furthermore, our calculus defines a distinguished root context where most inferences involving such literals take place. This context represents the non tree-like part of the model, and it exchanges information with other contexts using newly devised inference rules.

Definition 1. A context a-term is a term of sort a which is either x, or y, or a named individual o ∈ ΣOo , or of the form f(x) for f ∈ ΣOf . A context p-term is a term of sort p of the form B(y), B(x), B(f(x)), B(o), S(x, y), S(y, x), S(x, x), S(x, f(x)), S(f(x), x), S(x, o), S(o, x), S(o, o′ ), for f ∈ ΣOf , o and o′ ∈ ΣOo , B ∈ ΣOB , and S ∈ ΣOS . A root context a-term (p-term) is a term of sort a (p) of the form t{x ↦→ o′ }, with t a context a-term (p-term) and o′ ∈ ΣOo . A (root) context atom is an equality of the form A ≈ true, written simply as A, with A a context (root) p-term; a (root) context literal is a (root) context atom, an inequality true ̸≈ true, or an equality or inequality between a-terms (replacing x by o′ ∈ ΣOo ).

A (root) context clause is a clause of (root) context atoms in the body and (root) context literals in the head. A query clause has only atoms of the form B(x), with B ∈ ΣOB .

The kinds of information to be exchanged between adjacent contexts is determined by a set of triggers, which are named after the rules that they activate.

Definition 2. The set of successor triggers Su is the smallest set of atoms satisfying the following properties for each clause Γ → ∆ in O: (i) B(x) ∈ Γ implies B(y) ∈ Su; (ii) S(x, zi) ∈ Γ implies S(x, y) ∈ Su; and (iii) S(zi, x) ∈ Γ implies S(y, x) ∈ Su. The set of predecessor triggers Pr is defined as the set of literals

The set of root successor triggers Sur consists of all atoms B(o), S(y, o) and S(o, y) with B ∈ ΣOB , S ∈ ΣOS and o ∈ ΣOo . The set of root predecessor triggers Prr consists of Sur ∪ {B(y) | B ∈ ΣOB } ∪ {y ≈ o | o ∈ ΣOo }.

The definition of triggers extends that in [Bate et al., 2016] by considering equalities of a variable and an individual as information that should be propagated to predecessor contexts, and by identifying a specific set of triggers for propagating information to and from the distinguished root context.

Same as in resolution and other CB calculi, clauses are ordered using a term order ≻ based on a total order ⋗ on function symbols of sort a. The order restricts the derived clauses since only ≻-maximal literals can participate in inferences.

The following definition specifies the conditions that ≻ must satisfy; although each context can use a different ≻ order, aterms are compared in the same way across all contexts since ⋗ is globally defined. In [Tena Cucala et al., 2018, Appendix A] we show how to construct a context order once ⋗ is fixed.

Definition 3. Let ⋗ be a total order on symbols of ΣOf and ΣOo such that for every ρ ∈ Π, if ρ = ρ′ · ρ′′ , then oρ ⋗ oρ′ . A (root) context order ≻ w.r.t. ⋗ is a strict order on (root) context atoms satisfying each of the following properties:

1. A ≻ x ≻ y ≻ true for each context p-term A ̸= true;
2. n ≻m for each pair n,m ∈ ΣOo with n⋗m;
3. f(x) ≻ g(x), for all f, g ∈ ΣOf with f ⋗ g;
4. t[s1]p ≻ t[s2]p for any context term t, position p, and context terms s1, s2 such that s1 ≻ s2;
5. s ≻ s|p for each context term s and proper position p in s; 6. A ⊁ s for each atom A ≈ true ∈ Pr (Prr ) and context
6. term s /∈ {x, y, true} ∪ ΣOo .

The main difference between Definition 3 and the orderings used in prior work is the additional requirement that the global order ⋗ must satisfy on the set of nominals; this is necessary to ensure both completeness and termination.

We use a notion of redundancy elimination analogous to that of prior work to significantly reduce the amount of clauses derived by the algorithm.

Definition 4. A set of clauses U contains a clause Γ → ∆ up to redundancy, written Γ → ∆ ˆ∈U if

The first condition in Definition 4 captures tautological statements, whereas the second condition captures clause subsumption. Similarly to prior work, clauses A → A are not deemed tautological in our calculus since they imply that atom A may hold in a context.

We next define the notion of a context structure D as a digraph. Each node v, labelled with a set of clauses Sv, represents a set of "similar" terms in a model of O; edges, labelled with a function symbol, represent connections between neighboring contexts. Each context v is assigned a core corev specifying the atoms that must hold for all terms in the canonical model described by the context, and a term order ≻v that restricts the inferences applicable to Sv; since corev holds implicitly in a context, the conjunction corev is not included in the body of any clause in Sv.

Definition 5. A context structure for O is a tuple D = 〈V, E, core, S,⋗,≻〉 where V is a finite set of contexts containing the root context vr; E is a subset of V×V×ΣOf ; core is a function mapping each context v to a conjunction corev of atoms of the form B(x), S(x, y), S(y, x); S is a function mapping each non-root context v to a set of context clauses and vr to a set of root context clauses, ⋗ is a total order and ≻ is a function mapping each (root) context v to a (root) context order ≻v w.r.t. ⋗ where all ⋗ and ≻v satisfy Definition 3.

We now define when a context structure is sound with respect to O. In prior work, soundness was defined by requiring that clauses derived by the calculus are logical consequences of O. Our calculus, however, introduces additional nominals, and clauses mentioning them are not logical consequences of O. Furthermore, not all the the additional nominals generated by our calculus will correspond to actual elements of a canonical model. To address this difficulty, we introduce the following notions of N-reduction and N-compatibility.

Definition 6. Let N be a (possibly empty) set of additional nominals in ΣOo . Interpretation I with domain ∆I is Ncompatible if the following conditions hold for each nonempty nominal label ρ, which we rewrite as ρ = ρ′ · S:

• if oρ ∈ N, I ̸|= S(oρ′ , u) for each u ∈ ∆I ,
• if oρ ̸∈ N, I |= S(oρ′ , oρ), and there is k0 ∈ N s.t. for each u ∈ ∆I , I |= S(oρ′ , u) implies I |= u ≈ oρ′ ·Sk for some k ≤ k0, and for each k > k0, I |= oρ′ ·Sk ≈ oρ′ ·S1'.

The N-reduction N(Γ → ∆) of a clause Γ → ∆ is empty if an element of N occurs in Γ or in an inequality in ∆, and the clause Γ → N(∆) otherwise, with N(∆) obtained from ∆ by removing all literals mentioning a term in N.

Intuitively, given N and a model I of O, the notion of Nreduction tests whether it is possible to map the additional nominals not in N occurring in derived clauses to actual domain elements of I without invalidating the model. This intuition leads to the following notion of soundness.

Definition 7. A context structure D=〈V, E,core,S,⋗,≻〉 is sound if, for every model I of O, there exists a (possibly empty) set N of additional nominals and an N-compatible conservative extension J of I satisfying the following clauses: (i) N(corev ∧ Γ → ∆) for each v ∈ V and each Γ → ∆ in Sv; and (ii) N(coreu → corev{x ↦→ f(x), y ↦→ x}) for each 〈u, v, f〉 ∈ E.

As in existing CB calculi, the rules of our calculus are parameterised by an expansion strategy used to decide whether to create new contexts or re-use already existing ones.

Definition 8. An expansion strategy strat is a polynomially computable function which takes as input a triple (f, K1, D), where f ∈ ΣOf , K1 ⊆ Su, D = 〈V, E, S, core,⋗,≻〉 is a context structure, and returns a triple (v, core,≻) such that core ⊆ K1, ≻ is a context order w.r.t ⋗, and either v /∈ V or otherwise v ̸= vr, core = corev and ≻ = ≻v.

Three expansion strategies are typically considered in practice (see [Simanˇc´ık et al., 2011] for details). The trivial strategy pushes all inferences to a single context v⊤ with empty core and always returns (v⊤,⊤). The cautious strategy only creates contexts for concept names in existential restrictions; it returns (v⊤,⊤) unless f occurs in O in exactly one atom B(f(x)) with B ∈ ΣOB and B(x) ∈ K1, in which case it returns (vB,B(x)). Finally, the eager strategy creates a new context for each conjunction K1 by returning (vK1 , K1).

The inference rules of our calculus are specified in Tables 2 and 3. As in prior work, a rule is not triggered if the clauses that would be derived are already contained up to redundancy in the corresponding contexts. Rules in Table 2 are a simple generalisation of those in [Bate et al., 2016] for ALCHIQ

to take into account that certain rules can be applied to the distinguished root context and that clauses propagated to predecessor contexts may contain ground atoms. The Core rule ensures that all atoms in a context's core hold. The Hyper rule performs hyperresolution between clauses in a context and ontology clauses; in prior work, variable x had to map to itself in the σ used in the rule, but now x maps to an individual if the rule is applied on the root context. The Eq, Ineq and Fact rules implement equality reasoning, and the Elim rule performs redundancy elimination as in prior work. The Pred rule performs hyperresolution between a context and a predecessor context. The rule does not apply to the root context, but the calculus provides another rule for that. Ground and nonground body atoms are treated differently; the latter are simply copied to the body of the derived clause. Finally, the Succ rule extends the context structure using the expansion strategy as in prior work. As in the Hyper rule, variable x maps to a named individual on the root context.

The rules in Table 3 handle reasoning with nominals. Rule Join corresponds to a resolution step between two ground atoms of different clauses in the same context. Rule r-Succ complements Succ by dealing with information propagation from any non-root context to the root context; in turn, r-Pred complements Pred in an analogous way. In contrast to previous calculi, rules r-Succ and r-Pred can be used to exchange information between the root context and any other context, not just a neighboring one; this is due to the fact that nominal reasoning is intrinsically non-local. Finally, rule Nom introduces additional nominals when an anonymous element of the canonical model may become arbitrarily interconnected. The Nom rule does not apply if the input ontology lacks either inverse roles, or nominals, or number restrictions.

3.2 The Reasoning Algorithm and its Properties

We can obtain a sound and complete reasoning algorithm for ALCHOIQ by exhaustively applying the inference rules in Tables 2 and 3 on a suitably initialised context structure. This follows from the calculus satisfying two properties analogous to those required by CB calculi in prior work. The soundness property ensures that the application of an inference rule to a sound context structure yields another sound context structure. The completeness property ensures that any query clause entailed by O will be contained up to redundancy in a suitably initialised context of a saturated context structure.

Theorem 1 (Soundness). Given a context structure D which is sound for O, and an arbitrary expansion strategy, the application of a rule from Table 2 or Table 3 to D with respect to O yields a context structure which is sound for O.

Theorem 2 (Completeness). Let D be a context structure which is sound for O and such that no rule of Table 2 or Table 3 can be applied to it. Then, for each query clause ΓQ → ∆Q and each context q ∈ V such that all of the following conditions hold, we have that ΓQ →∆Q ˆ∈Sq also holds.

• C2. For each context atom A ∈ ∆Q and each A′ of the form B(x) such that A ≻q A′ , we have A′ ∈ ∆Q.
• C3. For each A ∈ ΓQ, we have ΓQ → A ˆ∈Sq.

To test whether O entails a query clause ΓQ → ∆Q, an algorithm can proceed as follows. In Step 1, create an empty context structure D, and fix an expansion strategy. In Step 2, introduce a context q into D, set its core to ΓQ, and initialise the order ≻q in a way that is consistent with Condition C2 in Theorem 2. Finally, in Step 3, saturate D over the inference rules of the calculus and check whether ΓQ → ∆Q is contained up to redundancy in Sq. Such algorithm generalises to check in a single run a set of input query clauses by initialising in Step 2 a context q for each query clause.

Our algorithmmay not terminate if the expansion strategy introduces infinitely many contexts. Termination is, however, ensured for strategies introducing finitely many contexts, such as those discussed in section 3.1.

Proposition 1. The algorithm consisting of Steps 1-3 terminates if the expansion strategy introduces finitely many contexts and rule Join is applied eagerly. If the expansion strategy introduces at most exponentially many contexts, the algorithm runs in triple exponential time in the size of O.

Our algorithm is not worst-case optimal for ALCHOIQ (an NEXPTIME-complete logic), as it can generate a doubly exponential number of additional nominals and a number of clauses per context that is exponential in the size of the relevant signature; thus, each context can contain a triple exponential number of clauses in the size of O. We can show, however, worst-case optimality for the well-known fragments of ALCHOIQ, and thus obtain pay-as-you-go behaviour.

Proposition 2. For any expansion strategy introducing at most exponentially many contexts, the algorithm consisting of Steps 1-3 runs in worst-case exponential time in the size of O if O is either ALCHIQ, or ALCHOQ, or ALCHOI, or if it is Horn. Furthermore, for ELHO ontologies, the algorithm runs in polynomial time in the size of O with either the cautious or the eager strategy.

Note that the strategies discussed in section 3.1 introduce at most exponentially many contexts. We conclude this section with an example illustrating the application of our calculus.

Example 3. Let O1 contain the following clauses.

We check whether O1 |= A(x) → C(x) using the eager expansion strategy. Figure 1 summarises the inferences relevant to deriving the query clause. Clauses 9 to 19 are attached to context vA having core A(x), clauses 20 to 23 to vB1 with core B1(x) ∧ S(y, x), clauses 24 to 27 to vB2 with core B2(x) ∧ S(y, x), and the remaining clauses to the root context vr with empty core.

Consider the state of the context structure once clauses 9 to 13 and 20 to 22 have been derived as in the calculus from Bate et al. [2016]. We apply r-Succ to clause 22, which creates an o-labelled edge to vr and adds clause 28; rule Nom derives clause 29 in vr, with o′ = oS1 an additional nominal. This clause can be back-propagated with r-Pred to yield clause 23 in vB1 ; in turn, this can be back-propagated with Pred to yield clause 14 in vA. Two applications of Eq yield clauses 15 and 16. Proceeding analogously in context vB2 , we derive clauses 24 to 27 and then clauses 17 and 18. Next, we apply r-Succ to clauses 15, 16 and 18 to derive clauses 30 to 32. The Hyper rule can be applied to these clauses to derive clause 33. The head of this clause is in Prr , so we can back-propagate using r-Pred with the edge from vA and clauses 15, 16 and 18 to derive our target, clause 19. ✁

4 Conclusion and FutureWork

We have presented the first CB reasoning algorithm for a DL featuring all Boolean operators, role hierarchies, inverse roles, nominals, and number restrictions. We see many challenges for future work. First, our algorithm runs in triple exponential time, when it should be possible to devise a doubly exponential time algorithm; we believe, however, that deriving such tighter upper bound would require a significant modification of our approach. Second, our algorithm should be extended with datatypes in order to cover all of OWL 2 DL. Finally, we are implementing our algorithm as an extension of the Sequoia system [Bate et al., 2016]. We expect good performance from the resulting system, as our calculus only steps beyond pay-as-you-go behaviour in the rare situation where disjunctions, nominals, number restrictions and inverse roles interact simultaneously.

Acknowledgments

Research supported by the SIRIUS centre for Scalable Data Access, and the EPSRC projects DBOnto, MaSI3 , and ED3 .