Handling Nominals and Inverse Roles using Algebraic Reasoning Humaira Farid and Volker Haarslev Concordia University, Montreal h_arid@encs.concordia.ca, haarslev@cse.concordia.ca Abstract. This paper presents a novel SHOI tableau calculus which incorporates algebraic reasoning for deciding ontology consistency. Nu- merical restrictions imposed by nominals, existential and universal re- strictions 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. 1 Introduction and Motivation Description Logic (DL) is a formal knowledge representation language that is used for modeling ontologies. Modern description logic systems provide reason- ing services that can automatically infer implicit knowledge from explicitly ex- pressed 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 in- dividuals within concept descriptions. However, nominals carry implicit global numerical restrictions that increase reasoning complexity. Moreover, the inter- action 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 ≡ {Ontario, Quebec, NovaScotia, NewBrunswick , Manitoba, BritishColumbia, PrinceEdwardIsland , Saskatchewan, NewfoundlandAndLabrador , Alberta}. If one tries to model that Canada consists of 11 provinces, it is trivial to see that it is not possible be- cause 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 rea- sonable amount of time. Consequence-based (CB) reasoning algorithms are also extended to more expressive DLs such as SHOI [6] and SROIQ [7]. Since their implementations are not available, we could not analyze these reasoners. However, algebraic DL reasoners are considered more efficient in handling numerical restrictions [10,13,14,25]. RacerPro [14] was the first highly optimized reasoner that combined tableau-based reasoning with algebraic reasoning [15]. Other tableau-based algebraic reasoner for SHQ [13], SHIQ [20], SHOQ [11,10] are also proposed to handle qualified number restrictions (QNRs) and their in- teraction with inverse roles or nominals. These reasoners use an atomic decom- position technique to encode number restrictions into a set of linear inequalities. These inequalities are then solved by integer linear programming (ILP). These reasoners perform very efficiently in handling huge values in number restrictions. However, their ILP algorithms are best-case exponential to the number of in- equalities. For example, in case of m inequalities they require 2m variables in order to find the optimal solution. However, for ILP with a huge number of variables it is not feasible to enumerate all variables. To overcome this problem, the column generation technique has been used [25,27] which considers a small subset of variables. However, to the best of our knowledge, no algebraic calculus can handle DLs supporting nominals and inverse roles simultaneously. 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 [12] contains more details about ILP and the example presented in Section 3.3. 2 Preliminaries 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 ∪ {R− | R ∈ NR } where R− is called the inverse of R. A function Inv returns the inverse of a role such that Inv(R) = R− if R ∈ NR and Inv(R) = S if R = S − and S ∈ 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 ∈ NC . In the following ]{.} denotes set cardinality. A role inclusion axiom (RIA) of the form R v S is satisfied by I if RI ⊆ S I . 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 C I ⊆ 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 C I 6= ∅. An Abox A is a finite set of assertions of the form a : C (concept assertion) with aI ∈ C I , and (a, b) : R (role assertion) with (aI , bI ) ∈ RI . Due to nominals, a concept assertion a : C can be transformed into a concept inclusion {a} v C and a role assertion (a, b) : R into {a} v ∃R.{b}. Therefore, concept satisfiability and Abox consistency can be reduced to Tbox consistency Table 1. Syntax and semantics of SHOI Construct Syntax Semantics atomic concept A AI ⊆ ∆I negation ¬C ∆I \ C I conjunction C uD C I ∩ DI disjunction C tD C I ∪ DI value restriction ∀R.C {x ∈ ∆I | ∀y : (x, y) ∈ RI ⇒ y ∈ C I } exists restriction ∃R.C {x ∈ ∆I | ∃y ∈ ∆I : (x, y) ∈ RI ∧ y ∈ C I } nominal {o} ]{o}I = 1 role R RI ⊆ ∆I × ∆I − inverse role R (R− )I = {(y, x) | (x, y) ∈ RI } transitive role R ∈ NR+ (x, y) ∈ RI ∧ (y, z) ∈ RI ⇒ (x, z) ∈ RI by using nominals. We use {o1 , . . . , on } as an abbreviation for {o1 } t · · · t {on } and may write {o} 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 {o1 , o2 , o3 } (or {o1 , o2 , o3 } v C), then o1 , o2 , o3 impose a numerical restriction that there can be at most (or at least, if o1 , o2 , o3 ∈ No are declared as pair- wise 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 reason- ing 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 ∈ V is labelled with a set of concepts L(x), and each edge hx, yi ∈ E with a set of role names L(x, y). For each node x ∈ 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 ∈ 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 alldthe concept axioms in a Tbox T to a single axiom > v CT such that CT := CvD∈T 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 ∈ No is a fresh nominal in T , which means that at least oI ∈ 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 ) ∈ L(x) and {C1 , C2 } * L(x) then set L(x) = L(x) ∪ {C1 , C2 } t-Rule if (C1 t C2 ) ∈ L(x) and {C1 , C2 } ∩ L(x) = ∅ then set L(x) = L(x) ∪ {C} for some C ∈ {C1 , C2 } ∀-Rule if ∀S.C ∈ L(x) and there ∃y with R ∈ L(x, y), C ∈ / L(y) and R v∗ S then set L(y) = L(y) ∪ {C} ∀+ -Rule if ∀S.C ∈ L(x) and there exist U, R with R ∈ NR+ and U v∗ R, R v∗ S, and a node y with U ∈ L(x, y) and ∀R.C ∈ / L(y) then set L(y) = L(y) ∪ {∀R.C} nommerge -Rule if for some o ∈ No there are nodes x, y with o ∈ 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 ∀R− .C ∈ L(y), R ∈ L(x, y), and hx, L(y, x)i ∈ / B(y) then set B(y) = B(y) ∪ {hx, L(y, x)i} fil -Rule if hR, C, n, Vi ∈ σ(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 ∈ V add C to L(v) and set ]v = n e-Rule if hR, C, n, Vi ∈ σ(x) and C ⊆ L(y), ]y ≥ n, R * L(x, y) then merge R into L(x, y) and {Inv(R) | R ∈ R} into L(y, x), and for all S with R v∗ S ∈ R add S to L(x, y) and Inv(S) to L(y, x) Fig. 1. The expansion rules for SHOI 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 branch- and-price technique (see Section 3.2 for details). We use equality blocking [18,16] due to the presence of inverse roles. 3.1 Expansion Rules In order to check the consistency of a Tbox T , the proposed algorithm creates a completion graph G using the expansion rules shown in Figure 1. A node x in G contains a clash if {A, ¬A} ⊆ L(x) for A ∈ NC or AM has no feasible solution for x. G is complete if no expansion rule is applicable to any node in G. T is consistent if G is complete and no node in G contains a clash. The u-Rule, t-Rule and ∀-Rule are similar to standard tableau expansion rules for ALC. The ∀+ -Rule preserves the semantics of transitive roles. The nommerge -Rule merges two nodes containing in their label the same nominal. Suppose there is o ∈ L(x) and o ∈ 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 ∈ E and hz, xi ∈ E, then L(z, y) = L(z, y) ∪ L(z, x). Similarly, if hy, zi ∈ E and hx, zi ∈ E, then L(y, z) = L(y, z) ∪ L(x, z). It also merges B(x) into B(y). If L(x, y) = {R} and ∀R− .C ∈ L(y), then the inverse-Rule encodes for AM the already existing R− -edge by adding a tuple hx, {R− }i to B(y). AM plays also an important role if nominals occur in universal restriction. For example, consider the axioms A v ∃R.B, B v ∃R− .Cu∃R− .Du∀R− .{o1 , o2 } and o1 uo2 v ⊥, where A, B, C, D ∈ NC , o1 , o2 ∈ No and R ∈ NR . Suppose we have A ∈ L(x), R ∈ L(x, y) and B ∈ L(y). Since nominals carry numerical restrictions, ∀R− .{o1 , o2 } 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 ∈ 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 ∃R.B u ∃R.C u ∀S. {o}, where A, B, C ∈ NC , o ∈ No , R, S ∈ NR , R v S, and A ∈ L(x). AM returns the solution σ(x) = {h{R, S}, {B, C, o}, 1i}. The fil -Rule is used to generate nodes based on the arithmetic solution that satisfies a set of inequalities. For the above solution, the fil -Rule creates one node y with cardinality 1 such that L(y) ← {B, C, o} 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 [8] proposed a column generation technique for solving linear programming (LP) problems, called Dantzig–Wolfe decomposition, where a large LP is decomposed into a master problem and a subproblem (or pricing problem). In case of LP problems with a huge number of variables, column generation works with a small subset of variables and builds a Restricted Master Problem (RMP). The Pricing Problem (PP) generates a new variable with the most reduced cost if added to RMP (see [4,26] for details). However, column generation may not necessarily give an integral solution for an LP relaxation, i.e., at least one variable has not an integer value. Therefore, the branch-and-price method [3] has been used which is a combination of column generation and branch-and- bound technique [9]. We employ this technique by mapping number restrictions to linear inequality systems using a column generation ILP formulation (see [26] for details). CPLEX [5] has been used to solve our ILP formulation. Encoding Existential Restrictions and Nominals into Inequalities The atomic decomposition technique [19] is used to encode numerical restrictions on concepts and role fillers into inequalities. These inequalities are then solved for deciding the satisfiability of the numerical restrictions. The existential re- strictions are converted into ≥ 1 inequalities. The cardinality of a partition element containing a nominal o is equal to 1 due to the nominal semantics; ]{o}I = 1 for each nominal o ∈ No . Therefore, the decomposition set is defined as Q = Q∃ ∪ Q∀ ∪ Qo , where Q∃ (Q∀ ) contains existential (universal) restrictions Fig. 2. Overview of the algebraic reasoning process and Qo contains all related nominals. Each element Rq ∈ Q∃ ∪ Q∀ represents a role R ∈ NR and its qualification concept expression q and each element Iq ∈ Qo represents a nominal q ∈ No . The elements in Q∀ are used by AM to ensure the semantics of universal restrictions. The set of related nominals Qo ⊆ No is defined as Qo = {o | o ∈ clos(q) ∧ Rq ∈ Q∃ ∪ Q∀ } where clos(q) is the closure of concept expression q. The atomic decomposition considers all possible ways to decompose Q into sets that are semantically pairwise disjoint. 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 ∈ 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 ∈ P 0 and P 0 ⊆ P and relaxing the integrality constraints on the xp variables. Initially P 0 is empty and RMP contains only artificial variables h to obtain an initial feasible inequality system. Each artificial variable corresponds to an element in Q∃ ∪Qo such that hRq , Rq ∈ Q∃ and hIq , Iq ∈ 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. X X X Min costp xp + M hRq + M hIq subject to (1) p∈P 0 Rq ∈Q∃ Iq ∈Qo X aR p xp + hRq ≥ 1 Rq ∈ Q∃ q (2) p∈P 0 X aIpq xp + hIq = 1 Iq ∈ Qo (3) p∈P 0 xp ∈ R+ with p ∈ P 0 (4) aR Iq + p , ap ∈ {0, 1}, hRq , hIq ∈ R with Rq ∈ Q∃ , Iq ∈ Qo q where a decision variable xp represents the elements of the partition element p ∈ R P 0 . The coefficients ap are associated with variables xp and ap q indicates whether I an R-neighbour that is an instance of q exists in p. Similarly, apq 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., ]{o}I = 1). Constraint (4) states the integrality condition relaxed from xp ∈ Z+ to xp ∈ 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 ∈ 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. X X X Min bq − πRq rRq − ωIq rIq subject to (5) q∈N Rq ∈Q∃ Iq ∈Qo rRq − bq ≤ 0 Rq ∈ Q∃ , R ∈ NR , q ∈ NC (6) rIq − bq = 0 Iq ∈ Qo , q ∈ No (7) rRq − rR> ≤ 0 R ∈ NR , q ∈ N (8) rR> − bq ≤ 0 Rq ∈ Q∀ , R ∈ NR , q ∈ N (9) rR> − rS> ≤ 0 R v S ∈ R, R, S ∈ NR (10) bq , rRq , rIq , rR> , rS> ∈ {0, 1} 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 P 0 . 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 |= 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 |= 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 restric- tions and nominals are converted into linear inequalities and added to RMP. Table 2. DL axioms and their corresponding PP inequalities (n ≥ 1) DL Axiom Inequality in PP Description Pn If a set contains A1 , ..., An , then it A1 u ... u An v B i=1 bAi − (n − 1) ≤ bB also contains B.∗ If a set contains A, then it also bA ≤ n P A v B1 t ... t Bn i=1 bBi contains at least one concept from B1 , ..., Bn . ∗ Encodes unsatisfiability and disjointness in case B v∗ ⊥ Other axioms, such as universal restrictions, role hierarchy, subsumption and disjointness, are embedded in PP. In case of feasible inequalities, the branch- and-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 ∃R.B u ∃R.{o1} B u {o1} v ⊥ B v ∃R.C u ∃R− .D u ∀S − .{o2} C uD v⊥ C v ∃R.E E v ∀S − . {o1} with NR = {R, S}, {A, B, C, D, E} ⊆ NC , {o1, o2} ⊆ No , and R v S ∈ R. For the sake of better readability, we apply in this example lazy unfolding [2,17]. 1. We start with root node x and its label L(x) = {A} and by unfolding A and applying the u-Rule we get L(x) = {A, ∃R.B, ∃R.{o1}}. 2. Since {∃R.B, ∃R.{o1}} ⊆ L(x), AM generates a corresponding set of inequli- ties and applies ILP considering known subsumption and disjointness. 3. For solving these inequalities, RMP starts with artificial variables, P 0 is initially empty, and Q∃ = {RB , Ro1 }, Q∀ = ∅ and Qo = {Io1 } (see Fig. 3). The objective of (PP 1a) uses the dual values from (RMP 1a). For each at-least restriction a constraint (e.g., ∃R.B rRB − bB ≤ 0) is added to (PP 1a), which indicates that if rRB = 1 then a variable bB will also be 1. Constraint (i) ensures that B and o1 cannot exist in same partition element. Constraint (ii) ensures the semantics of nominals. 4. The values of rRo1 , rIo1 are 1 in (PP 1a), therefore, the variable xRo1 Io1 is added to (RMP 1b). Since only one b variable (i.e., bo1 ) is 1, the cost of xRo1 Io1 is 1. P 0 = {{Ro1 , Io1 }} and the value of the objective function is reduced from 30 in (RMP 1a) to 11 in (RMP 1b). RMP 1a PP 1a Min Min 10hRB + 10hRo1 + 10hIo1 bB + bo1 − 10rRB − 10rRo1 − 10rIo1 Subject to: hRB ≥ 1 hRo1 ≥ 1 Subject to: r RB − b B ≤ 0 bB + bo1 ≤ 1 (i) hIo1 = 1 rRo1 − bo1 ≤ 0 rIo1 − bo1 = 0 (ii) Solution: cost = 30, hRB = 1, hRo1 = 1, hIo1 = 1 Solution: cost = −19, rRB = 0, Duals: πRB = 10, πRo1 = 10, ωIo1 = 10 rRo1 = 1, rIo1 = 1, bB = 0, bo1 = 1 Fig. 3. Node x: First ILP iteration Min RMP 1b PP 1b Min xRo1 Io1 + 10hRB + 10hRo1 + 10hIo1 bB + bo1 − 10rRB − 10rRo1 + 9rIo1 Subject to: h RB ≥ 1 Subject to: xRo1 Io1 + hRo1 ≥ 1 r RB − b B ≤ 0 bB + bo1 ≤ 1 (i) xRo1 Io1 + hIo1 = 1 rRo1 − bo1 ≤ 0 rIo1 − bo1 = 0 (ii) Solution: cost = 11, xRo1 Io1 = 1, hRB = 1, hRo1 , hIo1 = 0 Solution: cost = −9, rRB = 1, Duals: πRB = 10, πRo1 = 10, ωIo1 = −9 rRo1 = 0, rIo1 = 0, bB = 1, bo1 = 0 Fig. 4. Node x: Second ILP iteration 5. As the value of rRB is 1 in (PP 1b), the variable xRB is added to (RMP 1c). P 0 = {{Ro1 , Io1 }, {RB }} 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) = {h{R} , {o1} , 1i, h{R} , {B} , 1i}. 7. The fil -Rule creates two new nodes x1 and x2 with L(x1 ) ← {o1}, L(x2 ) ← {B}, ]x1 ← 1 and ]x2 ← 1. 8. The e-Rule creates edges hx, x1 i and hx, x2 i with L (hx, x1 i) ← {R, S} and L (hx, x2 i) ← {R, S} (because R v S ∈ R). It also creates back edges hx1 , xi and hx2 , xi with L (hx1 , xi) ← {R− , S − } and L (hx2 , xi) ← {R− , S − }. 9. By unfolding B in the label of x2 and by applying the u-Rule we get L(x2 ) = {B, ∃R.C, ∃R− .D, ∀S − .{o2}}. 10. The inverse-Rule encodes information about existing R− -neighbour x of x2 by adding a tuple hx, {R− , S − }i to B(x2 ). 11. AM uses {∃R.C, ∃R− .D} 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 ∀S − . {o2} is ensured by adding the following inequalities to PP: Min RMP 1c PP 1c xRo1 Io1 +xRB +10hRB +10hRo1 +10hIo1 Min bB + bo1 − 1rRB − 10rRo1 + 9rIo1 Subject to: xRB + hRB ≥ 1 Subject to: xRo1 Io1 + hRo1 ≥ 1 r RB − b B ≤ 0 bB + bo1 ≤ 1 (i) xRo1 Io1 + hIo1 = 1 rRo1 − bo1 ≤ 0 rIo1 − bo1 = 0 (ii) Solution: cost = 2, xRo1 Io1 = 1, xRB = 1, hRB , hRo1 , hIo1 = 0 Solution: Duals: πRB = 1, πRo1 = 10, ωIo1 = −9 cost = 0, all variables are 0. Fig. 5. Node x: Third ILP iteration 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, {R− , S − }i, AM adds node x in solution. Therefore, AM returns the solution σ(x2 ) = {h{R} , {C} , 1i , h{R− , S − } , {D, o2} , 1, {x}i}. 13. The fil -Rule creates only one new node x3 with L(x3 ) ← {C} and ]x3 ← 1, and updates the label of node x with L(x) ← {D, o2}. 14. The e-Rule creates edges hx2 , x3 i and hx3 , x2 i with L (hx2 , x3 i) ← {R, S} and L (hx3 , x2 i) ← {R− , S − }. 15. By unfolding C in the label of x3 we get L(x3 ) = {C, ∃R.E}. AM gives so- lution σ(x3 ) = {h{R} , {E} , 1i}. The fil -Rule creates node x4 with L(x4 ) ← {E} and ]x4 ← 1. The e-Rule creates edges hx3 , x4 i and hx4 , x3 i with L (hx3 , x4 i) ← {R, S} and L (hx4 , x3 i) ← {R− , S − }. 16. L(x4 ) = {E, ∀S − . {o1}} and after unfolding E the ∀-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 Performance Evaluation We developed a prototype system called Cicada1 that implements our calcu- lus as proof of concept. Besides the use of ILP and branch-and-price Cicada only implements a few standard optimization techniques such as lazy unfold- ing [2,17], nominal absorption [17], and dependency directed backtracking [1] as well as a ToDo list architecture [24] to control the application of the expansion rules. Cicada might not perform well for SHOI ontologies that require other optimization techniques. 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 Ontology Metrics Evaluation Results Evaluation Results n #Axioms #Concepts #Ind Cic FaC Her Kon Cic FaC Her Kon 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 Fig. 6. Metrics of Benchmark Ontologies and Evaluation Results with runtime in sec- onds and a timeout of 1000 seconds (TO=timeout, #=Number of..., Ind=Individuals, Cic=Cicada, FaC=FaCT++, Her=HermiT, Kon=Konclude) The first benchmark (see top part of Figure 6) uses two real-world ontologies. The ontology EU-Members (adapted from [10]) models 28 members of European Union (EU) whereas CA-Provinces models 10 provinces of Canada. We added nominals requiring 29 EU members and 11 Canadian provinces respectively. The results show that only Cicada can identify the inconsistency of EU-Members within the time limit. Moreover, Cicada is more than two orders of magnitude faster than FaCT++ in identifying the inconsistency of CA-Provinces. The second benchmark (see bottom part of Figure 6) consists of small syn- thetic 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 ∃R− .A and A v ∃R.X1 u, ..., u∃R.Xn u ∀R.{o1 , ..., on }. 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 Conclusion We presented a tableau-based algebraic calculus for handling the numerical re- strictions 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 alge- braic 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 nomi- nals, 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. References 1. Baader, F.: The description logic handbook: Theory, implementation and applica- tions. Cambridge university press (2003) 2. Baader, F., Hollunder, B., Nebel, B., Profitlich, H.J., Franconi, E.: Am empiri- cal analysis of optimization techniques for terminological representation systems. Applied Intelligence 4(2), 109–132 (1994) 3. Barnhart, C., Johnson, E.L., Nemhauser, G.L., Savelsbergh, M.W., Vance, P.H.: Branch-and-price: Column generation for solving huge integer programs. Opera- tions research 46(3), 316–329 (1998) 4. Chvatal, V.: Linear programming. Macmillan (1983) 5. CPLEX optimizer, https://www.ibm.com/analytics/cplex-optimizer 6. Cucala, D.T., Cuenca Grau, B., Horrocks, I.: Consequence-based reasoning for description logics with disjunction, inverse roles, and nominals. In: Proceedings of the 30th International Workshop on Description Logics (July 2017) 7. Cucala, D.T., Cuenca Grau, B., Horrocks, I.: Consequence-based reasoning for description logics with disjunction, inverse roles, number restrictions, and nominals. In: Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI-18. pp. 1970–1976 (2018) 8. Dantzig, G.B., Wolfe, P.: Decomposition principle for linear programs. Operations research 8(1), 101–111 (1960) 9. Desrosiers, J., Soumis, F., Desrochers, M.: Routing with time windows by column generation. Networks 14(4), 545–565 (1984) 10. Faddoul, J., Haarslev, V.: Algebraic tableau reasoning for the description logic SHOQ. Journal of Applied Logic 8(4), 334–355 (2010) 11. Faddoul, J., Haarslev, V.: Optimizing algebraic tableau reasoning for SHOQ: First experimental results. In: Proceedings of the 23rd International Workshop on De- scription Logics (DL’10). pp. 161–171 (2010) 12. Farid, H., Haarslev, V.: Handling nominals and inverse roles using algebraic reason- ing (2018), extended version of the paper published in Proceedings of the Interna- tional Workshop on Description Logics (DL’18). https://arxiv.org/abs/1810.00916 13. Farsiniamarj, N., Haarslev, V.: Practical reasoning with qualified number restric- tions: A hybrid Abox calculus for the description logic SHQ. AI Communications 23(2-3), 205–240 (2010) 14. Haarslev, V., Möller, R.: Racer system description. In: Proceedings of the Interna- tional Joint Conference on Automated Reasoning. pp. 701–705. Springer (2001) 15. Haarslev, V., Timmann, M., Möller, R.: Combining tableaux and algebraic meth- ods for reasoning with qualified number restrictions. In: Proceedings of the Inter- national Workshop on Description Logics (DL’01) (2001) 16. Hladik, J.: A tableau system for the description logic SHIO. In: Proceedings of the Doctoral Programme of IJCAR. vol. 106. Citeseer (2004) 17. Horrocks, I.: Using an expressive description logic: FaCT or fiction? In: Proceedings of the 6th International Conference on Principles of Knowledge Representation and Reasoning (KR’98). vol. 98, pp. 636–645 (1998) 18. Horrocks, I., Sattler, U.: A description logic with transitive and inverse roles and role hierarchies. Journal of logic and computation 9(3), 385–410 (1999) 19. Ohlbach, H., Köhler, J.: Modal logics, description logics and arithmetic reasoning. Artificial Intelligence 109(1-2), 1–31 (1999) 20. Roosta Pour, L., Haarslev, V.: Algebraic reasoning for SHIQ. In: Proceedings of the International Workshop on Description Logics (DL’12). pp. 530–540 (2012) 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 Seman- tics: 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)