We present a consequence-based calculus for the SHOI description logic. Known consequence-based reasoning procedures are either restricted to logics without nominals (e.g. SRIQ), or to Horn logics (e.g. Horn-SROIQ). In line with existing approaches, our algorithm uses context structures to assist in the derivation of clauses, which are generated by inference rules such as (hyper)resolution. These rules are applied only locally|that is, between clauses in either the same context or in neighbouring contexts. In order to deal with interactions between nominals, inverse roles, and disjunction, we allow for a restricted form of non-local inference. Our calculus displays worst-case optimal behaviour, and it is amenable to implementation.
Description logics (DLs) [
Consequence-based (CB) reasoning [
CB reasoning algorithms were originally proposed for the E L family of
lightweight description logics [
We continue this line of work by exploring the extension of CB techniques to non-Horn DLs with nominals. The combination of nominals, inverse roles, and disjunctions poses new challenges, such as the need for deriving clauses expressing non-local dependencies between contexts. We show how to extend the CB calculus for SHI [19] in order to overcome these issues, and we prove that the resulting calculus is a worst-case optimal decision procedure for subsumption in SHOI. We also show that the algorithm displays pay-as-you-go behaviour and, in particular, works in polynomial time when restricted to E LHO ontologies.
Our proposal is related to the deterministic ExpTime tableau calculi for
SHOI presented in [
First-Order Logic We use standard rst-order logic terminology. A signature is pair of nite sets ( A; f ) where A is set of predicates and f is a set of of function symbols of arity 0. A clause is a formula of the form 8x: ! , where (resp. ), called the body (resp. head ) of the clause, is a possibly empty conjunction (resp. disjunction) of atoms, and 8x is a universal quanti cation over all variables occurring in and , which is often omitted. We use > and ? to represent the empty conjunction and disjunction, respectively. We often use set notation to refer to relations between atoms, conjunctions, disjunctions, and clauses.
A substitution is a mapping from variables to terms. It can be expressed as fx1 7! t1; x2 7! t2; : : : g, which contains all mappings in di erent from the identity. The result of applying to a clause C or term t is written C and t , respectively. A position p in a term t = f (t1; : : : ; tn) is a sequence of natural numbers i1 i2 ik which identi es a particular subterm of t. Positions are de ned inductively, with tj = t and tjp = tijp0 for any p; p0; i such that p = i p0. If tjp = s, we write t[s0]p for the result of replacing the subterm s by s0 in position p of term t. Positions are de ned analogously for atoms.
An interpretation I is a pair (DI ; I ), where DI is a non-empty set (the domain), and I is a function which maps every f 2 f of arity k 2 N to a function from (DI )k to DI , and every predicate symbol of arity k 2 N to a subset of (DI )k. For each rst-order sentence ', an interpretation I induces a truth-value 'I in the usual way. An interpretation I satis es a sentence ' i 'I = true, in which case we write I j= '.
Orders A (strict) order on a non-empty set S is a binary, irre exive, transitive, and antisymmetric relation between elements of S. An order induces a non-strict order if it is extended with re exivity. An order is total if for any distinct a; b 2 S, either a b or b a. For any 2 f ; g, we write S a if there is b 2 S with b a. An order on a set S can be extended to an order 0 between subsets of S: given two subsets S1; S2 of S and an order on S, we have that S1 0 S2 if and only if for each element n 2 S2nS1 there is an element m 2 S1nS2 such that m n. Since the meaning will be clear from the context, we refer to an induced order 0 also as .
The SHOI description logic A SHOI ontology in the usual DL syntax
can be transformed in polynomial time and expressed as an equisatis able set
of rst-order clauses as indicated in Table 1, where the left-hand side contains
each possible normalised DL axiom form, and the right-hand side contains the
corresponding rst-order logic clause1. Transitivity axioms are encoded away
through the usual techniques [
Clauses with nominals in rst-order logic can be represented using the equality predicate . In order to deal with this predicate, reasoning procedures either exploit paramodulation techniques [26], or explicitly axiomatise equality. However, the inference rules of our algorithm have equality reasoning embedded into them. This allows us to choose a rst-order representation formalism with the property that the equality predicate will never appear in the clauses manipulated by the algorithm. In order to achieve this, we de ne a function mapping each nominal o in the ontology to a fresh unary predicate (o) = O, and use this predicate in the translation of each DL axiom or fact which features o. If o is the set of all nominals in the ontology signature, we denote as O the set f (o) j o 2 og. In order to preserve satis ability, for each O 2 O, we add an axiom of the form DL8, and we assume that the equality predicate is explicitly axiomatised. However, these axioms will be ignored by our algorithm, as the inference rules only use axioms of the form DL1-DL7, thereby preventing equality from appearing in derived clauses; this ontology subset is denoted O . 1 The type of the generated clauses can be seen as a subset of a broader kind, named
DL-clauses, which are generally used to express axioms of DLs in rst-order logic.
Our proposal builds upon the CB algorithms in [20] and [
The CB algorithms introduced above take an ontology as an input and use it to construct a context structure|a graph where each node v (a context ), represents a unique, speci c set of individuals, and contains clauses that hold only for those individuals, while each edge is labelled by a function symbol f 2 f which is used to represent f -successor relations between terms.
The set of individuals represented by each v is determined by a core, which is a collection of atoms corev in variables y and x with no function symbols. Each v represents those pairs of individuals (t1; t2) in a model I such that I satis es the grounding of the core by = fx 7! t1; y 7! t2g. However, context structures are constrained to ensure that any such pair of individuals is of the form (f I (sI ); sI ) for some term s and f 2 f in the label of an incoming edge. Therefore, we should see each context v as a representation of those individuals t which: (i) are instances of every B(x) 2 corev and (ii) if t = f (t0) for some f in an incoming edge from u, then t0 is represented in u and is an R-successor (or R-antecessor) of t for each R(x; y) (or R(y; x)) in corev. Consequently, for the clauses in a context, variable x ranges over each of these elements t, and variable y represents its immediate predecessor. This stands in contrast with the meaning of variables x and z in Table 1, which range over the interpretation domain as usual.
A set Sv is de ned for each v, and it contains clauses holding speci cally for those individuals represented by v; these clauses should only use variables y and x. A key feature of the consequence-based framework is that only functional terms of the form f (x) (with f 2 f ), are allowed in each Sv. This restriction simpli es the execution of the algorithm, and prevents term nesting, which can lead to termination problems. Moreover, this implies that clauses derived by the algorithm describe constraints which are strictly local, that is, which involve exclusively an element t in the interpretation domain, its possible successors f1(t); ; fn(t), and its ancestor t0, if it exists. However, this does not mean they are localised, since each clause holds not only for one element in the domain, but rather for any element represented by the context.
Once a context structure has been initialised, a set of inference rules is used to expand it by creating new contexts, edges, and deriving new clauses within contexts. These rules also act locally: they only take as input sets of clauses in a particular context v and (possibly) its neighbour, and add their output to these contexts, or to a newly created neighbour of v.
However, when nominals are allowed in the ontology, some form of nonlocal interaction is required, since individuals belonging to unrelated contexts (including contexts that are not even connected in the context structure) can collapse into each other, which may give rise to new consequences that need to be accounted for. As we explain in the next section, our algorithm deals with this issue by allowing clauses to express some non-local restrictions, and by introducing non-local inference rules. 4
Combining Nominals, Inverse Roles, and Disjunction In this section, we demonstrate how the CB approach introduced in [19], with support for disjunction and inverse roles, can be adapted to deal with nominals. We illustrate this by applying our calculus to determine that A v F is entailed by the ontology O given in Table 2, which uses nominals in a non-trivial way.
Suppose we attempt to build a Herbrand model using (a variant of) the hypertableau method. We start the procedure with an element c and the atom A(c). By axioms (1)-(6), we produce descendants f3(f1(c)) and f2(c), in the atoms B1(f3(f1(c))) and B2(f2(c)). By axioms (12) and (18), we also have B3(o3). Now, axioms (13)-(18), imply that each of the elements f3(f1(c)); f2(c); and o3 must be equal to either o1 or o2 (or both). Therefore, at least two of these three elements must be equal, even though we do not know which nominal they are equal to. As a result, in any branch, one of the axioms (7)-(9) can be used to derive either C(f2(c)) or C(f3(f1(c))). This can resolved with axioms (10) and/or (11) to obtain F (c), as desired.
The restriction that two of the three elements in ff3(f1(c)); f2(c); o3g must be equal is no longer local; in fact, f3(f1(c)) and f2(c) are not even connected to o3 in the tableau. This suggests that a consequence-based procedure should contain clauses which represent relations other than those between neighbouring individuals. However, if we allow for more variables in a context, to refer to elements in arbitrary distant contexts, the consequence-based method quickly collapses into a procedure analogous to resolution.
Instead, our algorithm allows only references to nominals in context clauses, in addition to the local individuals represented by y; x; f (x). This introduces the possibility of having ground atoms in context clauses. We also introduce nonlocal inference rules, which take a context as an input, and either a (possibly disconnected) nominal context, which represents a single nominal, or a special context known as the root context, where ground resolution can be applied.
In Figure 1, we illustrate how the algorithm works by applying it to the ontology O of Table 2. The algorithm is initialised with a root context v0 with core A(x), corresponding to the body of our query. We also create contexts vo1 , vo2 , and vo3 for the corresponding nominals, with cores O1(x), O2(x), and O3(x), respectively. Back in the root context, we use hyperresolution with axioms (1)(4) to derive clauses (23)-(26). Observe that we cannot resolve clause (23) with axioms (5) or (6), since that would lead to nested function terms. Instead, we rst have to create a successor context v1 with a Succ rule, apply the Core rule to generate the equivalent clause (28), and then we can apply those axioms to generate clause (30). Further applications of hyperresolution and generation of new successors lead to the clause > ! O1(x) _ O2(x) appearing in contexts v3 (which represents, among others, the term f3(f1(c))), v2 (id. for f2(c)) and v4 (id. for o3). We are now in the situation described above, where non-local inferences are required to derive further consequences.
We achieve this by using a new rule Split which generates atoms grounded in nominals. For instance, we apply this rule to clauses (33) and (35), selecting O2(x) to generate clause (42). The Split rule also introduces clause (43) in the context vo2 corresponding to the selected nominal, in order to explore the consequences of B1(o2). We follow the same procedure in v2, which adds clause (48) also to vo2 . These two clauses can now be resolved with axiom (9) to generate (49). This clause can be relevant to contexts v3 and v2, so we propagate it back to these contexts with a new rule Exp and obtain (50). Now C(x) can be resolved together with clause (34) with axiom (10) to derive (51). Then, we can apply again Split, selecting O1(x) and, after a similar procedure, we derive clause (58). Since the head of this clause involves exclusively the predecessor of x, it can be propagated back to context v1 with a rule Pred, and then, with axiom (11) and again the Pred rule, we derive (61) in v0.
In order to derive F (x) unconditionally in this context, we must show that the ontology either satis es both B2(o2) and B3(o1), or it derives F (x) by other means. We can explore the alternatives to satisfying B2(o2) starting from clause (47). Using a similar procedure to the one presented above with Split and Exp rules, and propagating the result (66) to the root context with Pred, we obtain (67). We then use a rule Join to resolve ground atoms in the root context to derive (68). Now, since clause (54) is grounded, we can copy it in the root context using a rule Root speci cally for this purpose. Using Join leads to (70). Core: > ! D(x) (28) Core: > ! R(y; x) (29) Hyper[5+28]: > ! B(f3(x)) (30) Hyper[6+28]: > ! R(x; f3(x)) (31) Pred[32+58]: B2(o2) ^ B3(o1) ! F (x) (59) Hyper[11+29+59]: B2(o2) ^ B3(o1) ! F (y) (60) Pred[32+75]: B2(o1) ^ B3(o2) ! F (x) (77) Hyper[11+29+77]: B2(o1) ^ B3(o2) ! F (y) (78)
Succ[23+24]: The only remaining task is to follow a symmetric procedure to derive (83), and using Join once again to obtain > ! F (x) in the root context.
vo1 Initialisation: > ! O1(x) (21) Split[37+39]: B1(x) ! B1(x) (46) Split[40+52]: B3(x) ! B3(x) (55) Hyper[8+46+55]: B1(x) ^ B3(x) ! C(x) (56) Split[37+47]: B2(x) ! B2(x) (63) Hyper[8+55+63]: B2(x) ^ B3(x) ! C(x) (64) Hyper[7+46+63]: B2(x) ^ B3(x) ! C(x) (71) Hyper[8+46+55]: B1(x) ^ B3(x) ! C(x) (73)
De nition 1 (Context terms, literals, and clauses). A context term is a term of the form x; y; f (x) for some f 2 f , or o for some o 2 o. A context atom is an atom of the form C(x), C(y), C(f (x)), R(x; y), R(y; x), R(x; f (x)), R(f (x); x), or C(o), with R a binary predicate in A, and C a unary predicate in A [ O. A context clause is a clause where all literals are context atoms, and which contains no function symbols in the body. A query clause contains only unary predicates B 2 A.
The sets we de ne next, called trigger sets, are collections of atoms which guide the application of inference rules. To give an example of how they work, consider the Succ rule, which carries information from a context v to a successor. The rule can only be applied if there is a context with a clause such that a successor trigger is in the clause.
De nition 2 (Trigger sets). The set of successor triggers is de ned as follows Su(O) = fB(x) j exists
! fR(y; x) j exists 2 O s.t. B(x) 2 and B 2
A
Observe that Pr(O) does not contain any O(y), and Su(O) does not contain any O(x). We also de ne an ordering for the atoms in the clauses; adding order to the technique reduces the amount of required computation.
De nition 3 (Context order). Let m be an arbitrary total order on function symbols. Let m0 be an order induced by m on terms such that f (x) m0 x m0 y, for any f 2 f and for each pair f; g of function symbols such that f m g, we have f (x) m0 g(x). A context order is a strict order on context atoms such that: (i) For each atom A, if t m0 s then A[t]p A[s]p, (ii) for any atom A 2 Pr(O) with variable y, we have A A0 for any other context atom A0.
Such an order always exists: consider an arbitrary lexicographic path order
[
We use a notion of redundancy to simplify the calculus by allowing for elimination of clauses that are subsumed by others in the context structure. De nition 4 (Redundancy). A set of clauses U contains a clause to redundancy (abbreviated u.t.r.), if and only if there exist 0 and such that 0 ! 0 2 U . We write ! 2^ U . ! 0 up
The annotated graph which guides the algorithm execution is de ned next: De nition 5 (Context structure). A context structure for an ontology O is a tuple D = hV; E ; core; S; ; ri, where V is a nite set of elements denominated contexts; E is a subset of V V f , that is, a nite set of directed edges between contexts, labelled by a function symbol; core is a function that assigns to each context a conjunction corev of atoms of Su(O); S is a function which maps every context v to a set of context clauses Sv; is a function which assigns to each context v a context order v, and r(V) is a function which chooses a context of V, denominated the root context.
The following de nes a notion of soundness for context structures, which is preserved as an invariant during the algorithm execution.
De nition 6 (Sound context structure). A context structure is sound if and only if for each context v 2 V and each context clause ! in Sv, we have: O j= 8x8y: (corev(x; y) ^ ! ) ; and for each edge hu; v; f i 2 E , we have:
O j= coreu ! corevfx 7! f (x); y 7! xg:
The rules of the algorithm require an expansion strategy, which is a \policy" for deciding whether to create new contexts or re-use existing ones. De nition 7 (Expansion strategy). An expansion strategy strat is a polynomially computable function which takes as input a triple (f; K; D), and returns another triple (v; core; ). In the input, f is a function symbol, K is a set of atoms with predicates in A, and D is a context structure. The output consists of a core core K which does not contain predicates in O, a context v which is either fresh or such that core = corev, and a context order .
Typically, three main natural expansion strategies are considered, depending on which nodes and core functions they return (the context order is chosen arbitrarily): the trivial strategy, which always returns (v>; >), with v> a xed context with empty core; the cautious strategy, which returns (vB; B(x)) if f occurs in O only in an atom B(f (x)), and (v>; >) otherwise, and the eager strategy, which returns (vK ; K); the latter was used in the example above.
The inference rules for our calculus are in Table 3. We assume, for simplicity, that repeated atoms are eliminated before adding a clause to a context. An execution of the algorithm on query Q ! Q chooses an expansion strategy and initialises a context structure D with a context r(V) = q with coreq = Q, an order q which satis es condition C2 of Theorem 2, a context vo for each o 2 o, with corevo = O(x), and an order o. Then, it saturates D by applying the inference rules in table 3 w.r.t. O until no further rules can be applied. Due to the following claims, which we prove in [24], we then have that Q ! Q 2^ Sq if and only if the query is entailed by O.
Theorem 1 (Soundness). Given an ontology O, a context structure D sound for O, and an arbitrary expansion strategy, the application of a rule from Table 3 to D with respect to O yields a context structure D0 which is sound for O.
Theorem 2 (Completeness). Let O be a normalised SHOI ontology, and D a context structure which is sound for O and such that no rule of Table 3 can be applied to it. Given a query clause Q ! Q with coreq = Q, we have that
Q ! Q 2^ Sq holds if: C1 O j= Q ! Q .
C2 For each context atom A(x) 2 Q and each context atom A0(x) such that
A(x) q A0(x), we have A0(x) 2 Q.
C3 For each A 2 Q, we have Q ! A 2^ Sq.
Proposition 1 (Worst-case optimality). For any expansion strategy introducing a number of contexts exponentially bounded with the size of the ontology, the consequence-based calculus presented in this section works in exponential time.
Indeed, the number of possible atoms that the algorithm can generate is quadratic
on the signature size (in binary atoms, only one term has function symbols), so
the number of possible clauses in a context is exponential on the size of O. Since
there is an exponential maximum number of contexts, at most exponentially
many clauses can be generated. Since each inference uses a quadratic number
of clauses, there are at most exponentially many inferences, which shows that
the algorithm works in exponential time. Given that subsumption is
ExpTimecomplete for SHOI [
Proposition 2 (Pay-as-you-go behaviour). For E LHO ontologies and queries of the form B1(x) ! B2(x), the calculus runs in polynomial time with the eager strategy.
Indeed, with the eager strategy, all derived clauses are of the form > ! B(x),
and since there are no universal quanti ers, a number of contexts at most
quadratic is derived. The nominal rules simply exchange clauses between
contexts if > ! O(x) is derived, similarly to the E LHO algorithm in [
We have presented the rst worst-case optimal consequence-based calculus for SHOI, a description logic with disjunction, inverse roles, and nominals, using explicit ground inferences to exchange information non-locally between contexts. The calculus becomes analogous to known procedures for ALC and E LHO whenever the ontology is restricted to those DLs. Further work will consider the extension of the technique presented here to counting quanti ers, which will pose a greater challenge since SHOIQ is known to be NExpTime-complete. 2741, pp. 412{426. Springer (2003), \url{http://www.cs.man.ac.uk/~schmidt/ publications/SchmidtHustadt03b.html} 19. Simanc k, F., Kazakov, Y., Horrocks, I.: Consequence-based reasoning beyond Horn ontologies. In: Proc. of the 22nd Int. Joint Conf. on Arti cial Intelligence (IJCAI 2011). pp. 1093{1098 (2011), download/2011/SiKH11a.pdf 20. Simanc k, F., Motik, B., Horrocks, I.: Consequence-based and xed-parameter tractable reasoning in description logics. Arti cial Intelligence 209, 29{77 (2014), download/2014/SiMH14a.pdf 21. Sirin, E., Parsia, B., Cuenca Grau, B., Kalyanpur, A., Katz, Y.: Pellet: A practical OWL-DL reasoner. J. of Web Semantics 5(2), 51{53 (2007), http://www. mindswap.org/papers/PelletJWS.pdf 22. Spackman, K.: Managing clinical terminology hierarchies using algorithmic calculation of subsumption: Experience with SNOMED-RT. J. of the Amer. Med.
Informatics Ass. (2000), fall Symposium Special Issue 23. Steigmiller, A., Liebig, T., Glimm, B.: Konclude: System description. J. of Web Semantics 27(1) (2014), http://www.websemanticsjournal.org/index.php/ps/ article/view/366 24. Tena Cucala, D., Cuenca Grau, B., Horrocks, I.: Consequence-Based Reasoning for Description Logics with Disjunction and Nominals. Tech. rep., University of Oxford, http://bit.ly/2pY2UrN (2017) 25. Tsarkov, D., Horrocks, I.: FaCT++ description logic reasoner: System description.
In: Proc. of the Int. Joint Conf. on Automated Reasoning (IJCAR 2006). Lecture Notes in Arti cial Intelligence, vol. 4130, pp. 292{297. Springer (2006), download/ 2006/TsHo06a.pdf 26. Wos, L., Robinson, G.: Paramodulation and theorem-proving in rst-order theories with equality. In: Michie, D., Meltzer, B. (eds.) Proceedings of the 4th Annual Machine Intelligence Workshop. Edinburgh University Press (1969)