Description Logics (DLs) are a family of knowledge representation formalisms used to represent and reason about an application's domain elements. They are applicable in the semantic web as they provide the basis for the Web Ontology Language (OWL). Decision procedures for expressive DLs enabling both nominals and QCRs were published in [10] with very weak optimizations if any (no DL reasoner was able to classify the WINE3 ontology until recent e orts [15]). Nominals are challenging in reasoning because in order to preserve their semantics, each nominal must be interpreted as exactly one individual, whereas a concept is interpreted as a set of individuals. Another challenge is that ontologies that use nominals no longer enjoy the quasi-tree model property which has always been advantageous for tableau. Major ine ciency sources can be due to (i) the high degree of non-determinism introduced by the use of GCIs or when merging domain elements is necessary, (ii) the construction of large models, or (iii) the interaction between constructors. The worst case occurs when nominals interact with inverse roles (I) and QCRs. Each of these constructs alone is challenging to reason with and needs special optimization techniques. Resolution-based reasoning procedures were proposed in [18] without being well suited in dealing with large numbers in QCRs. Hypertableaux [13] were recently studied to minimize non-determinism in DL reasoning with no special treatment for QCRs. Combining tableau and algebraic reasoning dramatically improved performance with QCRs [5]. In this paper, we extend our previous work in [3] to additionally allow nominals and unfoldable TBoxes. With nominals, the handling of numerical restrictions becomes more challenging since numerical restrictions imposed by nominals interact with restrictions specified with QCRs. The algorithm is based on the assumption that domain elements consists of a set of individuals divided into subsets depending on their role filler membership and/or concept membership. Also nominals can be seen as singleton sets and the at-least and at-most restrictions expressed in QCRs represent cardinality restrictions on the corresponding sets of role fillers. These restrictions on sets are encoded as linear inequations solved by a linear programming (LP) algorithm (such as simplex) with the objective of minimizing the sum of all cardinalities. If no solution for the inequations is possible, this means that the individuals cannot be distributed between sets without violating the cardinality restrictions. When a solution is returned, a 3 http://www.w3.org/TR/2004/REC-owl-guide-20040210/wine.rdf
minimum number of individuals is distributed among sets without violating any at-least or at-most restrictions. We also introduce proxy individuals as representative of domain elements with common restrictions thus reducing the size of a completion graph model. 2
T = fA v
T = fA v 1R:B; B1 v 8R:C; B2 v 8R::Cg 1R:B; B1 v 8R:C; B2 v 8R::C; o v 1S 1:(A u B1) u 1S 2:(A u B2)g T = fo v 1S 1:( 1R:B u 8R:C) u
1S 2:( 1R:B u 8R::C)g
CT = (:ot 1S 1:( 1R:B u 8R:C) u 1S 2:( 1R:B u 8R::C)) (5) In the following, we assume all concepts to be in their negation normal form (NNF). We use :˙C to denote the NNF of :C and nnf (C) to denote the NNF of C. The concept axioms in T can be reduced to a single axiom > v CT such that CT abbreviates
CvD2T nnf (:C t D) [
Adult v
306 hasBone:Bone 3
Nominals carry implicit numerical restrictions; they not only name individuals but also allow us to count them. This additional information carried with nominals interacts with concepts and roles in a way that can limit the number of individual (i) members of a certain concept C, or (ii) fillers for a certain role R. Given an individual s, instance of a concept E (s 2 EI), C 2 NC, R 2 NR, o1; : : : ; on 2 No, and n; m non-negative integers, we distinguish between and define global and local numerical restrictions.
E 2 T ) enforces a numerical restriction on the cardinality of the set of instances of
E; there can be at-most (at-least) n instances of E corresponding to the interpretation
of o1I [ : : : [ onI assuming o1; : : : ; on are mutually disjoint. Such at-most (at-least)
restrictions carried with nominals are global since they can a ect the set of all
individuals in the domain of interpretation ( I). Nominals can specify concept cardinalities
[
BloodT ype
o+ t A+ t B+ t AB+ t o t A t B t AB
Definition 2 (Local Restriction). QCRs carry explicit numerical restrictions; when E
is of the form ( nR:C), or ( mR:C) it holds a restriction on the cardinality of the set of
R-fillers of s. These restrictions are local to FIL(R; s). For example, having s 2 (Adult)I
with Adult defined in (7) imposes that at least 306 individuals s1, s2, . . . , s306 must be
hasBone-fillers of s, and therefore #FIL(R; s) 306.
(1)
(2)
(3)
(4)
(6)
The interaction between global and local restrictions makes the problem of reasoning
with nominals twofold. First, nominals break the advantageous tree model property of
TBoxes and tableau algorithms can no longer decide a TBox consistency test by
constructing a tree-like model. Second, the nominals semantics impose global restrictions
which means that arithmetic solutions used to satisfy a local restriction as in [
In [
For R; S in NR and CT ; D ALCOQ concepts, we define a new concept operator 8(RnS ):D,
and a role implication operator, R v S , needed to rewrite CT before applying the
calculus. These operators are based on set semantics such that given an interpretation I, then
(8 (RnS ):D)I = fs 2 I j hs; ti 2 RI ^ hs; ti < S I ) t 2 DIg is satisfied, and (RI S I)
is satisfied for each role implication R v S 2 R, with R a set of role implications and
can be seen as a weak form of a role hierarchy H [
Algorithm 1 Given A 2 NC, C , D ALCOQ concepts, R 2 NR and R the set of role implications, the following rewriting holds: rw(A; NR; R) ! A rw(:A; NR; R) ! :A rw((C u D); NR; R) ! (rw(C; NR; R) u rw(D; NR; R)) rw((C t D); NR; R) ! (rw(C; NR; R) t rw(D; NR; R)) rw((:C); NR; R) ! rw(:˙ C; NR; R) rw(8R:C; NR; R) ! 8R.rw(C,NR, R) rw(( nR:C); NR; R) ! ( nR0 u 8R0:rw(C; NR [ fR0g; R [ fR0 v Rg)) rw(( nR:C); NR; R) ! ( nR0 u 8R0:rw(C; NR [ fR0g; R)u
8 (RnR0).rw( :˙C,NR [ fR0g, R [ fR0 v Rg))
Given CT , a set NR of role names, and an empty set R of role implications, we
re-write CT using Algorithm 1 and Lemma 1 holds (see [
Please note that each rewriting step for a number restriction introduces a fresh role name R0 new in T and R. Thus, NR and R are extended. For example, rewriting CT in (5) gives CT = :uo t1S(21 1uS811Su21:8(S111:R( 2 u1R81Ru2:B8Ru1:8BRu::8CR)):C) ! with NR, R extended such that NR = fR; R1; R2; S 1; S 11; S 2; S 21g; R = fR1 v R; R2 v R; S 11 v S 1; S 21 v S 2g. 4.2
The atomic decomposition technique [
The Atomic Decomposition For each role R 2 NR that is used in a number restriction or a QCR, a fresh sub-role R0 introduced by the preprocessing enables a simple role hierarchy; R0 can have only one super role R. Let H(R) denote the set of role names for all sub-roles of R: H(R) = fR0 j (R0 v R) 2 Rg. We do not need to add R to H(R) since it is always implied and does not occur in number restrictions anymore after preprocessing. For every role R0 2 H(R), the set of R0-fillers forms a subset of the set of R-fillers (FIL(R0) FIL(R)). We define R0 to be the complement of R0 w.r.t. H(R), the set of R0-fillers is then defined as R0-fillers =(FIL(R) n FIL(R0)).
Each subset P of H(R) (P H(R)) defines a unique set of role names that admits
an interpretation PI corresponding to the unique intersection of role fillers for the role
names in P: PI = TR02P FIL(R0) \ TR002(H(R)nP) FIL(R00). PI cannot overlap with role
fillers for role names that do not appear in P since it is assumed to overlap with their
complement. This makes all PI disjoint. For example, if P1 = fR1; R2g, P2 = fR2; R3g
and H(R) = fR1; R2; R3g this means that P1 is the partition name for FIL(R1) \ FIL(R2) \
FIL(R3) which is equal to P1I and P2 is the partition name for FIL(R2) \ FIL(R3) \
FIL(R1), and therefore, although P1 \ P2 = fR2g we have P1I \ P2I = ; (see [
Each nominal o 2 No, oI can interact with R-fillers for some R in NR and become a subset of the set of R-fillers (oI FIL(R) if having for example 1R:C u 8R:o) . In order to handle such interactions we define the decomposition set DS of all possible role names and nominals as: DS = SR2NR H(R) [ No. Let P be the set of partition names defined for the decomposition of DS: P = fP j P DSg. For P DS, PI = SR2P FIL(R) \ fd 2 I j d 2 oI; o 2 P \ Nog \ fd 2 I j d 2 :oI; o 2 No n Pg. Then PI = I because it includes all possible domain elements which correspond to a nominal and/or a role filler; PI = SP DS PI.
Mapping Cardinalities to Variables We assign a variable name v for each partition name P such that v can be mapped to a non-negative integer value n using : V ! N such that (v) denotes the cardinality of PI. Let V be the set of all variable names and : V ! P be a one-to-one mapping between each partition name P 2 P and a variable v 2 V such that (v) = P, and if a non-negative integer n is assigned to v using then (v) = n = #PI. Let VS denote the set of variable names mapped to partitions for a role (S 2 NR) or a nominal (S 2 No) then VS is defined as VS = fv 2 V j S 2 (v)g. Using Inequation Solving Given a partitioning P for all roles in NR and nominals in No and a mapping of variables, we can reduce a conjunction of ( nR) and ( mR) to a set of inequations and reason about the numerical restrictions using an inequation solver based on the following principles.
partitions in P are mutually disjoint and the cardinality function is additive, a lower (upper) bound n (m) on the cardinality of the set of role fillers FIL(S) for some role S 2 H(R) can be reduced to an inequation of the form Pv2VS (v) n (Pv2VS (v) m). Thus, we can easily convert an expression of the form ( nS ) or ( mS ) into an inequation using such that (S ; ; n) = Pv2VS (v) n, and (S ; ; m) = Pv2VS (v) m. The cardinality of a partition with a nominal can only be 1 based on the nominals semantics which is encoded into inequations using (o; ; 1) and (o; ; 1) for each nominal o 2 No. In this way we make sure that the nominal semantics is preserved; there is one individual for each o 2 No: #oI = 1.
P2: Getting a Solution. Given a set a of inequations, an integer solution defines the mapping for each variable v occurring in a to a non-negative integer n denoting the cardinality of the corresponding partition. For example, assuming (v) = 4 and (v) = fR0; R00g, this means that the corresponding partition ( (v))I must have 4 fillers; #(FIL(R0) \ FIL(R00)) = 4. Additionally, by setting the objective function to minimize the sum of all variables a minimum number of role fillers is ensured at each level. then defines a distribution of individuals that is consistent with the numerical restrictions encoded in a and the hierarchy expressed in R. 4.3
In general the satisfiability of numerical restrictions does not decide TBox consistency since logical restrictions expressed using logical operators (u; t; :; v) and using 8 operators need also be satisfied. Numerical and logical restrictions share expressions and their satisfiability cannot be tested independently to decide a TBox consistency. For this purpose we propose a hybrid algorithm; we define a tableau for ALCOQ TBox consistency and describe the algorithm in the next section. Our tableau is di erent from other tableaux for ALCOQ by the way it ensures the semantics of the QCRs operator and the new operator (8(RnS )) introduced after preprocessing an unfoldable ALCOQ TBox. We also define clos(C) to be the smallest set of concepts such that: (a) C 2 clos(C), (b) if D 2 clos(C) then :˙D 2 clos(C), (c) if (E u D) or (E t D) 2 clos(C) then E; D 2 clos(C), (d) if (8R:D) or (8RnS :D) 2 clos(C) then D 2 clos(C). The set of relevant sub-concepts of a TBox T is then defined as clos(T ) = clos(rw(CT ,NR; R)).
Definition 3. [Tableau] Given an unfolded ALCOQ TBox T rewritten by applying
Algorithm 1, we define a tableau T = (S; L; E) as an abstraction of a model for T with
S a non-empty set of individuals, L : S ! 2clos(T ) a mapping between each individual
and a set of concepts, and E: NR ! 2S S a mapping between each role and a set of pairs
of individuals in S. For all s; t 2 S, A 2 NC, C,D 2 clos(T ), o 2 No, R, S 2 NR, and
given the definition RT (s) = ft 2 S j hs; ti 2 E(R)g, properties 1 - 10 must always hold:
1. CT 2 L(s)
Lemma 2. An ALCOQ TBox T is consistent i there exists a tableau for T .
Proof. The proof is similar to the one found in [
In this section, we describe a hybrid algorithm which decides the existence of a tableau
for an unfolded ALCOQ TBox T . Our algorithm is hybrid because it relies on tableau
expansion rules working together with an inequation solver, the corresponding model
is represented using a compressed completion graph (CCG). The CCG is di erent from
the “so-called" completion graphs used in standard tableau algorithms for ALCOQ [
Definition 4. [Compressed Completion Graph] A compressed completion graph is a directed graph G = (V; E; L; LE). Each node x 2 V is labeled with two labels: L(x) and LE(x), and each edge hx; yi 2 E is labeled with a set, L(hx; yi) NR, of role names.
L(x) denotes a set of concept expressions and role names such that L(x) clos(T ) [ P. By doing this, we not only label nodes based on the concept descriptions that they satisfy but also based on the partition they belong to. A partition name might include a nominal or a role name. We do not need to distinguish whether a nominal o 2 L(x) is part of a partition name or a concept expression; in both cases x satisfies the nominal o. When a role name R appears in L(x) this means that x belongs to the partition for R-fillers and can therefore be used as an R-filler. This tagging is needed for the re-use of individual nodes.
LE(x) denotes a set x of inequations that must have a non-negative integer solution. The set x is the encoding of ( nR) and ( mR) 2 L(x). In order to make sure that numerical restrictions local for a node x are satisfied while the global restrictions carried with nominals are not violated, LE(x) is propagated from each node to all its successors. This makes sure that nominals are globally preserved while still satisfying the numerical restrictions at each level.
Given T , we unfold T as outlined in Section 2 and build C0 which is rewritten into CT = rw(C0 ; NR; R) and P is the corresponding atomic decomT position. To decide the
T consistency of T we need to test the consistency of CT using i 2 No new in T such that iI 2 CT I and every new individual satisfies CT .
The algorithm starts with the completion graph G = (fr0g, ; , L, LE). With LE(ro) = So2No { (o; ; 1), (o; ; 1)} which is an encoding of the nominal semantics. The node r0 is artificial and is not considered as part of the model, it is only used to process the numerical restrictions on nominals using the inequation solver which returns a distribution for them. The distribution of nominals (solution) is processed by the fil-Rule (see Fig. 1) which non-deterministically initializes the individual nodes for nominals. After at least one nominal is created, G is expanded by applying the expansion rules given in Fig. 1 until no more rules are applicable or when a clash occurs. No clash triggers or rules other then the fil-Rule apply to ro.
Definition 5. [Clash] A node x in (V n fr0g) is said to contain a clash if: – (i) fC; :Cg L(x), or – (ii) a subset of inequations x LE(x) does not admit a non-negative integer solution, this case is decided by the inequation solver, or – (iii) for some o 2 No, #fx 2 (V n fr0g)j o 2 L(x)g > 1.
Definition 6. [Proxy node] A proxy node is a representative for the elements of each
partition. Proxy nodes can be used since partitions are disjoint and all elements in a
partition share similar restrictions (see Lemma 4 in [
When no rules are applicable or there is a clash, a completion graph is said to be complete. When G is complete and there is no clash, this means that the numerical as well as the logical restrictions are satisfied (CT I , ;) and there exists a model for T : the algorithm returns that T is consistent and inconsistent otherwise. 5.1
Given a node x in the completion graph, the expansion rules in Figure 1 are triggered when applicable based on the following priorities: – Priority 1: u-Rule, t-Rule, 8-Rule, ch-Rule, -Rule, -Rule, e-Rule. – Priority 2: fil-Rule. – Priority 3: 8n-Rule.
The rules with Priority 1 can be fired in arbitrary order. The fil-Rule has Priority 2
to ensure that all at-least and at-most restrictions for a proxy node x are encoded and
satisfied by the inequation solver before creating any new proxy nodes. This justifies
why role fillers or nominals are never merged nor removed from the graph; a distribution
of role fillers and nominals either survives into a complete model or fails due to a clash.
Also, assigning the fil-Rule Priority 2 helps in early clash detection in the case when the
inequation solver detects a numerical clash even before new nodes are created. The
8nRule has Priority 3. By giving this priority we ensure that the semantics of the 8(RnS )
operator are not violated. We allow the creation of all possible edges between a node
and its successors before applying the 8(RnS ) operator semantics. This rule priority is
needed to ensure the completeness of the algorithm (See Section 5.3 for proofs).
The u-Rule, t-Rule and the 8-Rule rules are similar to the ones in the standard tableau
rules for ALC [
8n-Rule. This rule is used to ensure the semantics of the new operator 8(RnS ):D
(defined in preprocessing) by making sure that all R-fillers are labelled, and together
with the ch-Rule (see explanation below) it has the same e ect as the choose-rule in [
-Rule and -Rule. These rules encode the numerical restrictions in the label L of a node x into a set ( x) of inequations maintained in LE(x) (P1 in Section 4.2). An inequation solver is always active and is responsible for finding a non-negative integer solution for x (P2 in Section 4.2) or triggering a clash if no solution is possible (see Def. 5). If the inequations added by these rules do not trigger a clash, then the encoded number restrictions can be satisfied by a possible distribution of role fillers.
ch-Rule. This rule is used to check for empty partitions. Given a set of inequations
in the label (LE) of a node x and a variable v such that (v) = P and P 2 P we
distinguish between two cases:
– (i) The case when PI must be empty (v 0; (v) = P); this can happen when
restrictions of elements assigned to this partition trigger a clash. For instance, if
{8R1:A, 8R2::Ag L(x), v 1 2 LE(x) and P = fR1; R2g then a node y assigned to
P with fR1; R2g L(hx; yi) triggers a clash fA; :Ag L(y) and v 0 is enforced.
– (ii) The case when PI must have at least one element (1 m (v)); if PI can
have at least one element without causing any logical clash, this means that we can
have m elements also in PI without a clash. Therefore, when creating nodes (using
the fil-Rule) of corresponding partitions, it is su cient to create one proxy node for
each partition (see Lemma 4 in [
Since the inequation solver is unaware of logical restrictions of filler domains we allow an explicit distinction between cases (i) and (ii). We do this by non-deterministically assigning 0 or 1 for each variable v occurring in LE(x).
fil-Rule. This rule is used to generate individual nodes depending on the distribution ( ) returned by the inequation solver. The rule is fired for every non-empty partition P using (v). It generates one proxy node as the representative for the m elements assigned to PI by the inequation solver. The proxy individual is tagged with its partition name using (v) in its label, CT is also added to its label to make sure that every node created by the fil-Rule also satisfies CT .
e-Rule. This rule connects a node x to a proxy individual y representing R-fillers of x by adding the edge for R between x and y. For instance, if ( 2R) 2 L(x) and there exists a node y assigned to PI such that R 2 P and P L(y), this means that y can be used as an R-filler of x. Therefore, the e-Rule creates/updates the edge hx; yi with R 2 L(hx; yi). The node y can be re-used to satisfy another ( nR. For instance, if we have another node x1 with ( 2R) 2 L(x1), y is re-used and R is added to the edge hx1; yi. 5.3
The soundness, completeness and termination of the algorithm presented in this paper are consequences of Lemmas 2, 3, 4, 5, and Lemma 6.
Lemma 3. Given an unfoldable TBox T and its complete and clash-free completion graph G. Let x be a node in G, C; D 2 NC; R 2 NR, we define Num(x) = fE2 L(x) j E is of the form nR; mRg as the set of at-least and at-most restrictions to be satisfied for x. A solution for the encoding x of Num(x) is valid w.r.t T : (i) it does not violate Num(y) for a node y in G, (ii) it does not violate a restriction implied by any operator used in T , (iii) it does not violate the hierarchy R introduced during preprocessing. Lemma 4 (Termination). When started with an unfoldable TBox T using the DL ALCOQ, the proposed algorithm terminates.
Lemma 5 (Soundness). If the expansion rules can be applied to T such that they yield a complete and clash-free completion graph, then T has a tableau.
Lemma 6 (Completeness). If T has a tableau, then the expansion rules can be applied
to T such that they yield a complete and clash-free completion graph.
Proof. The proofs for Lemmas 3, 4, 5, and Lemma 6 can be found in [
The work presented in this paper not only extends our work in [
The key intuition in our approach is to apply the atomic decomposition technique on the set of all nominals and all role fillers. By doing this, the decomposition reaches all domain elements and computes all possible groupings of these elements into mutually disjoint partitions. In a sense it performs a semantic split for groups of individuals and not necessarily for each individual (which is the case with standard tableau algorithms) using the ch-Rule rule.
Unfortunately the number of partitions is exponential to the size of the input
(number of nominals and QCRs) which results in an exponential blow up of variables. Naïve
applications of the ch-Rule give a double exponential worst case algorithm. However,
many of these partitions will not be assigned any individuals. For instance, in most of
the cases the partitions including more then one nominal will be empty assuming that
nominals are disjoint. As a default, one can assume that all partitions are empty and use
only those needed to satisfy the QCRs. In a sense, the inequation solver only allocates
and deals with non-zero variables and the variables not considered are assumed to be
zero. Which means that in the average case the algorithm does not have to deal with
inequations containing an exponential number of variables (see [
It has been shown in [