In this paper, we present a novel consequence-based algorithm to perform subsumption reasoning in SHOQ, which support nominals and Qualified Cardinality Restrictions (QCRs). Our algorithm maps numerical restrictions imposed by QCRs or nominals to inequalities and determines the feasibility of inequality systems by means of Integer Linear Programming.
Most modern DL reasoners, such as HermiT [
There is another type of reasoning algorithms, called consequence based algorithms, which instead of building counter-models (like tableau-based algorithms), directly derive logical consequences of axioms in the ontology using inference rules. These algorithms never check for subsumptions that are not entailed. Typically, the number of entailed subsumptions is much smaller than the number of potential subsumptions between ontology concepts. These algorithms can classify an ontology in a single pass.
Consequence-based (CB) algorithms were first introduced for the DL E L [
However, to the best of our knowledge, none of the existing CB algorithms could handle the combination of QCRs and nominals efficiently. As we discuss in Section 3, it is challenging to extend these algorithms to DLs such as SHOQ that combines different kinds of numerical restrictions: QCRs and nominals.
On the other hand, most existing DL reasoners try to satisfy imposed
numerical constraints by exhausting all possibilities. Merely searching for a model
in such an arithmetically uninformed or blind way is usually very inefficient.
Using arithmetic methods can improve the average case performance of numeric
reasoning. Employing this technique for tableau-based reasoning in SHOQ has
shown to have an impressive practical result [
In Section 3 we extend the framework introduced in [
Description Logics ALCHOQ and SHOQ are defined w.r.t. non-empty and disjoint sets of atomic concepts NC , roles NR and nominals No.
Ontologies are interpreted using Tarski-style semantics. An interpretation I = ( I ; :I ), where I is a non-empty set of elements called the domain, and :I is an interpretation function that maps each atomic concept A 2 NC to a subset of I , and each role R 2 NR to a subset of I I .
A Qualified Cardinality Restriction (QCR), also called qualified number restriction, specifies a lower ( nR:C) or upper ( nR:C) bound on the number of R-successors belonging to a certain concept C, where R 2 NR. A domain element y 2 I is said to be an R-successor if there exists a domain element x 2 I such that x and y are related trough the role R, hx; yi 2 RI . The set of all Rsuccessors for a given role R is defined as Succ(R) = fy 2 I j hx; yi 2 RI g. A qualifying concept A is a concept name that occurs in a QCR of the form nR:A or nR:A to impose a minimum or maximum on the number of R-successors for a role R 2 NR.
Nominals are known as named individuals. They are also considered as concepts with exactly one instance that will be interpreted as singleton sets. Nominals enable DLs with the notion of uniqueness and identity. There exist many concepts in the real world that need to be modeled using nominals such as “Moon”, “Earth” or “Canada”.
A literal L is a concept of the form C, o, 9R:C, 8R:C, nR:C, nR:C, for C 2 NC , o 2 No and R 2 NR. The set of all literals is denoted as NL. Through the rest of this paper we denote a conjunction and disjunction of literals with K and M , respectively. Furthermore, we identify them as a set of literals and use them in standard set operations. The conjunction (disjunction) of literals may be empty, which is abbreviated as > (?). An axiom is an expression of the form C1 v C2 (general concept inclusion (GCI)), R1 v R2 (role inclusion), or T rans(R) (role transitivity axiom ). A SHOQ ontology O is a finite set of axioms.
A clause is a general concept inclusion of the form dim=1 Li v Fin=m+1 Li
where 0 m n and each Li is a literal. A clause is normal if each Li
with 1 i m is an atomic concept and a clause is a query if each Li with
m + 1 i n is an atomic concept. In a clause of the form K v M , the
conjunction K is called the antecedent, and the disjunction M is called the consequence.
An ontology O is normalized if each GCI in O is a normal clause. The ontology
O can be converted to a normalized ontology O0 in linear time such that O0 is
a conservative extension of O. This conversion is known as structural
transformation (see, e.g., [
Due to the presence of nominals, assertions can be transformed to terminological knowledge (TBox axioms). So we only consider terminological reasoning in this research. In SHOQ the interaction of transitive roles with number restrictions would cause undecidability. To avoid this interaction, SHOQ allows number restrictions only with simple roles which are neither transitive nor have transitive sub-roles. 3
A consequence-based calculus for SHOQ In this section, we explain our consequence-based algorithm for classifying a normalized ALCHOQ ontology O having a finite set of queries Q to determine whether O j= q holds for each query q = K v M 2 Q. Since the goal of the algorithm is to obtain the ontology classification, we only consider queries of the form C1 v C2 where C1 and C2 are atomic concepts from O. A formal description of our algorithm is presented in Section 3.2. 3.1
This section demonstrate our algorithm at a high level by applying it to the ontology O and the query q as specified in Example 1 to prove that O j= q. Example 1. Let O be an ontology containing axioms (1) – (9), and q = A v D. One can readily verify that O j= q due to cardinality restrictions imposed on the concepts A; C by merging nominals o1; o2 and o3.
A v 9R:o1 (1) A v 9R:o3 t D (3) o1 v C (5) o1 v 2S:B (8) A v 9R:o2 (2) A v 1R:C (4) o2 v C (6)
B v o1 t o2 t o3 (9) o3 v C (7)
Our consequence-based algorithm constructs a graph whose vertices are called nodes. Each node describes a set of elements in the model I, which is an arbitrary model. The edges between nodes represent role successor relations between the corresponding elements. Each node v is associated with an atomic concept core(v). Intuitively, core(v) holds for every element of I that corresponds to v. Moreover, each node v is labeled with a set of clauses L(v). Each clause K v M 2 L(v) is related to core(v) and should be interpreted as core(v) u K v M .
Figure 1 illustrates the constructed graph for Example 1, where each node is shown as a circle. The core concept of each node v is shown as the subscript of v inside the circle, and the label of each node, L(v), is shown either below or above the circle. The numbers next to the clauses in L(v) correspond to the order of inference rule applications.
The inference process starts by initializing the algorithm according to the target query. Since in this example the query is q = A v D, we introduce a node vA where core(vA) = A, and add clause (10) to L(vA). Intuitively, this clause states that there has to be at least one element in the model I that satisfies A. Since nominals always exist, we also need to create one node vo, for representing each nominal o occurring in O. Therefore nodes voi for 1 i 3 are created to represent existing nominals and are initialized by clauses (11) – (13).
Afterwards, the subs rule (see Table 1) derives clauses (14) – (20). Since
only A is assumed to hold in vA, the algorithm derives only a linear number of
clauses. This rule is analogous to the Rv rule in the original completion rules
for E L [
Clause (14) and (15) state that vA must have R-successors o1I and o2I respectively. Clause (16) says that all the corresponding elements to vA must have an R-successor o3I or should satisfy D. On the other hand, clause (17) indicates that all the corresponding elements to vA must have at most one Rsuccessor in which C holds.
The Nom rule finds a solution that satisfies all these restrictions by means of an Integer Linear Programming (ILP) Component. This component is called whenever a QCR is added to the label of a node. Before feeding numerical restrictions to the ILP component, every number restriction should be encoded into an inequality. The encoding procedure will be discussed thoroughly in Section 4. The ILP component may also receive other information such as the subsumption relations in vo1 and vo2 in order to find a more constrained solution that is less likely to cause a contradiction later due to added entailments. The atomic concepts that participate in a disjunction with QCRs would not be reflected in inequalities, e.g., concept D in clause (16).
If the inequality system is feasible, the ILP component returns a possible solution which satisfies all numerical restrictions. The returned solution is a set of tuples each containing a partition element and its cardinality (see Section 4). In Example 1, the ILP component returns (vA) = fhfo1; o2; Cg; 1ig. Which means that, for satisfying the submitted constraints (14)-(17), there should exist one element in the domain in which o1; o2 and C hold. Due to the presence of nominals in the returned solution the Nom rule is applicable, which essentially checks if a nominal o always would appear in a partition element p together with a concept C 2 p (or another nominal o2 2 p). Accordingly, the Nom rule is applicable for nominals o1 and o2 and derives clauses (21) and (22).
The Nom rule does not apply to nominal o3, because clause (16) represents a possibility and if D is true in (16) then o3 does not have to exist in a partition element with o1 and o2. However, the consequences of assuming o3 to be equal to o1 and o2 still have to be checked. To reflect this possible equality in the graph, the Sigma rule adds clauses (26) – (29) to the graph. In general, the select function chooses a concept X of each partition element p as its representative. The concept X would be the core of a node v (core(v)= X). A clause D v D is added to the label of a node vX for every other concept D that holds in p, which reflects the possibility of holding D for elements corresponding to vX .
Clauses (26) and (21) state that o1; o2 and o3 are possibly merged, so, based on Clause (9) the cardinality of B would to be less than or equal to one. Clause (30) requires at least two elements in BI. One can verify that these constraints are infeasible altogether. The ILP component discovers this infeasibility and returns a set of clash culprits (Definition 7) that cause the contradiction. A clash culprit is the minimum set of literals such that their conjunction causes an infeasibility.
In this example, clauses o1 v o2, o1 v o3, o1 v 2R:B and B v o1 t o2 t o3 would be returned as a clash culprit altogether. But o1 v o3 is the only possible clause (shown by clause (26) and (28)) that participates in the contradiction. One can see that all (i.e. in our example, the only one) possible clauses that cause the clash exist in the label of the same node (L(o1)). Thus applying the Bottom rule adds clause (31) – (34) to the graph.
Clause (31) states that nominals o1; o3 can not hold (be merged) together, which makes the inequality system containing clauses (14) - (17) infeasible. There is only one possible clause in the returned clash culprits which is A v 9R:o1 and it belongs to L(vA), so, the Bottom rule produces clause (35).
Later, the inequality system corresponding to clauses (30) and (21) becomes feasible. Based on the solution returned by ILP, the Sigma rule requires two nodes corresponding to o2 and o3. But then, there is no need to introduce fresh nodes with cores o2 and o3 because our algorithm is designed to reuse the existing nodes vo2 and vo3 . Consequently, we introduce edges (36) and (37) using the Sigma rule.
Our reuse strategy is comparable to blocking techniques in tableau-based algorithms but is much more efficient in eliminating redundant computations. First, our algorithm never needs more than a linear number of nodes to the number of concepts occurring in ontology O, whereas tableau-based algorithms can construct trees of double exponential size. Second, the clauses in the label of each node are not localized to a specific element in I, and so our algorithm draws the inferences for a particular core only once.
Eventually, we use the Sigma rule to add clause (38), (39), and (40). At this point no further inference rule is applicable. Since all clauses are “relative” to the core of the corresponding node, clause (35) corresponds to A v D, so we have proved O j= A v D. In fact, due to (35), we know that O j= K v M for each query K v M such that A v D is a strengthening of K v M .
We are aware that an unrestricted application of the Subs rule can overwhelm
the whole graph with produced clauses. So, our next step will be to extend our
algorithm to employ an ordered resolution variant addressing this problem [
Definition 1 (Completion Graph). A Completion Graph G = (V; E ; L) is composed of a set of nodes. Each node v is labeled by an atomic concept C which is called core(v) and a set of clauses L(v). Each edge hu; vi 2 E is labeled by the set L(hu; vi) R.
In addition, G is over a set of literals L NL if L contains all literals in G. Through the rest of this paper we fix L to contain the set of literals occurring in O [ Q since O and Q are finite, set L is finite as well. Assuming v to be an arbitrary node in G and q = K v M to be an arbitrary query; then v covers q if core(v) K.
Definition 2 (Clause System). A clause system for a completion graph G is a function L that assigns a set of clauses L(v) to each node v 2 V. It is possible to decide query entailment based on L: A query q = K v M is entailed, O j= K v M , if and only if K v M 2 L(v), for each node v covering q and initialized so that K v L 2 L(v) holds for each literal L 2 K.
Theorem 1 states that all clauses derived by our calculus are indeed conclusions of the input ontology. The completeness of our algorithm is ensured by Theorem 2.
Definition 3 (Soundness). A completion graph G is sound for O, if for every edge R 2 L(hv; ui), there exist arbitrary elements ; 2 such that 2 (core(v))I , 2 (core(u))I and O j= h ; i 2 RI . A clause system L is sound for O if O j= core(v) u K v M holds for each node v 2 V and each clause K v M 2 L(v).
Theorem 1 (Soundness). Let G1 be a completion graph and let L1 be a clause system for G1. The completion graph G2 and the clause system L2 are obtained by applying an inference rule from Table 1 to G1 and L1. If G1 and L1 are sound for O, then both G2 and L2 are sound for O.
Theorem 2 (Completeness). Let G be a completion graph and let L be a clause system for G such that no inference rule from Table 1 is applicable to G and L. Then K v M 2 L(v) hold for each query q = K v M and each node v 2 V if O j= K v M and K v L 2 L(v) for each literal L 2 K.
are known to hold in a node v for which > v nR:C or > v nR:C has been derived in node v. Set Qp(v) contains QCRs that can possibly hold in a node v. These are those QCRs for which K v nR:L t M or K v nR:L t M has been derived in node v for some K 6 > or M 6 ?. The set Qp(v) is formally defined as Qp(v) = f./ nR:C j K v ./ nR:C t M 2 L(v); K 6 > or M 6 ?g.
are considered to hold in a node v. A clause K v M 2 L(v) is a possible clause, if either K > or M ?, otherwise, it would be a known clause. The set of known clauses in the label of a node v is denoted as Ck(v).
Definition 6 (select function). The select function chooses one qualifying concept C 2 p as the core, where C is either a qualifying concept in a known atleast restriction or a nominal, and p a partition element. If p contains a nominal o, then the select function always selects the nominal o as the representative for p. But if p contains more that one nominal then all of them are selected, one after the other. The consequences of the rule are applied to all these nominals. The method select is called a function because it returns a unique representative for all partition elements containing the same set of concepts.
Definition 7 (Clash Culprits (CC(v))). A Clash Culprit set (CC(v) = fCC1(v); :::; CCn(v)g) is returned by the ILP component if an inequality system is infeasible. A CCi; 1 i n consists of the minimum number of clauses such that the inequality system containing the corresponding inequalities is infeasible. Note that there may be more than one clash culprit for the same set of inequalities. For example assume we are trying to check the satisfiability of the QCRs: 2R:C; 3R:C and 1R:C. One can recognize two clash culprits in CC(v) that are involved in the clash, CC1 = f 2R:C; 1R:Cg and CC2 = f 3R:C; 1R:Cg. Considering each set of clash culprits may lead to a subsumption. Accordingly, we need to apply the Bottom rule for each CCi.
If all the clauses in a clash culprit are known information, we call it a strict unsatisfiablity, which can not be avoided by choosing an other possibility. The Bottom rule only considers possible clauses in a clash culprit set because known clauses can never be violated. Therefore, if all the clash culprits are known then it means that there is an unsatisfiability in the ontology. All clauses of a clash culprit set may not necessarily occur in the label of one particular node. In this case, no clauses can be derived based on the current knowledge. 4
We implement the ILP services in a separate module called the ILP component. The task of the ILP Component can be divided into three parts: producing variables, encoding numerical restrictions into inequalities and checking the satisfiability of derived inequalities.
The ILP component would be called for checking the satisfiablity of QCRs in the label of a node v. Each time, all QCR occurring in the label of v and all clauses in Ck(vC ), Ck(vo) and Cp(vo) are fed to ILP component, where C 2 Qv and o 2 No(v). 4.1
A decomposition set DS needs to include role successors of all related roles for a node v, which is defined as R(v) = fR j ./ n R:A occurs in L(v)g. If a role R appears in a partition element p, R 2 p, it means that all the elements of pI should be R successors. If a role does not appear in p, the elements of pI are assumed to be R0 successors where R0 is the complement of R.
One needs to include qualifying concepts in the decomposition set to capture the semantics of QCRs and also to handle their possible interaction with nominals. It allows to distinguish cases where role successors have different qualifications. When a partition element p includes a concept name A, it means that all the elements of pI are elements of AI . Otherwise, they are assumed to be elements of (:A)I . The set of qualifying concepts of R related to node v is defined as Qv(R) = fA j ./ nR:A occurs in L(v)g. Accordingly, the set of all qualifying concepts related to a node v is defined as Qv = SR2R(v) Qv(R).
Having nominals as part of our decomposition set allows reflecting their semantics in inequalities. Besides, the interpretation of each nominal o 2 No may interact with successors of a role R 2 NR if oI Succ(R). Additionally, The same nominal can interact with role successors of another role S. In this case, although R and S may not be related to each other according to the role hierarchy, their role successors may interact due to their interaction with the common nominal. If a nominal o 2 No is part of a partition element p, then it means that all the elements of pI have to be in oI . The set of related nominals for a node v, No(v) No; is defined as No(v) = fo j o occurs in L(vC ) such that C 2 Qvg. If a nominal o is not part of p then its negation :o is added to p by default. The restrictions imposed by nominals can not be handled node-locally. That is why nominals participate in the decomposition set of all related nodes. Definition 8 (Decomposition Set). A decomposition set DS(v) is defined for each node v, as DS(v) = R(v) [ Qv [ No(v).
Definition 9 (Partition). A partition P is the power set of DS(v) [ N:o, where N:o is the set of the negation of all nominals occurring in O. Each p 2 P is associated with a variable p, which is equal to the cardinality of pI . 4.2
The partition elements p 2 P are defined using the atomic decomposition technique, so they are semantically pairwise disjoint. Since the cardinality function of disjoint sets is additive, one can encode a cardinality restriction into an inequality using the sum of cardinalities, shown by sq, such that for each sq DS we have sq = sq p p for all p 2 P. Roughly speaking, sq is the sum of cardinalities of all partition elements containing sq. For example if DS = fR; C; og then R = RCo + RC + Ro + R and RC = RCo + RC . Hence, a cardinality bound imposed by QCRs or nominals on a subset of domain elements distributed over the elements in P can be encoded into inequalities as follows.
QCRs of the form nR:C or mS:D are mapped to inequalities RC n or SD m respectively. Based on nominal semantics, the sum of cardinalities of all partition elements containing a particular nominal should be equal to 1. We encode this cardinality bound by adding two inequalities of the form o 1 and o 1, for each nominal o 2 No.
Providing more information to the ILP component reduces the risk that a solution is returned which will fail later due to newly derived entailments.
Feeding subsumptions and disjointness to the ILP component allows the so-called infeasible operator to set the cardinality of some partition elements to zero. For this purpose, we define a binary variable bC 2 f0; 1g, C 2 DS, associated with each member of a decomposition set in order to apply conditional constraints on the presence of a role, concept or nominal in a partition element. Assuming that b? 0, we use binary variables and inequalities to disable infeasible partition elements, using the mappings presented below.
Subsumption Relation Assuming that in a clause of the form K v M , where K denotes dn j=1 Lj , all the literals are atomic i=1 Li and M denotes Fm concepts or nominals and Li 2 DS. Then the ILP component maps clause K v M to the inequality Pin=1 bLi (n 1) Pjm=1 bLj . For example translating a subsumption relation A v B produces bA bB, which ensures that if a partition element contains the atomic concept A, it should contain A’s subsumer B. In other words the cardinality of a partition element which contains A but not B has to be equal to zero.
This mapping can also be used for encoding axioms of the form A v o1 t o2 where o1 and o2 are two nominals. The obtained inequality, bA bo1 + bo2 , guarantees that if a partition element contains the atomic concept A then it has to contain either o1 or o2, i.e., the cardinality of a partition element that contains A but neither o1 nor o2, should be equal to zero.
Role Subsumption Every role subsumption relation of the form R v S can be encoded to the inequality bR bS . This inequality ensures that if a partition element contains a subrole R, it must contain all of R’s superroles, otherwise the cardinality of such a partition element should be equal to zero.
Universal Restriction A universal restriction of the form 8R:A can be
encoded to the inequality bR bA. The semantics of universal restriction implies
that all R successors are instance of A. The generated inequality satisfies this
semantics by implying that if a partition element contains the role R it should
also contain the concept A.
Lemma 1. If the submitted inequality system to the ILP component is feasible,
it will return a solution that satisfies all the constraints. The returned arithmetic
solution assigns a positive integer n to p, which denotes the cardinality of the
corresponding partition element. The ILP component would iterative through all
possible solutions that exist for solving an equality system [
tuples hp; pi produced by the ILP component for solving a particular inequality system related to a node v, where p is a partition element and p 2 N; p 1 is the cardinality of p.
If the inequality system is infeasible, then the ILP component returns the smallest set of clauses, called clash culprit set (Definition 7), such that the inequality system containing their corresponding inequalities is infeasible. There may be more than one minimum clash culprit set for each inequality system. 5
This paper presented an algebraic consequence-based reasoning algorithm for SHOQ. To the best of our knowledge, this is the first extension of consequencebased algorithms for the expressive description logic SHOQ. During the reasoning process, only one node is created for representing elements associated with each concept. Using a representative node for each concept not only helps in reducing the size of the generated framework but also allows for re-using elements. In contrast to tableau-based reasoners, our calculus naturally handles cyclic descriptions without the need for any blocking strategies to ensure termination.
Unlike most reasoning algorithms for SHOQ, the algebraic consequencebased method allows arithmetically informed reasoning about the numerical restrictions on domain elements by mapping numerical restrictions to inequalities and handling obtained inequality systems using integer linear programming methods. The consequence-based SHOQ reasoning is based on the atomic decomposition technique which is applied to the proper decomposition set allowing the calculus to handle the various interactions between nominals, role successors and their qualifications. The inference rules are designed in a way to derive all consequences of presented axioms while benefiting from lazy unfolding to avoid overwhelming the framework with unnecessary axioms. The inference rules are inspired by resolution to resolve complement literals.