This paper presents a novel SHOI tableau calculus which incorporates algebraic reasoning for deciding ontology consistency. Numerical restrictions imposed by nominals, existential and universal restrictions are encoded into a set of linear inequalities. Column generation and branch-and-price algorithms are used to solve these inequalities. Our preliminary experiments indicate that this calculus performs better on SHOI ontologies than standard tableau methods.
Description Logic (DL) is a formal knowledge representation language that is
used for modeling ontologies. Modern description logic systems provide
reasoning services that can automatically infer implicit knowledge from explicitly
expressed knowledge. Designing reasoning algorithms with high performance has
been one of the main concerns of DL researchers. One of the key features of
many description logics is support for nominals. Nominals are special concept
names that must be interpreted as singleton sets. They allow to use Abox
individuals within concept descriptions. However, nominals carry implicit global
numerical restrictions that increase reasoning complexity. Moreover, the
interaction between nominals and inverse roles leads to the loss of the tree model
property. Most state-of-the-art reasoners, such as Konclude [23], Fact++ [24],
HermiT [21], have implemented traditional tableau algorithms. Konclude also
incorporated consequence-based reasoning into its tableau calculus [22]. These
reasoners try to construct completion graphs in a highly non-deterministic way
in order to handle nominals. For example, a small ALCO ontology models
Canada consisting of its ten provinces: CA_Province fOntario, Quebec,
NovaScotia, NewBrunswick , Manitoba, BritishColumbia, PrinceEdwardIsland ,
Saskatchewan, NewfoundlandAndLabrador , Albertag. If one tries to model that
Canada consists of 11 provinces, it is trivial to see that it is not possible
because the cardinality of CA_Province is implicitly restricted to the 10 provinces
listed as nominals. However, according to our preliminary experiments, above
mentioned DL reasoners are unable to decide this inconsistency within a
reasonable amount of time. Consequence-based (CB) reasoning algorithms are also
extended to more expressive DLs such as SHOI [
However, algebraic DL reasoners are considered more efficient in handling
numerical restrictions [
In this paper, we present a novel algebraic tableau calculus for SHOI to
handle a large number of nominals and their interaction with inverse roles. The
rest of this paper is structured as follows. Section 2 defines important terms and
introduces SHOI. Section 3 presents the algebraic tableau calculus for SHOI.
Section 4 provides evaluation results for the implemented prototype Cicada. The
last section concludes our paper. An extended version of this paper [
In this section, we introduce SHOI and some notations used later. Let N = NC [ No where NC represents concept names and No nominals. Let NR be a set of role names with a set of transitive roles NR+ NR. The set of roles in SHOI is NR [ fR j R 2 NRg where R is called the inverse of R. A function Inv returns the inverse of a role such that Inv(R) = R if R 2 NR and Inv(R) = S if R = S and S 2 NR. An interpretation I = ( I ; I ) consists of a non-empty set I of individuals called the domain of interpretation and an interpretation function I . Table 1 presents syntax and semantic of SHOI. We use > (?) as an abbreviation for A t :A (A u :A) for some A 2 NC . In the following ]f:g denotes set cardinality.
A role inclusion axiom (RIA) of the form R v S is satisfied by I if RI SI . We denote with v the transitive, reflexive closure of v over NR. If R v S, we call R a subrole of S and S a superrole of R. A general concept inclusion (GCI) C v D is satisfied by I if CI DI . A role hierarchy R is a finite set of RIAs. A Tbox T is a finite set of GCIs. A Tbox T and its associated role hierarchy R is satisfied by I (or consistent) if each GCI and RIA is satisfied by I. Such an interpretation I is then called a model of T . A concept description C is said to be satisfiable by I iff CI 6= ;. An Abox A is a finite set of assertions of the form a : C (concept assertion) with aI 2 CI , and (a; b) : R (role assertion) with (aI ; bI ) 2 RI . Due to nominals, a concept assertion a : C can be transformed into a concept inclusion fag v C and a role assertion (a; b) : R into fag v 9R:fbg. Therefore, concept satisfiability and Abox consistency can be reduced to Tbox consistency by using nominals. We use fo1; : : : ; ong as an abbreviation for fo1g t t fong and may write fog as o. Moreover, we do not make the unique name assumption; therefore, two nominals might refer to the same individual.
Nominals carry implicit global numerical restrictions. For example, if C v fo1; o2; o3g (or fo1; o2; o3g v C), then o1; o2; o3 impose a numerical restriction that there can be at most (or at least, if o1; o2; o3 2 No are declared as pairwise disjoint) three instances of C. These restrictions are global because they affect the set of all individuals of C in I . These implicit numerical restrictions increase reasoning complexity. 3
An Algebraic Tableau Calculus for SHOI In this section, we present an algebraic tableau calculus for SHOI that decides Tbox consistency. Since nominals carry numerical restrictions, algebraic reasoning is used to ensure their semantics. The algorithm takes a SHOI Tbox T and its role hierarchy R as input and tries to create a complete and clash-free completion graph in order to check Tbox consistency. The reasoner is divided into two modules: 1) Tableau Module (TM), and 2) Algebraic Module (AM).
Let G = (V; E; L; B) be a completion graph for a SHOI Tbox T where V is a set of nodes and E a set of edges. Each node x 2 V is labelled with a set of concepts L(x), and each edge hx; yi 2 E with a set of role names L(x; y). For each node x 2 V , if L(x) contains a universal restriction on role R and there exists an R-neighbour of x, then B(x) contains a tuple of the form hv; L(x; v)i where v 2 V is an R-neighbour of x. We use ]v to denote the cardinality of a node v. For convenience, we assume that all concept descriptions are in negation normal form.
TM starts with some preprocessing and reduces all the concept axioms in a Tbox T to a single axiom > v CT such that CT := dCvD2T nnf (:C t D), where nnf transforms a given concept expression to its negation normal form. The algorithm checks consistency of T by testing the satisfiability of o v CT where o 2 No is a fresh nominal in T , which means that at least oI 2 CT I and CT I 6= ;. Moreover, since >I = I then every domain element must also satisfy CT . For creating a complete and clash-free completion graph, TM u-Rule if (C1 u C2) 2 L(x) and fC1; C2g * L(x)
then set L(x) = L(x) [ fC1; C2g t-Rule if (C1 t C2) 2 L(x) and fC1; C2g \ L(x) = ;
then set L(x) = L(x) [ fCg for some C 2 fC1; C2g 8-Rule if 8S:C 2 L(x) and there 9y with R 2 L(x; y), C 2= L(y) and R v S then set L(y) = L(y) [ fCg 8+-Rule if 8S:C 2 L(x) and there exist U; R with R 2 NR+ and U v R, R v S, and a node y with U 2 L(x; y) and 8R:C 2= L(y) then set L(y) = L(y) [ f8R:Cg nommerge -Rule if for some o 2 No there are nodes x, y with o 2 L(x) \ L(y), x 6= y then if x is an initial node, then merge y into x, else merge x into y inverse-Rule if 8R :C 2 L(y), R 2 L(x; y), and hx; L(y; x)i 2= B(y)
then set B(y) = B(y) [ fhx; L(y; x)ig l -Rule if hR; C; n; Vi 2 (x) and x is not blocked then 1. if V = ; and there exists no R-neighbour y of x with C L(y),
]y n, then create a new node y with L(y) C and ]y n
2. else for all v 2 V add C to L(v) and set ]v = n
e-Rule if hR; C; n; Vi 2 (x) and C L(y), ]y n, R * L(x; y)
then merge R into L(x; y) and fInv(R) j R 2 Rg into L(y; x), and
for all S with R v S 2 R add S to L(x; y) and Inv(S) to L(y; x)
applies expansion rules (see Figure 1 and Section 3.1). AM handles all numerical
restrictions using ILP. It generates inequalities and solves them using the
branchand-price technique (see Section 3.2 for details). We use equality blocking [
The u-Rule, t-Rule and 8-Rule are similar to standard tableau expansion rules for ALC. The 8+-Rule preserves the semantics of transitive roles. The nommerge -Rule merges two nodes containing in their label the same nominal. Suppose there is o 2 L(x) and o 2 L(y), and nodes x and y are not the same, then nommerge -Rule merges x into y. It adds L(x) to L(y) and moves all edges leading to (from) x so that they lead to (from) y. For each node z, if hz; yi 2 E and hz; xi 2 E, then L(z; y) = L(z; y) [ L(z; x). Similarly, if hy; zi 2 E and hx; zi 2 E, then L(y; z) = L(y; z) [ L(x; z). It also merges B(x) into B(y).
If L(x; y) = fRg and 8R :C 2 L(y), then the inverse-Rule encodes for AM the already existing R -edge by adding a tuple hx; fR gi to B(y). AM plays also an important role if nominals occur in universal restriction. For example, consider the axioms A v 9R:B, B v 9R :C u9R :Du8R :fo1; o2g and o1uo2 v ?, where A; B; C; D 2 NC , o1; o2 2 No and R 2 NR. Suppose we have A 2 L(x), R 2 L(x; y) and B 2 L(y). Since nominals carry numerical restrictions, 8R :fo1; o2g implies that we can have at most 2 R -neighbours of y. However, standard tableau reasoners might create two new R -neighbours of y without considering the existing R -neighbour x of y. Then they try to merge these three nodes in a non-deterministic way to satisfy the numerical restriction imposed by nominals. In our approach, the inverse-Rule encodes information about an existing R -neighbour of y and AM generates a deterministic solution.
For a node x, AM transforms all existential restrictions, universal restrictions and nominals to a corresponding system of inequalities. AM then processes these inequalities and gives back a solution set (x). The set (x) is either empty or contains solutions derived from feasible inequalities. In case of infeasibility AM signals a clash. A solution is defined by a set of tuples of the form hR; C; n; Vi with R NR, C N , n 2 N, n 1 and V V . Each tuple represents n R-neighbours of x (where R is a set of roles) that are instances of all elements of C. Here, V is an optional set that contains existing R-neighbours of x that must be reused and C is added to their labels. Consider the axiom A v 9R:B u 9R:C u 8S: fog, where A; B; C 2 NC , o 2 No, R; S 2 NR, R v S, and A 2 L(x). AM returns the solution (x) = fhfR; Sg; fB; C; og; 1ig. The l -Rule is used to generate nodes based on the arithmetic solution that satisfies a set of inequalities. For the above solution, the l -Rule creates one node y with cardinality 1 such that L(y) fB; C; og and ]y = 1. The e-Rule creates an edge between nodes x and y, and adds R; S to L(x; y) and Inv(R); Inv(S) to L(y; x). The e-Rule always adds all implied superroles to edge labels. 3.2
Generating Inequalities
Dantzig and Wolfe [
Branch-and-Price Method In the following, we use a Tbox T and its role hierarchy R, a completion graph G, a decomposition set Q and a partitioning P that is the power set of Q containing all subsets of Q except the empty set. Each partition element p 2 P represents the intersection of its elements. We decompose our problem into two subproblems: (i) restricted master problem (RMP), and (ii) pricing problem (PP). RMP contains a subset of columns and PP computes a column that can maximally reduce the cost of RMP’s objective. Whenever a column with negative reduced cost is found, it is added to RMP. Number restrictions are represented in RMP as inequalities, with a restricted set of variables. The flowchart in Figure 2 illustrates the whole process. Restricted Master Problem RMP is obtained by considering only variables xp with p 2 P0 and P0 P and relaxing the integrality constraints on the xp variables. Initially P0 is empty and RMP contains only artificial variables h to obtain an initial feasible inequality system. Each artificial variable corresponds to an element in Q9 [Qo such that hRq , Rq 2 Q9 and hIq , Iq 2 Qo. An arbitrarily large cost M is associated with every artificial variable. If any of these artificial variables exists in the final solution, then the problem is infeasible. The objective of RMP is defined as the sum of all costs as shown in (1) of the RMP below.
Min X costpxp + M hRq + M X hIq
Iq2Qo 1
Rq 2 Q9 (1) (2) (3) where a decision variable xp represents the elements of the partition element p 2 P0. The coefficients ap are associated with variables xp and apRq indicates whether an R-neighbour that is an instance of q exists in p. Similarly, aIpq indicates whether a nominal q exists in p. The weight costp defines the cost of selecting p and it depends on the number of elements p contains. Since we minimize the objective function, costp in the objective (1) ensures that only subsets with entailed concepts will be added which are the minimum number of concepts that are needed to satisfy all the axioms. Constraint (2) encodes existential restrictions and (3) numerical restrictions imposed by nominals (i.e., ]fogI = 1). Constraint (4) states the integrality condition relaxed from xp 2 Z+ to xp 2 R+. Pricing Problem: The objective of PP uses the dual values ; ! as coefficients of the variables that are associated with a potential partition element. The binary variables rRq , rIq , bq (q 2 N ) are used to ensure the description logic semantics. A binary variable rR> is used to handle role hierarchy. A variable bq is set to 1 if there exists an instance of concept q and rRq is set to 1 if there exists an R-neighbour that is an instance of concept q. Likewise, rIq is set to 1 if there exists a nominal q. Otherwise these variable are set to 0. The PP is given below.
Min X bq q2N rRq rIq rRq rR> rR>
X Rq2Q9 bq bq = 0 0 0 0 0 rR>
bq rS>
X
Iq2Qo Rq rRq !Iq rIq bq; rRq ; rIq ; rR> ; rS> 2 f0; 1g where vector and ! are dual variables associated with (2) and (3) respectively. For each at-least restriction represented in (2), Constraint (6) is added to PP, which ensures that if rRq = 1 then variable for bq must exist in P0. Similarly, (7) ensures the semantics of nominals represented in (2). Constraints (8) - (10) ensure the semantics of universal restrictions and role hierarchies respectively.
We can also map the semantics of selected DL axioms, where only atomic concepts occur, into inequalities, as shown in Table 2. For every T j= A u B v C, AM adds bA+bB 1 bC to PP. Therefore, if PP generates a partition containing A and B, then it must also contain C. Similarly, for every T j= A v B t C, AM adds bA bB + bC to PP. This inequality ensures that if a partition contains A, then it must also contain B or C.
Soundness and Completeness of Algebraic Module All existential restrictions and nominals are converted into linear inequalities and added to RMP. Other axioms, such as universal restrictions, role hierarchy, subsumption and disjointness, are embedded in PP. In case of feasible inequalities, the branchand-price algorithm returns a solution set that contains valid partition elements. Since the branch-and-price algorithm satisfies all the axioms embedded in RMP and PP, this solution is sound. Moreover, it is also complete because CPLEX is used to solve linear inequalities and it does not overlook any possible solution. Proposition 1. For a set of inequalities, the arithmetic module either generates an optimal solution which satisfies all inequalities or detects infeasibility. 3.3
Example Illustrating Rule Application and ILP formulation Consider the small Tbox
A v 9R:B u 9R:fo1g
B u fo1g v ? B v 9R:C u 9R :D u 8S :fo2g
C u D v ?
C v 9R:E
E v 8S : fo1g
with NR = fR; Sg, fA; B; C; D; Eg NC ; fo1; o2g No, and R v S 2 R. For
the sake of better readability, we apply in this example lazy unfolding [
Constraint (ii) ensures the semantics of nominals. 4. The values of rRo1 ; rIo1 are 1 in (PP 1a), therefore, the variable xRo1Io1 is added to (RMP 1b). Since only one b variable (i.e., bo1) is 1, the cost of xRo1Io1 is 1. P0 = ffRo1; Io1gg and the value of the objective function is reduced from 30 in (RMP 1a) to 11 in (RMP 1b).
RMP 1a
10hRB + 10hRo1 + 10hIo1 Subject to: hRB hRo1 hIo1 = 1 Solution: cost = 30, hRB = 1, hRo1 = 1; hIo1 = 1 Duals: RB = 10; Ro1 = 10; !Io1 = 10 rRB rRo1 Subject to:
PP 1b 5. As the value of rRB is 1 in (PP 1b), the variable xRB is added to (RMP 1c).
P0 = ffRo1, Io1g; fRBgg and the cost is further reduced from 11 in (RMP 1b) to 2 in (RMP 1c). 6. All artificial variables in (RMP 1c) are zero which might indicate that we have reached a feasible solution. The reduced cost of (PP 1c) is not negative anymore which means that (RMP 1c) cannot be improved further. Therefore, AM terminates after third ILP iteration and returns the optimal solution (x) = fhfRg ; fo1g ; 1i, hfRg ; fBg ; 1ig. 7. The l -Rule creates two new nodes x1 and x2 with L(x1) fo1g, L(x2) fBg, ]x1 1 and ]x2 1. 8. The e-Rule creates edges hx; x1i and hx; x2i with L (hx; x1i) fR; Sg and L (hx; x2i) fR; Sg (because R v S 2 R). It also creates back edges hx1; xi and hx2; xi with L (hx1; xi) fR ; S g and L (hx2; xi) fR ; S g. 9. By unfolding B in the label of x2 and by applying the u-Rule we get L(x2) = fB; 9R:C; 9R :D; 8S :fo2gg. 10. The inverse-Rule encodes information about existing R -neighbour x of x2 by adding a tuple hx; fR ; S gi to B(x2). 11. AM uses f9R:C; 9R :Dg to start ILP. Due to lack of space we cannot provide the complete RMP and PP solution process here. Since R v S, the universal restriction 8S : fo2g is ensured by adding the following inequalities to PP: Min xRo1Io1 +xRB +10hRB +10hRo1 +10hIo1
Min Subject to: xRB + hRB
1 1rRB rRB rRo1 bB bo1 0 0 rR rS 0, rS bo2 0, and for all rRq we added an equality rRq rR>> 0.>Therefore>, whenever rRq = 1 the values of rR> ; rS> ; bo2 = 1 . 12. Since B(x2) contains hx; fR ; S gi, AM adds node x in solution. Therefore,
AM returns the solution (x2) = fhfRg ; fCg ; 1i ; hfR ; S g ; fD; o2g ; 1; fxgig. 13. The l -Rule creates only one new node x3 with L(x3) fCg and ]x3 1, and updates the label of node x with L(x) fD; o2g. 14. The e-Rule creates edges hx2; x3i and hx3; x2i with L (hx2; x3i) fR; Sg and L (hx3; x2i) fR ; S g. 15. By unfolding C in the label of x3 we get L(x3) = fC; 9R:Eg. AM gives solution (x3) = fhfRg ; fEg ; 1ig. The l -Rule creates node x4 with L(x4) fEg and ]x4 1. The e-Rule creates edges hx3; x4i and hx4; x3i with L (hx3; x4i) fR; Sg and L (hx4; x3i) fR ; S g. 16. L(x4) = fE; 8S : fo1gg and after unfolding E the 8-Rule adds o1 to L(x3).
However, o1 already occurs in L(x1) and x1 6= x3. Therefore, the nommerge Rule merges node x3 into node x1. 17. Since no more rules are applicable, the tableau algorithm terminates. 4
We developed a prototype system called Cicada1 that implements our
calculus as proof of concept. Besides the use of ILP and branch-and-price Cicada
only implements a few standard optimization techniques such as lazy
unfolding [
Therefore, we built a set of synthetic test cases to empirically evaluate Cicada. Figure 6 presents some metrics of benchmark ontologies and evaluation results. We compared Cicada with major OWL reasoners such as FaCT++ (1.6.5) [24], HermiT (1.3.8) [21], and Konclude (0.6.2) [23]. 1 System and test ontologies: https://users.encs.concordia.ca/~haarslev/Cicada
Ontology Metrics Evaluation Results Ontology Name #Axioms #Concepts #Ind Cic FaC Her Kon EU-Members 67 32 28 4.86 TO TO TO CA-Provinces 32 14 11 2.85 316.4 TO TO
TestOnt-Cons TestOnt-InCons n #AxiOonmtsol#ogCyoMnceetprtiscs#Ind CEivcaluFaatCionHReresKulotsn CEivcaluFaaCtionHReresKulotsn 40 92 43 41 3.39 TO TO TO 4.41 TO TO TO 20 53 23 21 1.21 TO TO TO 3.16 TO TO TO 10 33 13 11 0.91 TO TO TO 2.68 401.7 TO TO 7 27 10 8 0.64 1.26 3.47 3.56 2.32 1.48 3.70 3.71 5 23 8 6 0.41 0.02 0.13 0.24 2.21 0.12 0.46 0.14
The first benchmark (see top part of Figure 6) uses two real-world ontologies.
The ontology EU-Members (adapted from [
The second benchmark (see bottom part of Figure 6) consists of small synthetic test ontologies that are using a variable n for representing the number of nominals. In order to test the effect of increased number of nominals we defined concept C and A as C v 9R :A and A v 9R:X1u; :::; u9R:Xn u 8R:fo1; :::; ong. Nominals o1; :::; on and concepts X1; :::; Xn are declared as pairwise disjoint. The first set consists of consistent ontologies in which we declared C and X1; :::; Xn 1 as pairwise disjoint. The second set consists of inconsistent ontologies in which we declared C and X1; :::; Xn as pairwise disjoint. Only Cicada can process the ontologies with more than 10 nominals within the time limit. 5
We presented a tableau-based algebraic calculus for handling the numerical restrictions imposed by nominals, existential and universal restrictions, and their interaction with inverse roles. These numerical restrictions are translated into linear inequalities which are then solved by using algebraic reasoning. The algebraic reasoning is based on a branch-and-price technique that either computes an optimal solution, or detects infeasibility. An empirical evaluation of our calculus showed that it performs better on ontologies having a large number of nominals, whereas other reasoners were unable to classify them within a reasonable amount of time. In future work, we will extend the technique presented here to SHOIQ. 21. Shearer, R., Motik, B., Horrocks, I.: HermiT: A highly-efficient OWL reasoner. In: Proceedings of the OWL: Experiences and Directions (OWLED). vol. 432, p. 91 (2008) 22. Steigmiller, A., Glimm, B., Liebig, T.: Coupling tableau algorithms for expressive description logics with completion-based saturation procedures. In: Proceedings of the 7th International Joint Conference on Automated Reasoning (IJCAR’14). pp. 449–463. Springer (2014) 23. Steigmiller, A., Liebig, T., Glimm, B.: Konclude: system description. Web Semantics: Science, Services and Agents on the World Wide Web 27, 78–85 (2014) 24. Tsarkov, D., Horrocks, I.: FaCT++ description logic reasoner: System description.
In: Proceedings of the International Joint Conference on Automated Reasoning. pp. 292–297. Springer (2006) 25. Vlasenko, J., Daryalal, M., Haarslev, V., Jaumard, B.: A saturation-based algebraic reasoner for ELQ. In: Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning (PAAR 2016). pp. 110–124. CEUR (2016) 26. Vlasenko, J., Haarslev, V., Jaumard, B.: Pushing the boundaries of reasoning about qualified cardinality restrictions. In: Proceedings of the International Symposium on Frontiers of Combining Systems. pp. 95–112. Springer (2017) 27. Zolfaghar Karahroodi, N., Haarslev, V.: A consequence-based algebraic calculus for SHOQ. In: Proceedings of the International Workshop on Description Logics (DL’17) (2017)