ion provides an easier to grasp algorithm with less intermediary transformation steps and increased efficiency. We give a proof of the completeness of our algorithm that relies solely on the SHIQ tableau method, without requiring any further background knowledge. Besides pure terminology reasoning, the DL calculus can be extended to ABox reasoning, providing the basis for an efficient two-phase data reasoning framework. Here, the DL calculus is used in the first phase to simplify the content of the TBox by (1) performing those reasoning steps that can be done independently of the ABox and (2) eliminating the axioms that cannot participate in the ABox reasoning. The content of the ABox is only accessed in the second phase when the simplified TBox allows for answering instance retrieval queries in a focused, efficient way. The above mentioned techniques are implemented in the SHIQ ABox reasoner called DLog, available to download from SourceForge.
The Tableau Method [
Other approaches use first-order resolution for reasoning. A resolution-based
inference algorithm is described in [
Reading the whole ABox is not a feasible option in case the ABox is bigger than the available memory or the content of the ABox changes so frequently that on-the-fly ABox access is an utmost necessity. Typical such scenarios include reasoning on web-scale or using description logic ontologies directly on top of existing information sources, such as in a DL based information integration system.
We have developed a DL ABox reasoner called DLog [
Our current work with the DL calculus aims to improve on the calculus
presented in [
This paper is structured as follows. In Section 2 we present the DL calculus that performs consistency check for a SHIQ TBox, and show that it can also be used to decide concept satisfiability. In Section 3 we prove that the calculus is complete. Section 4 extends the DL calculus to ABox reasoning. Finally, Section 5 concludes by giving a brief summary of our results. 2
In this section we present a reasoning algorithm called DL calculus which decides the consistency of a SHIQ TBox. Before doing so, however, we show that such an algorithm can be used for deciding concept satisfiability as well.
Suppose we want to know whether concept C is satisfiable in the presence of TBox T . Let R be a role that appears neither in T nor in C. Let us consider a new TBox T 0 = T ∪ {> v ∃R.C}. Given that R is a new role name, it is easy to see that the newly added axiom will only introduce inconsistency to the TBox if C is unsatisfiable. C is satisfiable in the presence of TBox T if and only if T 0 is consistent. Hence, by giving an algorithm for TBox consistency check, we also provide an algorithm for concept satisfiability check.
The algorithm can be summarized as follows. We determine a set of concepts
that have to be satisfied by each individual of an interpretation in order for the
TBox to be true. Next, we introduce inference rules that derive a new concept
from one or two concepts. Using the inference rules, we saturate the knowledge
base, i.e., we apply the rules as long as possible and add the consequent to
the knowledge base. We also apply redundancy elimination: whenever a concept
extends another, it can be safely eliminated from the knowledge base [
To illustrate our calculus, we show how to derive the empty concept from an inconsistent SHIQ TBox T . Suppose that T forces the following concepts to be true on all individuals (i.e. T contains the axioms > v Ci, 1 ≤ i ≤ 6): C1 : C2 : C3 : C4 : C5 : C6 : ∃hasChild .Clever ∃hasChild −.Rich ≤ 1hasChild .Tall ≤ 1hasChild .Fat
The derivation proceeds through the following steps. To anticipate the DL calculus, we give the corresponding inference rules, together with the premise concepts (for compactness we abbreviate hasChild with hc):
C13 : ⊥ (Rule4: C1,C3) (Rule2: C7,C5) (Rule4: C8,C4)
(Rule6: C9) (Rule5: C10,C2) (Rule2: C11,C6) (C12) If someone has a clever child and has at most one tall child, then either he does not have any tall and not clever children, or else he also has a clever and not tall child (C1 + C3 → C7). If he has a clever and not tall child, then this child is clever and fat (C7 + C5 → C8). Given that nobody can have more than one fat child, the person having a clever and fat child can have no fat and not clever children (C8 + C4 → C9). We obtain that for any individual, either he does not have any tall and not clever children, or he does not have any fat and not clever children. In particular, this entails that he cannot have any tall and fat and not clever children (C9 → C10). We know that every individual has a rich parent and it is true for the parent that he cannot have a child that is tall and fat and not clever, so the individual itself cannot be tall and fat and not clever, so he is either not tall or not fat or clever (C10 + C2 → C11). Hence, nobody can have a child that is tall and fat and not clever (C11 + C6 → C12), so we obtained a contradiction (C12 → C13). 2.2
We first eliminate transitivity from the knowledge base as described in [
L1 t L2 t · · · t Li L1 t (≥ kR.L2)
L1 t (≤ nR.L2) A derivation in the DL calculus generates concepts that are slightly more general. We call this broader set SHIQ-concepts, defined as follows (C, D, E stand for concepts containing no role expressions):
C C t G(
≤ nR.D) C t (≥ kS.E) t G( ≤ nR.D) 2.3
Before presenting the inference rules, we define some important notions. A literal concept is a possibly negated atomic concept. A bool concept contains no role expressions (only negation, union and intersection are allowed). In the following, we will always assume that a bool concept is presented in a simplest disjunctive normal form, i.e., it is the disjunction of conjunctions of literal concepts. So for example, instead of A t A t (B u ¬B u C) we write A, and A u ¬A is replaced with ⊥. We also impose a partial ordering ( ) on DL concept expressions, as follows: Definition 1 (concept ordering). 1. A ≥-concept is greater than any ≤-concept or any bool concept. 2. A ≤-concept is greater than any bool concept. 3. C1 = (≤ n1R1.A1) is greater than C2 = (≤ n2R2.A2) if and only if: – R1 R2 or – R1 = R2 and n1 > n2 or – R1 = R2, n1 = n2 and A1 A2 4. For atomic roles, R S if R is lexicographically greater than S. 5. For atomic concepts, A B if A is lexicographically greater than B. 6. ¬A A 7. ¬A B if A B 8. A ¬B if A B 9. F Ai F Bi if ∃i(∀j(Ai 6= Bj ∧ (Bj Ai → ∃l(Al = Bj )))) 10. d Ai d Bi if ∃i(∀j(Ai 6= Bj ∧ (Bj Ai → ∃l(Al = Bj )))) In the above we allow F Ai (d Ai) to be singular, i.e., it can stand for a nondisjunctive (non-conjunctive) concept.
Definition 2 (maximal concept). In a set N of concepts, concept C ∈ N is maximal if it is greater than any other concept in N .
The -ordering given in Definition 1 is not total. However, any two disjuncts of a SHIQ-concept (cf. Section 2.2) are comparable, hence, for any disjunctive SHIQ-concept we can talk about the maximal disjunct. 2.4
The inference rules are presented in Figure 1, where Li stand for literal concepts, C, D, E are bool concepts and W is a SHIQ-concept without ≥-concept. The rules manipulate on one disjunct of each premise and we make the further restriction that the involved disjunct must be maximal. Some of the rules do not preserve the DNF form of bool concepts. In such cases, an additional step is required to transform the bool concepts appearing in the consequent into DNF form. For the sake of simplicity, these additional steps are omitted from Figure 1.
It is straightforward to show that the inference rules are sound, i.e., that any interpretation satisfying the premises will necessarily satisfy the conclusion as well. We leave this to the reader. 2.5
We saturate the knowledge base, i.e., we apply the rules in Figure 1 to deduce new concepts as long as possible. We claim that saturation terminates. For any TBox with finite signature, there can only be finitely many distinct role expressions and bool concepts. Furthermore, note that each inference rule either leaves the arity of a number restriction unaltered or reduces it. So in a (≤ nR.C) or (≥ nR.C) expression the number of possible values for n, R and C is bound for a fixed TBox. As all SHIQ-concepts are disjunctions of bool, ≤, and ≥-concepts, we have an upper limit for the set of deducible SHIQ-concepts: generating every possible SHIQ-concept still requires only finitely many steps. Rule2 Rule3 Rule4 Rule5 Rule6
D t (LD1 u LD2 · · · u ¬L)
C t D C t (LC1 u LC2 · · · u L) W t (≥ nR.C) D W t (≥ nR.(C u E)) where E is obtained by resolving C and D using Rule1 W1 t (≤ nR.C) W2 t (≥ kS.D) W1 t W2 t (≥ (k − n)S.(D u ¬C)) n < k, S v∗ R
W1 t (≤ nR.C) W2 t (≥ kS.D) W1 t W2 t (≤ (n − k)R.(C u ¬D)) t (≥ 1S.(D u ¬C) n ≥ k, S v∗ R D t (≤ 0R.C) W t (≥ kS.E)
W t ¬C t (≥ kS.(E u D)) where inv(S) v∗ R and D is a bool concept W t (≤ 0R.C) t (≤ 0R.D)
W t (≤ 0R.(C u D))
In this section we prove that the method presented in Section 2 is complete, i.e., whenever there is some inconsistency in a TBox T , the empty concept is deduced. We prove completeness by showing that if a saturated set SatT does not contain ⊥ then the axiom > v d SatT has a model. Instead of building the model itself, we will prove that the SHIQ tableau method can find one such model; in the course of the tableau method the concepts of SatT are added to the label of every newly created node. 3.1
We require the following ordering on the tableau rules: t-rule, u-rule, ∃-rule, ≥-rule, ∀-rule, ./ -rule and ≤-rule. When applying the t-rule we proceed with the branch3 that adds the minimal possible concept to the label of a node.
The concepts of SatT give rise to the appearance of literal concepts in labels of nodes. Depending on what type of SHIQ-concept was involved, we say that a literal concept was derived from a bool concept, a ≤-concept or a ≥-concept.
Whenever a node n contains a disjunctive concept W t C, the branch where C is added to the label of n is only examined after each disjunct in W that is smaller than C has been proved unsatisfiable. A clash occurs in the tableau tree 3 Throughout this paper, “branch” refers to a branch of the meta-tableau tree, i.e., one of the tableaux resulting from the application of a non-deterministic rule. when an atomic concept name and its negation both appear in the label of some node. In this case we roll back and proceed with another branch. A final clash occurs when there are no branches left, i.e., the tableau proves the inconsistency of SatT . We show that no final clash can be reached if SatT does not contain ⊥.
Let us assume that the tableau method reaches a final clash. Literal concepts X and ¬X appear in the label of a node and there are no other branches to be examined. We examine in turn the different concepts from which the clash could have been derived and show contradiction. 3.2
Suppose that X and ¬X were derived from bool concepts, i.e., SatT contains concepts
WC = C1 t (C2 u X)
WD = D1 t (D2 u ¬X) Since there are no more branches, (C2 u X) and (D2 u ¬X) are maximal in WC and WD, respectively, and each disjunct in C1 and D1 leads to a clash. WC and WD are resolvable using Rule1, so SatT contains
W = C1 t D1 W cannot be empty because we assumed that SatT does not contain ⊥. Should W contain X or ¬X, we can resolve it with either WC or WD resulting in a concept W2 that makes W redundant. This follows from conditions 6-10 of Definition 1 and the fact that X and ¬X are maximal in WC and WD. After possibly several such inference steps we obtain a concept Wi that contains neither X nor ¬X. Let us assume that W = Wi, i.e., we derived from WC and WD a concept W that does not contain X or ¬X. Both X and ¬X are greater than any disjunct in W . This means that before introducing X we have already examined all branches corresponding to W . We assumed that each of these branches leads to a clash, hence a final clash was reached before X appeared in the label. This is a contradiction.
The Application of the ≥-rule Let us now assume that one of the contradicting concepts, say X was derived from a ≥-concept and ¬X from a bool concept. SatT contains concepts WC = C1 t (≥ nR.(C2 t (C3 u X))) WD = D1 t (D2 u ¬X) Since there are no more branches, (≥ nR.(C2 t (C3 u X))) and (D2 u ¬X) are maximal in WC and WD, respectively, (C3 u X) is maximal in (C2 t (C3 u X)) and each disjunct in C1, C2 and D1 leads to a clash. WC and WD are resolvable in the calculus using Rule2, so SatT contains
W = C1 t (≥ nR.(C2 t (D1 u C3 u X))) W makes WC redundant, so the only way the latter can be present in SatT is that WC = W , i.e., D1 is one of the conjuncts of C3. We know that C1, C2 and D1 all lead to clash, so we obtain a final clash on WC = W without WD, contradicting our assumption. 3.4
The Application of the ∀-rule We now examine the case when one of the concepts participating in the final clash is derived from a (≤)-concept with zero arity, i.e., a ∀-concept. The ∀-rule adds a concept to the label of either a successor or the predecessor.
In the first case some successors have been created, so the node containing the ∀-concept also contains a ≥-concept, i.e., SatT contains concepts WC = C1 t (≥ nS.C)
WD = D1 t (≤ 0R.D) where S v∗ R. As previously, we assume that (≥ nS.C) is maximal in WC , (≤ 0R.D) is maximal in WD and each disjunct in C1 and D1 leads to clash. WC and WD can be resolved using Rule3, resulting in
W = C1 t D1 t (≥ nS.(C u ¬D)) By the time the ≥-concept from WC and the ≤-concept from WD appear in the label of a node, the ≥-concept from W also appears in the label. Hence, we create another set of n S-successors (the ≥-rule is applied prior to the ∀-rule), with label (C u ¬D). Should this be inconsistent, we obtain a clash before the ∀-rule. Consequently, adding ¬D to the first set of n S-successors of the node will not introduce any clash that would not have occurred otherwise.
In the second case the ∀-rule fires upwards and a bool concept is added to the predecessor. This happens when a node contains concept (≥ nS.D) and one of the thus created successors contains a concept (≤ 0R.C) where inv(S) v∗ R. That is, SatT contains the following concepts:
WC = C1 t (≥ nS.C)
WD = D1 t (≤ 0R.D) (≥ nR.C) is maximal in WC , (≤ 0S.D) is maximal in WD, each disjunct in C1 leads to clash in the parent and each disjunct in D1 leads to clash in the successor. Either D1 does not contain any ≤-concepts, or Rule6 is applicable to it yielding to a concept WD0 = D10 t (≤ 0R.D0), where D10 does not contain any ≤-concepts. In the latter case, let WD = WD0 . WC and WD can be resolved by Rule7, resulting in
W = C1 t ¬D t (≥ nS.(C u D1)) By the time the ∀-rule in the successor fires, the t-rule has already been applied on the parent, so one of the disjuncts of W appears in the label of the latter. It cannot be a disjunct of C1 because they all lead to clash. If it is a disjunct of ¬D then the ∀-rule in the successor does not fire. Finally, if the parent contains the concept (≥ nS.(C u D1)), that must have lead to a final clash because we know that D1 together with C leads to clash in a successor. In conclusion, by the time the ∀-rule would be applicable, it either does nothing or we have already obtained a final clash. It remains to be seen if we might obtain a final clash through a ≤-rule, i.e., the identification of some nodes. Note that by the time a ≤-rule is applied, we have already performed all possible ./ -rules. We will show that in case of an identification that could potentially lead to a final clash, the identification is not only possible, but it can be performed simply by eliminating some successors, without having to add any concepts to the label of the remaining nodes4.
Let some node contain concepts (≤ nR.D) and (≥ niSi.Ai), where 1 ≤ i ≤ l and Si v∗ R. Suppose that Σil=1ni > n, so we need to perform identification and failing to do so would lead to a final clash. This can only happen when SatT contains concepts
W = E t (≤ nR.D)
Wi = Fi t (≥ niSi.Ai) 1 ≤ i ≤ l where (≤ nR.D) is maximal in W , (≥ niSi.Ai) is maximal in Wi, each disjunct in E and Fi leads to clash and D can be deduced from each Ai (using the bool concepts in SatT ). We will also consider the case when the node has an Rpredecessor, i.e., when it is the S0-successor of some node and inv(S0) v∗ R. By using induction on n, i.e., the arity of the ≤ concept, we show that identification is possible by simply deleting some nodes in the tableau.
The base case, when n = 0 has already been partly discussed in the section of the ∀-rule. We have seen that whenever the ∀-rule would have to put a concept C in the label of some successors, there are other successors having the same label plus C. This means that we can simply delete the successors whose label do not contain C. We also need to examine what happens when we have an R-predecessor. Then, the node was created due to a (≥ kS0.X) concept in the parent, where inv(S0) v∗ R. So, SatT contains concepts
W = E t (≤ 0R.D)
V = G t (≥ kS0.X) where E is false in the examined node and G is false in the parent. The above two concepts can be resolved using Rule5, resulting in
G t ¬D t (≥ kS0.(X u E)) One disjunct of this concept is satisfied by the parent and it cannot be G. If the parent satisfies ¬D then it is not affected by the (≤ 0R.D) concept. If the concept (≥ kS0.(X u E)) appears in its label, there will be successor nodes with label X u E. The examined node was created with concept X and we know that the branch where E was added to the label failed, so X u E is not satisfiable. So, should the label of the parent really contain (≥ kS0.(X u E)), we would have obtained a clash even before applying the ≤-rule, contrary to our assumption.
For the inductive step, assume that any ≤-concept with arity smaller than n can be satisfied by deleting some nodes. Concepts W and W1 in SatT are 4 We might, however, have to extend the label of an edge due to identification, but this cannot lead to clash. resolvable using Rule4, resulting in
E t F1 t (≤ (n − n1)R.(D u ¬A1)) t (≥ 1S1.(A1 u ¬D)) D is deducible from A1 using bool concepts of SatT , so the calculus also deduces E t F1 t (≤ (n − n1)R.(D u ¬A1)) (1) Due to the ./ -rule, the label of every successor contains either A1 or ¬A1. n−n1 < n, so the inductive hypothesis applies to (1), i.e., all the successors whose label contains both D and ¬A1 can be identified into n − n1 nodes without altering the labels of the remaining nodes. Further to this, there are n1 successors created with the ≥-concept in W1 – we say that A1 is the creator concept of these nodes, – plus some k other successors such that the ./ -rule put A1 into their labels. 1. If k ≤ n1 then we can eliminate n1 − k nodes from those having A1 as their creator concept, leaving exactly n1 successors whose label contains A1. 2. If k > n1 then each of the nodes whose creator concept is A1 can be eliminated since there are more then n1 other nodes satisfying A1. In case we still have too many successors left, we repeat the above argument on the successors originating from concepts W2, W3, . . . Wl. Again, either we find that eliminating some of the successors with creator concept Ai gives a good identification, or we can eliminate all the successors with creator concept Ai. In the latter case we proceed with Ai+1 etc. until at most n successors remain.
In case ni > n then Rule3 is applied instead of Rule4 when resolving W and Wi, resulting in:
E t Fi t (≥ (ni − n)Si.(Ai u ¬D)) Since D is deducible from Ai, the calculus deduces E t Fi. We know that all disjuncts in E and Fi are false, so we obtained a final clash even before introducing the ≤- and ≥-concepts, contradicting our assumption. 4
In this section we sketch an extension to the DL calculus that performs ABox
reasoning. Although the answers that we obtained in our test queries are identical
to those of other reasoners, we do not yet have a formal proof of completeness.
Accordingly, this section should be seen as an indication of our future work.
Currently, the DLog data reasoner uses the calculus described in [
We restrict our attention to extensionally reduced ABoxes, i.e., we assume that the concept assertions only contain literal concepts. An arbitrary knowledge base can be easily transformed to satisfy this constraint. Furthermore, we use the Unique Name Assumption (UNA): we assume that different names refer to different individuals. The rules in Figure 2 are added to the 6 inference rules 7 C t (L1 u L2 · · · u L)
C(a) ¬L(a) 8 C t (L1 u L2 · · · u L(a))
C ¬L(a) 9 W t (≤ nR.C) {R(a, bi)}in=+11
W (a) t Fin=+11 ¬C(bi) 10 W t (≤ nR.C)(a) {R(a, bi)}in=+11
W t Fin=+11 ¬C(bi) presented in Figure 1. As before, the resolved literals have to be maximal in their respective concepts.
An important property of the ABox DL calculus is that the rules for data
axioms do not involve ≥-concepts. This suggests that all inference steps involving
≥-concepts can be performed before accessing the ABox, allowing us to break
the ABox reasoning into two parts: (1) an ABox independent DL calculus is
first applied to the TBox until all the consequences of ≥-concepts are inferred;
(2) next we perform the actual data reasoning using a much simpler TBox (as
all ≥-concepts can be eliminated). The output of the first phase is translated
to first-order clauses during data reasoning and ≥-concepts give rise to skolem
functions. Without ≥-concepts, we can work with function-free clauses, which
makes the reasoning task much easier [
We have presented the DL calculus, a resolution based algorithm for deciding the consistency of a SHIQ TBox. The novelty of this calculus is that it is defined directly on DL axioms. We hope that further research will reveal that the DL calculus provides a reasonable alternative to the Tableau Method for TBox reasoning.
We have extended the DL calculus to consider ABox axioms as well, providing the basis of a two-phase ABox reasoning framework. The DL calculus is used to perform the first phase involving the TBox only. Given that the TBox is relatively permanent over time, the speed of this phase is not crucial as it has to be performed only once. What really matters is that by the end of this phase we can eliminate many axioms that make the knowledge base much simpler. Thanks to the eliminations, we can translate the initial knowledge base into a set of first-order clauses that are function-free. The absence of function symbols enables us to use the query driven, highly efficient data reasoning techniques implemented in the DLog ABox reasoner. It has to be noted, however, that the ABox extension of the DL calculus requires further work.