We present a non-deterministic consequence-based procedure for the description logic ALCHI. Just like the similar style (deterministic) procedures for EL and Horn-SHIQ, our procedure explicitly derives subsumptions between concepts, but due to non-deterministic rules, not all of these subsumptions are consequences of the ontology. Instead, the consequences are only those subsumptions that can be derived regardless of the choices made in the application of the rules. This is similar to tableau-based procedures, for which an ontology is inconsistent if every expansion of the tableau eventually results in a clash. We report on a preliminary experimental evaluation of the procedure using a version of SNOMED CT with disjunctions, which demonstrates some promising potential.
Consequence-based and tableau-based methods are two well-known approaches to
reasoning in Description Logics (DLs). The former work by deriving logical consequences
of axioms in the ontology using inference rules while the latter by building
countermodels for conjectures. Historically, consequence-based methods have been applied to Horn
DLs, most prominently, the E L family [
The most straightforward attempt to combine the best from both worlds is to
implement both a consequence-based and a tableau-based procedure and use one or
another depending on the ontology. Indeed, several tableau reasoners, including Pellet and
Konclude, switch to a consequence-based algorithm for E L inputs. A more advanced
approach, is to automatically split the ontology into parts and use a consequence-based
algorithm for the deterministic part (which often covers nearly all of the ontology) and
tableau for the rest. Such reasoners as MORe [
Another line of research is to extend consequence-based calculi to deal with
nondeterminism. One notable approach has been developed for ConDOR, a reasoner for
full ALCH [
In this paper we present another consequence-based procedure for a non-Horn logic,
this time for ALCHI, but instead of resolution we incorporate some of the tableau
features into our inference rule system. Specifically, we present non-deterministic rules
with alternative conclusions to deal with non-determinism (instead of deriving
disjunctions) and prove soundness, completeness, and termination of the corresponding
saturation procedure. We show that our procedure is another step towards combining the best
from the consequence-based and tableau-based worlds: It retains the optimal worst-case
complexity, goal directedness, and the “granularity” property of consequence-based
reasoning (i.e. computation of subsumers for different concepts can be done with
limited interaction which enables concurrent [
Finally, we present results of a preliminary evaluation using Horn ontologies and
the same disjunctive extension of the anatomical part of SNOMED CT which was used
to evaluate ConDOR (SCT-SEP) [
The syntax of ALCHI is defined using a vocabulary consisting of countably infinite sets of atomic roles and atomic concepts. We use the letters R; S for roles, C; D for concepts, and A; B for atomic concepts. Complex concepts are defined by the grammar
C(i) ::= > j ? j A j C1 u C2 j C1 t C2 j :C j 9R:C j 8R:C;
where R is either an atomic role or its inverse (written R ). Semantics is defined in the
standard way; formal details can be found in the technical report [
An ALCHI ontology is a finite set of concept inclusion and role inclusion axioms of the form C v D and R v S, respectively. The ontology classification task requires to compute all entailed subsumptions between atomic concepts occurring in O.
An ALCHI ontology O is Horn if for every axiom C v D, the concepts C and D satisfy, respectively, the following grammar definitions:
C(i) ::= > j ? j A j C1 u C2 j C1 t C2 j 9R:C;
D(i) ::= > j ? j A j D1 u D2 j 9R:D j 8R:D j :C: That is, negations and universal restrictions should not occur on the left-hand side of concept inclusions, and disjunctions should not occur on the right-hand side.
A consequence-based procedure for Horn-ALCHI can be presented using the rules
in Fig. 1. These rules are similar to the rules for Horn-SHIQ [
: > 2 sub(O) is that they can operate directly on complex concepts without requiring the ontology to be normalized. Here we denote by sub(O) the set of concepts occurring in the ontology O (possibly as subconcepts). The rules derive subsumptions of the form H v U with
U :: = ? j C j 9R:K; H; K :: = di2I Ci; (1) (2) where Ci 2 sub(O) (i 2 I) and C 2 sub(O). The premises of each rule (if any) are given above the horizontal line, the conclusion below, and the side conditions that determine when each rule is applicable (in terms of O) after the colon.1 Note that the concept inclusion axioms in O are used not as premises of the rules but as side condition of Rv. The side conditions of the rules R8 , R9 , R8!, and R9! use the precomputed role hierarchy vO, which is the smallest reflexive transitive relation on roles such that R v S 2 O implies R vO S and R vO S . It can be shown (and follows from the more general result of this paper) that the inference system in Fig. 1 is sound and complete for deriving all entailed subsumptions with concepts occurring in the ontology, namely that for every C 2 sub(O) and every H of the form (2), we have O j= H v C iff either H v ? or H v C is derivable by the rules in Fig. 1 for O. 3
Non-Deterministic Consequence-Based Reasoning in ALCHI
Extending consequence-based procedures beyond Horn DLs is difficult because dealing
with non-deterministic constructors, such as disjunction, requires reasoning by case. In
tableau-style procedures which construct (representations of) models, dealing with
nondeterministic constructors is straightforward: if a domain element is an instance of BtC
then it should be an instance of B or C. In consequence-based procedures that derive
entailed subsumptions directly, this kind of principle is not valid: if A v B tC is entailed,
1Rule Rt+ stands for two rules with single premises H v C1 and H v C2 respectively.
then it is not true that either A v B or A v C is entailed. The consequence-based
procedure for (non-Horn) ALCH [
One of the well-known disadvantages of resolution-based procedures compared to search-based (DPLL-style) procedures, is that resolution can produce many long disjunctions which can occupy a considerable amount of space and make inferences slow because merging disjunctions is not a trivial operation. In this paper we, thus, reconsider the former idea of splitting disjunctions using a non-deterministic rule: R
H v C1 t C2
t H v C1 j H v C2
Just like in tableau-based procedures, this rule creates two branches in which
subsumptions can be independently derived. As discussed above, it is not true that all
subsumptions derived in one of the branches will be entailed by the ontology. However, it can
be the case for the subsumptions that are derived on every branch, i.e., regardless of
the non-deterministic choices made. For example, if we split subsumption A v B t C
on A v B and A v C, then in both branches we can derive A v D using axioms
B v D 2 O and C v D 2 O respectively. This idea of considering common
conclusions in all non-deterministic branches is somewhat reminiscent of the Stålmarck’s
procedure for propositional logic (see, e.g., [
As can be seen, A v B can be derived in both of these branches, but O 6j= A v B.
To understand the problem in Example 1, we first need to understand how to interpret rules like (3). Given an interpretation I = ( I ; I ), we say that an element a 2 I satisfies a subsumption C v D in I (or C v D is satisfied in I by a) if a 2 CI implies a 2 DI . So, rule Rt can be understood as follows: for each a 2 I if a satisfies the premise H v C1 t C2 then it satisfies one of the conclusions H v C1 or H v C2. Clearly, this is true for this rule (and every I), however, this property fails for rules R? , R8 , and R9 in Fig. 1, even if I j= O. For a counter-example, take I = ( I ; I ) with
I = AI = fa; bg, BI = fbg, CI = fag, and SI = RI = fha; bi; hb; aig. Clearly, I is a model of O in Example 1, and a satisfies both A v 9R:A and A v C, but, a does not satisfy the conclusion A v 9S:C obtained from these premises by R9 . Hence, the inference by R9 in Example 1 is unsound.
To “fix” rule R9 , we use a similar observation as in ConDOR [
H v 9R:K K v C H v 9S:C j H v 9R:(K u :C) : 9S:C 2 sub(O)
R vO S (4) Example 2. Consider the ontology O from Example 1. Using the updated rule (4), we can now obtain the following inferences for A:
Note that in the rightmost branch, we derive the subsumption A v 9R:(A u :C) to which rule R9 can potentially be applied. In order to check if this rule is applicable, we need to derive subsumptions for A u :C:
A u :C v A A u :C v 9R:A A u :C v B t C
If we now consider the rightmost branch in the derivation for A and the leftmost branch for A u :C we obtain a set of subsumptions for which all inferences are applied but neither A v B nor A v ? is derived. Hence, we can conclude that O 6j= A v B.
Figure 2 presents a generalization and extension of the rules in Fig. 1 to (full) ALCHI using the idea similar to rule (4). The new rules now derive subsumptions R+ R R R R: R? of the form H v U , where U is of the form (1), and
H; K := l Ci u l :Dj ; i2I j2J (5) where Ci 2 sub(O) (i 2 I), and Dj 2 sub(O) (j 2 J ). Note that the rule R? has remained the same, and is still formally unsound under our new interpretation. This rule will be dealt with by our procedure in a special way, which does not affect soundness. 3.1
Just like for other consequence-based procedures [
Theorem 1 (Completeness). Let O be an ALCHI ontology, H a conjunction of form (5), D a concept occurring in O such that O j= H v D, and M a set of subsumptions closed under all rules in Fig. 2. Then either H v D 2 M or H v ? 2 M .
The proof of Theorem 1 (cf. [
: 8
It is possible to prove the converse of Theorem 1, namely that if O 6j= H v D, then there exists a set of subsumptions M closed under the rules in Fig. 2 that contains neither H v D nor H v ?. This result, however, is not very useful in practice because in order to check whether O j= H v D using this result, one would need to enumerate all M closed under the rules in Fig. 2. Just like tableau-based procedures do not need to enumerate all completion graphs, we do not need to enumerate all such closed sets M . In particular, subsumptions derived for different conjunctions H of the form (5) can be in most cases considered independently.
The following concept satisfiability procedure (short CSAT) checks satisfiability of conjunctions H of the form (5) using the rules in Fig. 2: 1. We apply the inference rules in Fig. 2 (introducing conjunctions H as necessary according to Remark 1) and record every derived subsumptions H v U in a separate local branch for each H, just like in Example 2. 2. If a subsumption H v U was derived using a non-deterministic rule, we also remember the alternative conclusion of this rule in a branching point. 3. If we derive a local clash H v ?, we remove all conclusions on the branch for H starting from the last non-deterministically derived conclusion, and produce the alternative conclusion, which we now consider as deterministically derived. 4. If local clash H v ? is derived and there are no non-deterministically derived conclusions on the branch for H anymore, we mark H as inconsistent. 5. Rule R? is applied only if for the right premise of the rule K v ? (local clash in the branch for K), the conjunction K is marked as inconsistent. 6. The procedure terminates when no more rules can be applied and for each derived local clash H v ? (on the branch for H), H is marked as inconsistent.
Note that even though we apply rule R? in a restricted way, because of the last condition, the resulting set M of subsumptions will be closed under all rules in Fig. 2. Also note that if some conclusion H v U was derived using a premise K v V with K 6= H (using rules R? , R8 or R9 ), we do not remove K v V when we backtrack H v U as we remove only conclusion on the local branch for H. Likewise, if we remove the premise K v V , we do not need to remove the conclusion H v U derived from this premise. In other words, premises from other local branches can never result in inconsistency of H, and so, deriving and backtracking of conclusions can be performed for each local branch independently.
By Theorem 1, each H that is not marked as inconsistent by our procedure must be satisfiable since H v ? 2= M for the resulting closure M . We will also prove the converse, namely that only unsatisfiable H can be marked as inconsistent by CSAT.
The rules in Fig. 2 can be used not only for checking satisfiability of H, but also for computing its entailed subsumers. The following branch exploration procedure (short BEXP) continues after CSAT, and computes the set S(H) of concepts D such that H v D appear on every branch of H that does not contain a local clash: 1. For each H not marked as inconsistent, create a set S(H) of candidate subsumers consisting of those D 2 sub(O) such that H v D is on the branch for H. 2. Remove all conclusions on the branch for H starting from the last non-deterministic conclusion, and produce the alternative conclusion. 3. Apply the rules like in CSAT (this may extend other branches), backtracking if necessary, but do not mark H as inconsistent when no backtracking in H is possible. 4. After all rules are reapplied and there is no local clash in H, remove from S(H) all
D for which H v D no longer occurs on the branch. 5. Repeat from Step 2 until no non-deterministic conclusions are left on the branch.
It follows from Theorem 1, that S(H) contains all concepts D 2 sub(O) such that O j= H v D since D is removed from S(H) only when we find M closed under the rules in Fig. 2 such that H v D 2= M . In the next section we prove the converse, namely that if O 6j= H v D then there is a branch of H that does not contain H v D. 3.2
To prove soundness of the procedures CSAT and BEXP described in the previous section, we need to formally define our non-deterministic derivation strategy. Definition 1 (Tableau, Local Tableau). A tableau (for O) is a triple T = (H; ; t), where H is a set of conjunctions of the form (5), is a partial order on H, and t is a function that assigns to every H 2 H a tree t(H) called the local tableau for H whose nodes are labeled by subsumptions H v U (with this H), U of the form (1), such that: 1. For each node n of t(H), there is a rule in Fig. 2 for O such the label of n is a conclusion of this rule and all premises of the form H v U (with this H) are labels of some ancestors of n (the nodes on the path from the root of t(H) to n without n); if the inference is by R? , the second premise K v ? must be such that K H. 2. If the label is obtained by a non-deterministic rule (Rt , R:+, R8+, R8 , R9 ), the node should have a sibling node labeled by the alternative conclusion of the rule. 3. All labels of the nodes on the same branch in t(H) must be different. 4. If K H then all branches of t(K) must contain the local clash K v ?.
Intuitively, each local tableau t(H) for H describes the set of branches that are encountered for H by procedure BEXP described in Sect. 3.1. For example, the two trees in Example 2 are local tableaux respectively for H = A and H = A u :C. The partial order is the order in which the conjunctions H are marked as inconsistent. According to the last condition, we set K H if K is marked as inconsistent and H is not. Thus, rule R derives H v ? from K v ? by our procedure only if K H.
? Theorem 2 (Soundness). Let T = (H; ; t) be a tableau for O. Then for each H 2 H and each concept D (not necessarily occurring in O) such that O 6j= H v D, there exists a branch in t(H) that contains neither H v ? nor H v D.
Proof. The proof is by induction on . Assume that the claim holds for each K H, and prove it for H. Since O 6j= H v D, there is a model I = ( I ; I ) of O and a 2 I such that a does not satisfy H v D in I, i.e., a 2 HI n DI . We prove that there is a branch in t(H) such that every label H v U on this branch is satisfied in I by a, that is a 2 U I . This implies that neither H v ? nor H v D occurs on this branch.
It is sufficient to show that for every node n in t(H), if a satisfies the labels of all ancestors of n then a satisfies the label of n or of its sibling node (if there is one). According to Definition 1, these labels are obtained by some rule in Fig. 2 in which all premises of the form H v U must be the labels of some ancestors of n. That is, all premises of the rule with the left-hand side H are satisfied in I by a. We will show that in this case, the conclusion of the rule (respectively, one of the non-deterministic conclusions if the rule is non-deterministic) is also satisfied in I by a: – Rules R0, R?, R+>, Rv, Ru , Ru , R: , Ru+, Rt+, R:+, R8!, R9!: These are deterministic rules that contain only premises with the left-hand side H. It is easy to see that for all these rules the conclusion is a logical consequence of the premises and O. Since I j= O, a satisfies the conclusion because it satisfies all premises. – Rules Rt , R:+, R8+, R8 , R9 : These are non-deterministic rules. For each rule we show how to choose one of the conclusions that is satisfied in a.
For Rt , since a 2 (C1 t C2)I , we have either a 2 C1I or a 2 C2I . Hence a satisfies either H v C1 or H v C2. The proofs for R+ and R+ are similar. : 8 For R8 , we have a 2 (9R:K)I . That is, there exists b 2 KI such that ha; bi 2 RI . Since R vO S , we have hb; ai 2 SI . If a 2 CI , then a satisfies the left conclusion H v C. Otherwise, a 2= CI and so b 2= (8S:C)I since hb; ai 2 SI . Hence b 2 (K u :8S:C)I and a 2 9R:(K u :8S:C). So, a satisfies the right conclusion H v 9R:(K u :8S:C). The proof for R9 is similar. – RKul6=e RH?. B:TyhDiseifisnaitdioenter1m,hinoiwsteicverru,lwe,ebumtufsotrhitasvreigKht preHm,isaendKsov, e?vewrye bmraaynchhavoef t(K) contains K v ?. Since K H, by induction hypothesis, O j= K v ? (if O 6j= K v ? there would be a branch in t(K) without K v ?). So, this case is not possible since a must satisfy the premise H v 9R:K, but a 2= (9R:K)I = ;. pRreomoafrokf2T.hNeoorteemtha2t. tThehasteciso,ntdhepsreempriesemsisoefsrudloesnRot8haavnedaRny9 imwpearcetnoont ussoeudndinnetshse. The purpose of these premises, is to restrict the non-deterministic “guessing” made by these rules to the cases that are sufficient for completeness. Note also that if the second premises of these rules are entailed by the ontology, e.g., they are derived deterministically, then the right conclusion is equivalent to H v ?, thus it cannot be satisfied by a that does not satisfy H v D. Hence the right conclusion is not necessary in this case, and so, these rules could be applied deterministically as in Fig. 1. This strategy makes sure that our procedure is deterministic when applied to Horn-ALCHI ontologies.
To combine Theorems 1 and 2 and obtain soundness and completeness for our procedure, we need to define when the tableau is fully expanded under inferences. Definition 2 (Fully Expanded Tableau). Let T = (H; ; t) be a tableau. A branch of t(H) is closed if H v ? occurs on this branch. Otherwise, the branch is called open. A branch is fully expanded if there exists a set M of subsumptions closed under the rules in Fig. 2 such that all subsumptions of the form H v U in M (with this H) occur on this branch. T is fully expanded if every open branch of every t(H) is fully expanded.
Note that each time all rules are reapplied without producing a local clash at Step 4 of procedure BEXP in Sect. 3.1, we obtain a set M closed under the rules (possibly different from the previous one). So, we “fully expand” every branch in our procedure. However, BEXP is far from enumerating all possible sets M closed under the inference rules. E.g., we do not explore all possible combinations of branches in local tableaux. Corollary 1 (Correctness). Let T = (H; ; t) be a fully expanded tableau for O. Then for every H 2 H and every D occurring in O, we have O j= H v D iff the subsumption H v D is derived in every open branch of t(H).
It is possible to prove that BEXP runs in exponential time in the size of O.
Informally, the running time is bounded by the sum of sizes for each local tableau. There are
at most exponentially many local tableaux (one per each conjunct H), and it can
further be shown that the size of each local tableau is also exponential. See the technical
report [
The branch exploration procedure BEXP described in Sect. 3.1 can be readily used for classification, i.e., computing the entailed subsumption between atomic concepts in O. We need to iterate over all singleton conjuncts H of atomic concepts, and for each one compute the set S(H) of atomic concepts, subsumptions with which occur on every branch. Another way to compute atomic subsumers for H, is to reduce subsumption entailment to concept satisfiability testing, as done in tableau-based procedures: O j= H v D iff O j= H u :D v ?.We can use our first procedure CSAT for this purpose. The next example demonstrates the key differences between these two approaches. Example 3 (Long Fork). Consider the ontology O containing the following axioms: A v B t C; B v D; C v D; D v D1 u u Dn; (n > 0): The two branches in the tree for H = A contain the following sets of atomic subsumers for A: S1(A) = fA; B; D; D1; : : : ; Dng, and S2(A) = fA; C; D; D1; : : : ; Dng. Hence the procedure BEXP can find the set of common subsumers S(A) = S1(A) \ S2(A) = fA; D; D1; : : : ; Dng in O(n) steps. If we use CSAT instead and test satisfiability for each candidate A v Di, (1 i n), then we potentially need O(n2) steps since for each Hi = A u :Di we can produce O(n) conclusions A u :Di v Dj , 1 j n.
This difference between the two strategies can be observed not only on toy examples
but also on real ontologies (cf. [
Tableau reasoners usually implement further optimizations exploiting a partially
constructed taxonomy that can reduce the number of subsumption tests [
We used the July 2013 release of SNOMED CT,2 an E L+-restricted version of GALEN, and the version of SNOMED CT with disjunctions mentioned in the introduction (SCT-SEP). Performance is tested on classification and the results are averaged over 5 runs (excluding 2 warm-ups). We used a PC with Intel Core i5-2520M 2.50GHz CPU, running Java 1.6 with 4GB of RAM available to JVM.
Performance results of classification are presented in Table 1. The procedure works in two steps as described in Sect. 3.1: satisfiability testing for all atomic concepts using CSAT, then exploring branches to compute subsumers using BEXP. First, the results show that our implementation is slightly faster than ConDOR and considerably faster than Konclude on SCT-SEP. Second, it is comparable to ELK on deterministic E L+ ontologies. The numbers for ELK with 1 and 4 worker threads demonstrate that the difference is mostly due to concurrency: our implementation does not perform computations in parallel yet. BEXP is not necessary for this case as everything is deterministic. In this paper, we presented a non-deterministic consequence-based reasoning procedure for ALCHI, proved its correctness, and presented some promising preliminary evaluation. The procedure retains many nice properties of previously known consequencebased methods, such as optimal worst-case complexity, but also employs some tableaulike features, such as backtracking, without need for blocking to achieve termination.
Our future plan is to extend the implementation to fully support ALCHI, integrate some optimizations used in ELK (including concurrency), and investigate extensions of the procedure with other constructors, such as number restrictions. We conjecture that it is easier to support new features using non-deterministic rules rather than resolution.
2http://www.ihtsdo.org/snomed-ct/