A Saturation-based Algebraic Reasoner for ELQ Jelena Vlasenko, Maryam Daryalal, Volker Haarslev, and Brigitte Jaumard Concordia University, Montreal, Quebec, Canada Abstract We present a reasoning architecture for deciding subsumption for the description logic ELQ. Our architecture combines saturation rules with algebraic reasoning based on Integer Linear Programming (ILP). De- ciding the so-called numerical satisfiability of a set of qualified cardi- nality restrictions is reduced to constructing a corresponding system of linear inequalities and applying ILP methods in order to determine whether this system is feasible. Our preliminary experiments indicate that this calculus offers a better scalability for qualified cardinality re- strictions than approaches combining both tableaux and ILP as well as traditional (hyper)tableau methods. 1 Introduction and Motivation We present a reasoning architecture for the description logic (DL) ELQ that is inspired by saturation-based algorithms for EL [BBL05] but incorporates a new algebraic approach to decide subsumption for ELQ. ELQ is as expressive as ALCQ because every ALCQ Tbox T can be rewritten to an ELQ Tbox T 0 such that T 0 is a conservative extension of T . This is possible since ELQ allows one to write axioms denoting disjunction and negation via QCRs (see Section 3 for an example). The performance of the original ALCQ tableau algorithm [HB91] that is implemented by most DL reasoners covering QCRs is not optimal. To perform a concept satisfiability test, this tableau algorithm creates role successors to satisfy at-least restrictions, e.g. ≥ 20 R.C. Given at-most restrictions, e.g., ≤ 10 R.D, ≤ 10 R.E, the algorithm resolves each R-successor as either D or ¬D, and E or ¬E. If an at-most restriction for R is violated (≤ 10 R.D), the algorithm nondeterministically merges two R-successors that are instances of D. This uninformed process is highly inefficient, especially when the algorithm has to deal with larger cardinalities and/or large sets of related QCRs. In our previous work (originally inspired by [OK99]) we have shown that algebraic tableau can improve reasoning on QCRs dramatically for DLs such as SHQ [FH10c], SHIQ [RH12], and SHOQ [FH10a, FH10b]. The basic idea in these calculi is to transform a set of QCRs into a system of linear inequalities to be solved by Integer Linear Programming (ILP). If ILP finds a solution to the system of inequalities, i.e., the system is feasible, then the corresponding set of QCRs is satisfiable provided completion rules encounter no logical clashes for the returned numerical solution. Although the prototypes implementing the above-mentioned approaches on algebraic tableaux [FH10c, RH12, FH10b] could demonstrate runtime improvements of several orders of magnitude for reasoning about QCRs (and nominals) we identified the following disadvantageous characteristics: (i) Given n QCRs (and nominals) the naive encoding of the corresponding system of inequalities requires n rows and 2m columns, where m is the cardinality of the set P of all the role names and concepts occurring in the n given QCRs. Let us illustrate this with a small example: ≥ 2R.C u ≥ 2R.D u ≤ 2R.E. In this case, P = {R, C, D, E}, n = 3, m = 4. In Copyright c by the paper’s authors. Copying permitted for private and academic purposes. In: P. Fontaine, S. Schulz, J. Urban (eds.): Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning (PAAR 2016), Coimbra, Portugal, 02-07-2016, published at http://ceur-ws.org 110 P P P P order to represent the QCRs as inequalities we create xCi ≥ 2, xDj ≥ 2, xDk ≥ 2, and xEl ≤ 2. For instance, the variables xCi represent the cardinalities of all elements in the power set of P that contain C, R. The same holds for the other variables respectively. As an additional constraint we specify that all variables must be greater or equal to zero. Our objective function minimizes the sum of all variables. Intuitively speaking, the above-mentioned concept conjunction is feasible and in this trivial case also satisfiable if the given system of inequalities has an integer solution. It is easy to see that the size of such an inequality system is exponential to m. Furthermore, in order to ensure completeness, we required a so-called choose rule that implements a semantic split that nondeterministically adds for each variable x either the inequality x ≤ 0 or x ≥ 1. Unfortunately, this m uninformed choose rule could fire 22 times in the worst case and cause a severe performance degradation. (ii) The employed ILP algorithms were best-case exponential in the number of occurring QCRs due to the explicit representation of 2m variables. In [FH10a, FH10b] we developed an optimization technique called lazy partitioning that tries to delay the creation of ILP variables but it cannot avoid the creation of 2m variables in case m QCRs are part of a concept model. Our experiments in [FH10a, FH10b, FH10c] indicated that quite a few ILP solutions can cause clashes due to lack of knowledge about known subsumptions, disjointness, and unsatisfiability of concept conjunctions. This knowledge can help reducing the number of variables and eliminating ILP solutions that would fail logically. For instance, an ILP solution for the example presented in the previous paragraph might require the creation of an R-successor as an instance of C u D u ¬E. However, if C and D are disjoint this ILP solution will cause a clash (and fail logically). Characteristic (i) can be avoided by eliminating the choose rule for variables. This does not sacrifice complete- ness because the algorithms implementing our ILP component are complete (and certainly sound) for deciding (in)feasibility. In case a system is feasible (or numerically satisfiable), dedicated saturation rules determine whether the returned solutions are logically satisfiable. In case of logical unsatisfiability a corresponding unsat- isfiable concept conjunction is added to the input of the ILP component and therefore monotonically constrains the remaining feasibility space. Consequently, previously computed solutions that result in unsatisfiability are eliminated. For instance, the example above would be deemed as infeasible once the ILP component learns that C and D are subsumed by E and that C and D are disjoint. The avoidance of characteristic (ii) is motivated by the observation that only a small number of the 2m variables will have non-zero values in the optimal solution of the linear relaxation, i.e., no more variables than the number of constraints following the characteristics of the optimal solution of a linear program, see, e.g., [Chv83]. As a consequence, only a limited number of variables have a nonzero value in the integer optimal solution. In addition, linear programming techniques such as column generation [DW60, GG61] can operate with as few variables as the set of so-called basic variables in linear programming techniques at each iteration, i.e., nonbasic variables can be eliminated and are not required for the guarantee of reaching the conclusion that a system of linear inequalities is infeasible, or for reaching an optimal LP solution. Although the required number of iterations varies from one case to another, it is usually extremely limited in practice, in the order of few times the number of constraints. The efficiency of the branch-and-price approach, which is required in order to derive an ILP solution, see, e.g., [BJN+ 98, Van11, LD05], depends on the quality of the integrality gap (i.e., how far the optimal linear programming solution is from the optimal ILP solution in case the system of inequalities is feasible, and on the level of infeasibility otherwise). Several studies have been devoted to improving the convergence of column generation algorithms, especially when degeneracy occurs (see, e.g., [DGL14]) or when convergence is too slow (see, e.g., [ADF09]), and to accelerating the convergence of branch-and-price algorithms [DDS11]. Furthermore, our ILP component considers known subsumptions, disjointness, and unsatisfiability of concept conjunctions and uses a different encoding of inequalities that already incorporates the semantics of universal restrictions. We delegate the generation of inequalities completely to the ILP component. To summarize, the novel features of our architecture are (i) saturation rules that do not backtrack to decide subsumption (and disjointness); (ii) feasibility of QCRs is decided by ILP (in contrast to [BMC+ 16]); (iii) our revised encoding of inequalities and the aggregation of information about subsumption, disjointness, and unsatisfiability of concept conjunctions allows a more informed mapping of QCR satisfiability to feasibility and reduces the number of returned solutions that fail logically; (iv) the best-case time complexity of our ILP feasibility test is polynomial to the number of inequalities [Meg87]. In the following sections we present our saturation rules, introduce our ILP approach, sketch soundness, completeness, and termination, present our preliminary evaluation results, and conclude with a summary and future work. 111 2 A Calculus for ELQ The DL ELQ allows the concept-forming constructors u (conjunction), ≤ (at-most restriction), and ≥ (at-least restriction). The semantics of ELQ concepts and roles is defined by an interpretation I = (∆I , ·I ) that maps a concept A ∈ NC (NC is a set of concept names) to AI ⊆ ∆I and a role R ∈ NR (NR is a set of roles) to RI ⊆ ∆I × ∆I . We assume the predefined concepts > and ⊥ with >I = ∆I and ⊥I = ∅. ELQ concepts are inductively defined from the sets NC and NR using the constructors as follows (n, m ∈ N, n ≥ 1, k · k denotes set cardinality, F R,C (x) = {y ∈ C I | (x, y) ∈ RI }): (i) (C u D)I = C I ∩ DI ; (ii) (≥ n R.C)I = {x | kF C,R (x)k ≥ n}; (iii) (≤ m R.C)I = {x | kF C,R (x)k ≤ m}. The latter two constructors are called QCRs. A concept C is satisfiable if there exists an I such that C I 6= ∅. An ELQ Tbox T is defined as a finite set of axioms of the form C v D and such an axiom is satisfied by I if C I ⊆ DI . We call I a model of T if it satisfies all axioms in T . We use CAT to denote the set that contains > Q and all concept names used in T , C¬A A T = {¬A | A ∈ CT \ {>}}, CT to denote the set that contains all QCRs (and A ¬A Q their negation) used in T , and define CT = CT ∪ CT ∪ CT . We use RT to denote the set of roles used in T . A Tbox T is normalized if all axioms are of the form A1 v B, A1 v ./ n R.A2 , ./ n R.A1 v B, A1 u A2 v B, with B ∈ CAT ∪ {⊥}, A1 , A2 ∈ CAT , and ./ ∈ {≥, ≤}. It is easy to see that this can be done in polynomial time following the normalizations described in [BBL05, Kaz09, SMH14]. A normalized Tbox is always in negation normal form because it does not allow the occurrence of negation. Some of our saturation rules make use of the negation operator ¬˙ which returns the negation normal form for named concepts and QCRs defined as ¬(C) ˙ = ¬C, ¬(¬C) ˙ = C, ¬(≤ ˙ m R.C) = ≥ m+1 R.C, and ¬(≥ ˙ n R.C) = ≤ n−1 R.C for m ≥ 0, n ≥ 1. We adopted the idea of saturation graphs from [BBL05, SGL14]. Our saturation graphs have been extended to deal with ELQ and delegate numerical reasoning on QCRs to an ILP component. A saturation graph G = (V, E, L, LP , L¬ P ) is a directed graph where V = VP ∪VA ∪VC such that VP , VA , VC are pairwise disjoint. VP = {vA | A ∈ CAT } is the set of predefined nodes, VA = {vS | S ⊆ CAT } the set of anonymous nodes representing role successors, and VC is the set of nodes called QCR clones representing subsumption or disjointness tests based on QCRs. Each node vS ∈ V uniquely represents either an element (S ∈ L(vS )) of CAT or a subset (S ⊆ L(vS )) of CAT ∪ C¬A T . We also call S the initial label of vS . Each v ∈ V is labelled with Q a set of concepts L ⊆ CT ∪ {⊥} and sets of subsumption tuples LP , L¬ A P ⊆ {hp, qi | p ⊆ CT , q ⊆ CT }. Each 0 0 0 edge hv, v i ∈ E is labelled with a set L(v, v ) ⊆ RT where v is called an r-successor (R-successor) of v with r ⊆ L(v, v 0 ) (R ∈ L(v, v 0 )). Given a normalized Tbox T and a corresponding saturation graph G the label set LP (L¬ P ) contains tuples specifying subsumption (disjointness) conditions caused by QCRs. A subsumption tuple of the form hp, qi consists of a set of precondition concepts p ⊆ CAT and a set of QCRs q ⊆ CQ T . Some of the rules that operate on LP and L¬ P make use of special (negated) membership (∼∈ , is new), subset (⊂ ∪) operators, and a map (ϕ) ∼ ), union (∼ operator. We define is new(q, S) = h{>}, {q}i ∼ ∈ / S and add to(Q, S) as S ← S ∼ ∪ {h{>}, {Q}i} if Q is a QCR or S←S∼ ∪ Q if Q is a set of subsumption tuples. Given sets T, T 0 of subsumption tuples, hp, qi ∼ ∈ T is true if there are p0 , q 0 such that hp0 , q 0 i ∈ T , p ⊆ p0 , and 0 0 0 q⊆q;T ⊂ ∼ T is true if ∀t ∈ T ⇒ t ∼ ∈ T holds. {hp1 , s1 i} ∼ ∪ {hp2 , s2 i} is defined as {hp2 , s1 ∪ s2 i} if p1 ⊆ p2 and {hp1 , s1 i, hp2 , s2 i} otherwise. The map operator is defined as ϕ(A, T ) = {hp ∪ {A}, qi | hp, qi ∈ T } with A ∈ CAT . Our saturation rules interface the ILP component via the predicate infeasible(S) which transforms all QCRs in S to a corresponding system of inequalities and returns true if this system is infeasible. Otherwise it returns false. If S contains no QCRs it also returns false. A node v is called numerically satisfiable or feasible, if the set Q ⊆ L(v) of QCRs is feasible. A concept A is called feasible if its node vA is feasible. The number of possible solutions for a feasible node can be huge1 and quite a few solutions might eventually cause logical unsatisfiability. In order to ensure termination and logically constrain the number of possible solutions for a node v as much as possible, the ILP component makes use of concept information derived from a Tbox T and its saturation graph G. For a node v ∈ VP ∪ VA we define Qv = {C | ./ n R.C ∈ L(v)} ∪ {¬D | ≤ 0 R.D ∈ L(v)} as the set of QCR qualifications occurring in L(v). The information aboutSconcept unsatisfiability and subsumption, which is used by the ILP component, is defined by the set unsat S= v∈VP ∪VA unsat v , which contains sets of concepts whose conjunction is unsatisfiable, and the set subs v = v∈VP ∪VA subs v , which contains sets of tuples representing entailed subsumption relationships of the form A v B or A1 u A2 v B. unsat v = {{A} | A ∈ Qv , ⊥ ∈ L(vA )} ∪ {q | q ⊆ Qv , ⊥ ∈ L(vq ), vq ∈ VA } ∪ {{Ai , Aj } | ¬Ai ∈ L(vAj ), {Ai , Aj } ∩ Qv 6= ∅, i, j ∈ 1..2, i 6= j} 1 In [FH10c, Sec. 4.1.1] it was shown that if a node label contains p (q) QCRs of the form ≥ n R .C (≤ m R0 .C 0 ), then 2qN i i i j j j cases/solutions can exist with N = pi=1 ni . P 112 subs v = {h{A1 , A2 }, Bi | {A1 , A2 } ⊆ Qv , C1 u C2 v D ∈ T , Ci ∈ L(vAi ), B ∈ L(vD ), i ∈ 1..2} ∪ {h{A}, Bi | B ∈ L(vA ), A ∈ Qv } In case a node v is numerically satisfiable, the set σ(v) contains solutions for feasible inequality systems denoted by the QCRs in L(v). A QCR solution is described by a set of tuples of the form hr, q, ni with r ⊆ RT and q ⊆ CAT ∪ C¬AT sets of roles and concepts respectively, and n denotes the cardinality of the set of r-successors that are instances of all concepts contained in q. A saturation graph G is initialized with representative nodes for all concepts in CAT . For instance, for a concept A a node vA is created with L(vA ) = {>, A} and LP (vA ) = L¬ P (vA ) = ∅. The saturation rules are applied to an initialized saturation graph until no rule is applicable anymore. Only the vP4 -Rule and v¬ P4 -Rule with v ∈ VC can be applied to a node v if ⊥ ∈ L(v). This algorithm computes the named subsumers for all predefined nodes and, thus, decides satisfiability and subsumption for all concepts in CAT . A concept A is satisfiable iff ⊥ ∈ / L(vA ), and A is subsumed by B iff B ∈ L(vA ). The top section of Figure 1 contains five rules. The v-Rule (v¬ -Rule) allows a QCR or named concept on its right-hand (left-hand) side. The v∗ -Rule ensures that L(v) contains all QCRs and (negated) named concepts inherited from its subsumers. The vu -Rule is a standard EL rule complemented by its contrapositive version (v¬ u -Rule). The second section contains two rules that deal with role successors where # denotes the cardinality of an anonymous node. If hr, q, ni ∈ σ(v) the fil-rule and e-rule ensure that an edge r ⊆ L(v, vq ) exists that connects v to an anonymous successor vq with L(vq ) = q and #vq = n, i.e., vq represents n identical r-successors of v. For a node v the ⊥-Rule records clashes by adding ⊥ to L(v). For a node v 0 created by the fil-rule there is no need to propagate ⊥ to its predecessor v because v 0 represents one of possibly many existing QCR solutions for v. If all QCR solutions for v fail, the ILP component eventually determines that v is infeasible and thus unsatisfiable. The fourth section of Figure 1 contains five rules that create and maintain subsumption tuples. Only three ¬ of these rules (P./ -Rule, P./ -Rule, Pu -Rule) derive tuples from axioms. The other two rules propagate tuples up ¬ (vP -Rule) or down (vP -Rule) the subsumption hierarchy. The bottom section of Figure S 1 lists rules that discover subsumptions or disjointness due to subsumption tuples. Q(v, S) is defined as hp,qi∈S {q | p ⊆ L(v)} and contains applicable QCRs selected from the set S of subsumption tuples. The relation clone ⊆ V × (CAT ∪ CT¬A ) × V keeps track of subsumption or disjointness tests and their associated QCR clones. For instance, a QCR clone v 0 ∈ VC of vA contains all QCRs contained in L(vA ) and LP (vB ) (L¬ 0 P (vB )) and represents the test whether A is subsumed by (disjoint to) B. If v becomes unsatisfiable, then B (¬B) is added to L(vA ). The vP1 -Rule creates necessary QCR clones, the vP2 -Rule (vP3 - Rule) ensures that Q(vA , LP (vB )) (L(vA ) ∩ CQ 0 T ) is contained in L(v ). The vP4 -Rule adds B to L(vA ) if vA ’s corresponding clone is unsatisfiable. The other four rules deal with disjointness in an analogous way. 3 Small Tbox Example Illustrating Rule Application We demonstrate our calculus with a small ALCQ Tbox T which entails C v D1 u ¬D2 (see below). A slightly different example (C-SAT-exp-ELQ) is also used in our synthetic benchmark (see Section 6) and surprisingly none of the tested reasoners besides Avalanche and Racer can classify the version with n = 10 within a time limit of 1000 seconds. C v ≥ 20 R.> u ≤ 10 R.A u ≤ 10 R.B C v D1 t D2 D1 v ≤ 10 R.¬A, D2 v ≤ 9 R.¬B The following steps show our rewriting of T into T 0 , which is a normalized ELQ Tbox that is a conservative extension of T . 1. We remove the occurrence of t and add the entailment C v D1 t D2 using fresh concepts X3 , X4 and a fresh role S1 . C v ≥ 20 R.> u ≤ 10 R.A u ≤o10 R.B C u ≥ 1 S1 .(X3 u X4 ) v D1 These two axioms entail C v D1 t D2 C u ≥ 2 S1 .> v D2 D1 v ≤ 10 R.¬A D2 v ≤ 9 R.¬B 2. We normalize the axioms (but allow a conjunction on the right-hand side for sake of brevity) and replace ¬A, ¬B by notA, notB and new axioms using fresh roles S2 , S3 such that ¬notA v A and ¬notB v B are 113 v-Rule if A v φ ∈ T , φ ∈ / L(vA ) then add φ to L(vA ) v¬ -Rule if φ v A ∈ T , ¬A ∈ L(v), ¬φ ˙ ∈ / L(v) then add ¬φ ˙ to L(v) v∗ -Rule if A ∈ L(v), τ ∈ L(vA ), τ ∈ / L(v) then add τ to L(v) vu -Rule if A1 u A2 v B ∈ T , {A1 , A2 } ⊆ L(v), B ∈ / L(v) then add B to L(v) v¬ u -Rule if Ai u Aj v B ∈ T , {¬B, Ai } ⊆ L(v), ¬Aj ∈ / L(v) then add ¬Aj to L(v) fil-Rule if hr, q, ni ∈ σ(v), ¬∃ vq ∈ V : q ⊆ L(vq ), #vq ≥ n then create vq ∈ VA with L(vq ) ← q and #vq ← n e-Rule if hr, q, ni ∈ σ(v), q ⊆ L(vq ), #vq ≥ n, r * L(v, vq ) then add r to L(v, vq ) ⊥-Rule if ⊥ ∈ / L(v) ∧ (infeasible(L(v)) ∨ {A, ¬A} ⊆ L(v)) then add ⊥ to L(v) P./ -Rule if ./ n R.A v B ∈ T , is new(¬(./ ˙ n R.A), LP (vB )) then add to(¬(./˙ n R.A), LP (vB )) ¬ P./ -Rule if A v ./ n R.B ∈ T , is new(./ n R.B, L¬ P (vB )) then add to(./ n R.B, L¬ P (v B )) P -Rule if B ∈ L(vA ), LP (vA ) 6⊂ ∼ LP (vB ) then add to(LP (vA ), LP (vB )) P ¬ -Rule if B ∈ L(vA ), L¬ 6⊂ ¬ P (vB ) ∼ LP (vA ) then add to(LP (vB ), L¬ ¬ P (vA )) Pu -Rule if Ai u Aj v B ∈ T , ϕ(Ai , LP (vAj )) 6⊂ ∼ LP (vB ) then add to(ϕ(Ai , LP (vAj )), LP (vB )) vP1 -Rule if Q(v, LP (vB )) 6= ∅, {B, ¬B} ∩ L(v) = ∅, clone(v, B) = ∅ then create v 0 ∈ VC , L(v 0 ) ← {>}, clone(v, B) ← {v 0 } vP2 -Rule if v 0 ∈ clone(v, B), {B, ¬B} ∩ L(v) = ∅, Q(v, LP (vB )) * L(v 0 ) then add to(Q(v, LP (vB )), L(v 0 )) vP3 -Rule if v 0 ∈ clone(v, B), {B, ¬B} ∩ L(v) = ∅, L(v) ∩ CQ 0 T * L(v ) ∩ CT Q Q 0 then add to(L(v) ∩ C , L(v )) vP4 -Rule if {B, ¬B} ∩ L(v) = ∅, v 0 ∈ clone(v, B), ⊥ ∈ L(v 0 ) then add B to L(v) v¬ P1 -Rule if Q(v, L¬ P (vB )) 6= ∅, {B, ¬B} ∩ L(v) = ∅, clone(v, ¬B) = ∅ then create v 0 ∈ VC , L(v 0 ) ← {>}, clone(v, ¬B) ← {v 0 } v¬ P2 -Rule if v 0 ∈ clone(v, ¬B), {B, ¬B} ∩ L(v) = ∅, Q(v, L¬ 0 P (vB )) * L(v ) ¬ 0 then add to(Q(v, LP (vB )), L(v )) v¬ P3 -Rule if v 0 ∈ clone(v, ¬B), {B, ¬B} ∩ L(v) = ∅, L(v) ∩ CQ 0 T * L(v ) ∩ CT Q then add to(L(v) ∩ CQ , L(v 0 )) vP4¬ -Rule if {B, ¬B} ∩ L(v) = ∅, v 0 ∈ clone(v, ¬B), ⊥ ∈ L(v 0 ) then add ¬B to L(v) Figure 1: Saturation rules (φ ∈ CAT ∪ CQ T , τ ∈ CT ; ./ ∈ {≥, ≤}; i, j ∈ 1..2, i 6= j) 114 entailed. This Tbox T 0 additionally entails C v X5 u ¬X7 . C v ≥ 20 R.> u ≤ 10 R.A u ≤ 10 R.B C u X5 v D1 ≥ 1 S1 .X6 v X5 X3 u X4 v X6 C u X7 v D2 ≥ 2 S1 .> v X7 D1 v ≤ 10 R.notA D2 v ≤ 9 R.notB ≤ 1 S2 .> v notA o These two axioms entail ¬notA v A ≥ 1 S2 .> v A ≤ 1 S3 .> v notB o These two axioms entail ¬notB v B ≥ 1 S3 .> v B 3. Known subsumptions or unsatisfiability of concept conjunctions are derived from T 0 . subs = {h{C, X5 }, D1 i, h{C, X7 }, D2 i, h{X3 , X4 }, X6 i} unsat = ∅ ¬ 4. After applying the rules v, P./ , P./ , Pu we get the following node labels (for sake of better readability we denote vA , where A is a concept name, simply as A when used for the labels L, LP , L¬ P ; anonymous and clone nodes are denoted as vai and vcj respectively). L(C) = {>, C, ≥ 1 S1 .X3 , ≥ 1 S1 .X4 , ≥ 20 R.>, ≤ 10 R.A, ≤ 10 R.B} σ(C) = {h{R}, {¬A, ¬B, ¬notB }, 20i, h{S1 }, {X3 , X4 , X6 }, 1i} L¬P (C) = {h{>}, {≥ 1 S1 .X3 }i, h{>}, {≥ 1 S1 .X4 }i, h{>}, {≥ 20 R.>}i, h{>}, {≤ 10 R.A}i, h{>}, {≤ 10 R.B}i} L(D1 ) = {>, D1 , ≤ 10 R.notA} L¬P (D1 ) = {h{>}, {≤ 10 R.notA}i} LP (D1 ) = {h{>, C}, {≤ 0 S1 .X6 }i L(D2 ) = {>, D2 , ≤ 9 R.notB } L¬P (D2 ) = {h{>}, {≤ 9 R.notB }i} LP (D2 ) = {h{>, C}, {≤ 1 S1 .>}i LP (X5 ) = {h{>}, {≤ 0 S1 .X6 }i} LP (X7 ) = {h{>}, {≤ 1 S1 .>}i} LP (notA) = {h{>}, {≥ 2 S2 .>}i} LP (A) = {h{>}, {≤ 0 S2 .>}i} LP (notB ) = {h{>}, {≥ 2 S3 .>}i} LP (B) = {h{>}, {≤ 0 S3 .>}i} 5. After applying the rules v¬ ¬ ¬ P1 , vP2 , vP3 (is C disjoint to D2 ?) and creating the clone vc1 clone(C, ¬D2 ) ← vc1 L(vc1 ) = {>, ≥ 1 S1 .X3 , ≥ 1 S1 .X4 , ≥ 20 R.>, ≤ 10 R.A, ≤ 10 R.B, ≤ 9 R.notB } 6. After applying the fil- and e-rule for vc1 and the rules v¬ , ⊥ for va1 σ(vc1 ) = {h{R}, {¬A, ¬B, ¬notB }, 20i, h{S1 }, {X3 , X4 , X6 }, 1i} L(vc1 , va1 ) = {R} L(va1 ) = {>, ¬A, ¬B, ¬notB , ≤ 0 S2 .>, ≤ 0 S3 .>, ≥ 2 S3 .>, ⊥}, #va2 = 20 L(vc1 , va2 ) = {S1 } L(va2 ) = {>, X3 , X4 , X6 }, #va2 = 1 Based on the unsatisfiability of va1 we add {¬A, ¬B, ¬notB } to unsat. 7. After applying the fil- and e-rule for vc1 again, the rules v¬ , ⊥ for va3 σ(vc1 ) = {h{R}, {¬A, ¬B, notB }, 9i, h{R}, {¬A, B, ¬notB }, 1i, h{R}, {A, ¬B, ¬notB }, 10i, h{S1 }, {X3 , X4 , X6 }, 1i} L(vc1 , va3 ) = {R} L(va3 ) = {>, ¬A, ¬B, notB , ≤ 0 S2 .>, ≤ 0 S3 .>}, #va3 = 9 L(vc1 , va4 ) = {R} L(va4 ) = {>, ¬A, B, ¬notB , ≤ 0 S2 .>, notA, ≥ 2 S3 .>}, #va4 = 1 115 L(vc1 , va5 ) = {R} L(va5 ) = {>, A, ¬B, ¬notB , ≤ 0 S3 .>, notB , ⊥}, #va2 = 10 Based on the unsatisfiability of va5 we add {A, ¬B, ¬notB } to unsat. Together with the previous addition to unsat we learned that {¬B, ¬notB } is unsatisfiable. 8. The ⊥-rule adds ⊥ to L(vc1 ) because infeasible(L(vc1 )) is true due to {¬B, ¬notB } ∈ unsat. 9. The v¬ P4 -rule adds ¬D2 to L(C). 10. The rules v¬ ¬ u and v add ¬X7 and ≤ 1 S1 .> to L(C). 11. After applying the rules vP1 , vP2 , vP3 (is C subsumed by X5 ?) and creating the clone vc2 clone(C, X5 ) ← vc2 L(vc2 ) = {>, ≥ 1 S1 .X3 , ≥ 1 S1 .X4 , ≥ 20 R.>, ≤ 10 R.A, ≤ 10 R.B, ≤ 1 S1 .>, ≤ 0 S1 .X6 } 12. The ⊥-rule adds ⊥ to L(vc2 ) because infeasible(L(vc2 )) is true due to role S1 . 13. The vP4 -rule adds X5 to L(C). 14. The vu -rule adds D1 to L(C). Other rules are still applicable but for sake of brevity we do not illustrate their application. Furthermore, no other concept subsumptions are entailed w.r.t. T . 4 ILP Component We now present the large-scale optimization framework we have designed for solving the system of QCRs in the DL ELQ. It is based on a decomposition technique, called DantzigWolfe decomposition or more commonly column generation technique [Las70, Chv83], combined with a branch-and-price technique [BJN+ 98] in order to either detect that the system is infeasible, or to compute an optimal solution of the system. Given T , v ∈ V and S containing QCRs, define the qualifying role set of v as SQ = {α(./ nR.C) | ./ nR.C ∈ S} ∪ {C | ./ nR.C ∈ S} ∪ {>, ⊥}, where α defines a mapping between a QCR and its associated (proxy) subrole of R that is new in T , e.g., α(./ nR.C) = R0 with R0 v R and R0 new in T . The role partitioning PSQ of a qualifying role set SQ is defined as the power set of SQ (without the empty set). Note that a qualifying concept can be a member of a partition at least one role. For each partition p ∈ PSQ , S only if the partition also containsT we define pI = fil (v, p) ∩ (∆I \ Y ∈SQ \p fil (v, Y )) where fil (v, p) = e∈p fil (v, e) and fil (v, e) = eI if e is a concept and fil (v, e) = {y I | (v I , y I ) ∈ eI } if e is a role. The semantics of role partitions in PSQ is defined in such a way that their interpretations are pairwise disjoint. The absence of a role or concept in a partition implies the presence of its semantic negation. We now define a mapping ξ from S to a linear inequality system as follows: - ξ(≥ nR.C) = { q∈PS |R0 ∈q xq ≥ n} with R0 = α(≥ nR.C), P Q - ξ(≤ nR.D) = { q∈PS |R00 ∈q xq ≤ n} ∪ q∈Q {xq ≤ 0}, such that Q = {p ∈ PSQ | D ∈ p ∧ R00 ∈ P S / p}, with Q R00 = α(≤ nR.D). S In order to determine whether ξ(S) = ./nR.C∈S ξ(./ nR.C) is feasible using a highly scalable solution, we propose a column generation ILP formulation for expressing ξ(S) as a mathematical ILP model, which will be solved using a branch-and-price algorithm [BJN+ 98]. Given T , v ∈ V , S, SQ and PSQ , the ILP model associated with the feasibility problem of ξ(S) can be written as follows: X min costp xp (1) p∈PSQ X 0 ≥role subject to: aR p xp ≥ δ R 0 R0 ∈ SQ (2) p∈PSQ X 0 ≤role aR p xp ≤ δ̄R0 R0 ∈ SQ (3) p∈PSQ xp ∈ Z+ p ∈ PSQ , (4) 116 ≥role ≤role ≥role ≤role where SQ = {α(≥ nR.C) | ≥ nR.C ∈ S}, SQ = {α(≤ nR.C) | ≤ nR.C ∈ S}, SQ role = SQ ∪ SQ , δ R0 (δ̄R0 ) is the cardinality of an at-least (at-most) restriction on a subrole R0 ∈ SQ role , and xp represents a partition of the set PSQ . costp is defined as the number of concepts in partition p. When the set of inequalities has a non empty solution set, we are interested in partitions that only contain the entailed concepts, i.e., the minimum number of concepts that are needed to satisfy all the axioms. Consequently, in the objective, costp ensures that output partitions only contain the entailed concepts, i.e., the minimum number of concepts that are needed to satisfy all the axioms. In order to design a scalable solution of (1)-(4), which has an exponential number of variables, we consider a solution scheme that makes use of an implicit representation of the constraint matrix. This corresponds to using a branch-and-price method, a generalization of a branch-and-bound method [NW88] in which the linear relaxation of (1)-(4) is solved with a column generation algorithm ([Las70], [Chv83]). The linear relaxation is defined by (1)-(3) and constraint (40 ), which is written as follows: x p ∈ R+ p ∈ PSQ . (40 ) Next step is to use an implicit representation of all the variables of (1)-(40 ). Therefore, instead of defining the variables for p ∈ PSQ , we do it for p ∈ PS0 Q ⊆ PSQ , leading to the so-called restricted ILP or restricted master problem in the mathematical programming literature, in which constraints (40 ) are replaced by constraints x p ∈ R+ p ∈ PS0 Q , (400 ) with PS0 Q = ∅ at the outset. We next have an iteration solution process in which, at each iteration, the column generation algorithm tries to generate an improving partition p, i.e., a partition such that, if added to the current PS0 Q , improves the objective of formulation (1)-(400 ). The partition generator (PG), also called pricing problem in the mathematical programming literature, is a mathematical ILP model with two sets of decision variables: 0 aR = 1 if role R0 is in the generated partition, 0 otherwise ; bC = 1 if concept C ∈ SQ concept is in the generated concept partition, 0 otherwise, where SQ containing all the concepts of SQ and no subrole. The (PG) model can be stated as: X X 0 0 X 0 0 (PG) min bC − aR π̂ R − aR ω̂ R (5) concept C∈SQ ≥role ≤role R0 ∈SQ R0 ∈SQ 0 ≥role subject to: aR ≤ bC R0 ∈ SQ , C = R0 .qualif ier (6) 0 ≤role bC ≤ aR R0 ∈ SQ , C = R0 .qualif ier (7) concept bC ≤ b> C ∈ SQ (8) b⊥ = 0 (9) 0 bC , aR ∈ {0, 1} R0 ∈ SQ role concept , C ∈ SQ role = SQ \ SQ , (10) 0 0 where π̂ R and ω̂ R are the optimal values of the dual variables of problem (1)-(400 ) (see [Chv83] if not familiar with linear programming concepts). The objective function (5) is the so-called reduced cost of a partition (or column, see again [Chv83] for more details on the column generation method). Constraints (6)-(10) implement the semantics of ξ(S). (PG) returns a valid partition of PSQ , assuming no other information is provided. In its feasibility space, it contains a 1-to-1 mapping between the said partitions and algebraic inequalities. If other informations such as: (i) subsumption (T |= A v B), (ii) binary subsumption (A u B v C) and (iii) disjointness (T |= A1 u · · · u An v ⊥, n ≥ 1) are provided, the cardinality of some partitions p ∈ PSQ might need to be 0. Depending on the information received, the semantics can be implemented by (in)equalities, using a 1-to-1 mapping presented below. - For every T |= A v B, set SQ concept = SQconcept ∪ {A, B} and add bA ≤ bB to (PG), in order to guarantee that if a generated partition contains a certain concept, it does contain all its subsumers. - For every T |= A u B v C, update SQ concept concept = SQ ∪ {A, B, C} and add bA + bB − 1 ≤ bC to (PG). Then, if (PG) generates a partition containing A and B, it must contain C as well. - For every disjointness relation T |= A1 u · · · u An v ⊥, n ≥ 1, set SQ concept concept = SQ ∪ {A1 , . . . , An } and Pn add i=1 bAi − n + 1 ≤ b⊥ to (PG). This inequality ensures that if all the concepts Ai , i = 1, . . . , n are present in a partition; this partition cannot be generated since otherwise it would contain ⊥ as well. 117 Figure 2: Overview of ILP solution process - If there is some concept C with ¬C ∈ SQ concept , the relationship of C and ¬C can be modelled with equality bC + b¬C = 1. This implies that every generated partition contains exactly one of C and ¬C. Every partition generated by (PG), which possibly contains some of the above inequalities or equalities, satisfies all the input axioms except the QCRs, which are taken care of in (1)-(400 ). The column generation method is an iterative process in which (1)-(400 ) and (PG) are alternatively solved until (PG) cannot provide any new improving partitions, i.e., when the optimal value of the objective of (PG) is positive. This corresponds to one of the optimality conditions when solving a linear program, see, e.g., [Chv83] for more details. In the branch-and-price algorithm, an implicit enumeration scheme with a breadth first search (BFS) explo- ration strategy, branching is done upon a subrole R0∗ selected as follows:   X 0  R0∗ = arg 0max aR p × max {x̂ p − bx̂ p c, dx̂ p e − x̂ p } , (11) R ∈SQrole  0  p∈P 0∗ 0∗ leading to two branches, one with aR = 0 and the other one with aR = 1. This branching scheme is clearly exhaustive and valid (see [Van11] and [NW88]). The branch-and-price algorithm terminates when either an integer feasible solution for (1)-(4) is found, or an infeasibility is detected, i.e., either the linear programming relaxation (1)-(400 ) has no solution (in most of the infeasibility cases) or the branch-and-price algorithm fails to find a feasible integer solution, see [NW99]. A flowchart is provided in Figure 2 to summarize the solution process. Soundness and Completeness The mapping presented in the previous paragraphs is a one-to-one mapping between the axioms and the algebraic inequalities. Thus, the feasibility space defined by (2)-(4) represents all the instances that satisfy all axioms. Following the decomposition ILP model that is proposed, constraints related to satisfying QCRs are addressed in (2)-(4), while all other axioms are embedded in (PG). The branch-and-price algorithm, if (1)-(4) is feasible, returns one set of valid partitions, and the selection of them is made by the objective (1). 118 The result of the proposed solution process is sound. Indeed, every model produced by the large-scale opti- mization framework, i.e., ILP model (1)-(4) and branch-and-price algorithm, satisfies all the axioms that are fed to the ILP component. It is also complete, because the feasibility spaces of the (1)-(400 ) and (PG) consider all the possible models through the one-to-one mapping that leads to ILP model (1)-(4). In addition, the branching rule in the branch-and-price algorithm considers a partitioning of the overall solution space, therefore no solution is left out. 5 Soundness and Completeness Due to lack of space we can only sketch the soundness and completeness proofs for our saturation rules. Given the presentation in the previous section we know that the algorithms implementing the ILP component are sound and complete and terminate in finite time for deciding whether a set of QCRs is feasible, i.e., numerically satisfiable. Intuitively speaking our soundness proof is an extension of the one for EL but all subsumptions or disjointness involving QCRs are based on QCR infeasibility tests performed by the ILP component. Once a subsumption or disjointness has been proven, its evidence as an element of a node label becomes part of the saturation graph. Since QCRs can interact with one another a QCR solution and its corresponding model is not proof enough for a subsumption unless it is known to be the only possible solution. In order to test QCR-based entailment the label sets LP and L¬P of potential (non-)subsumer nodes together with node labels are used for a feasibility test. If such a set of QCRs has been proven to be infeasible, the corresponding subsumption or disjointness can be added to the graph. Thus, only entailed subsumptions or disjointness will be inferred. Lemma (Soundness). Let G be the saturation graph for a normalized Tbox T after the application of all satu- ration rules in Figure 1 has terminated and C ∈ CAT and D ∈ CAT ∪ {⊥}, β ∈ {D, ¬D}. ˙ Then T |= C v β if it holds that β ∈ L(vC ). Proof. Let us assume that each rule application creates a new saturation graph and the sequence of rule applica- ¬ R,C I I S G1 , . . . , Gm with Gi = (Vi , Ei , Li , LP i LP i ) and i ∈ 1..m. Let tions until termination produce a sequence of graphs F (x) = {y ∈ C | (x, y) ∈ R }, and Q(v, S) = hp,qi∈S {q | p ⊆ L(v)}. For all m ∈ N, models I of T , r ⊆ RT , and x ∈ C I we claim the following holds: (i) if β ∈ Lm (vC ) then T |= C v β; (ii) if r ⊆ Lm (vC , vq ), #vq ≥ n I then there exist yi ∈ ∆I with (x, yi ) ∈ R∈r RI , yi ∈ q0 ∈q q 0 , i ∈ 1..n. T T We prove our claim by induction on m. We start with m = 0 and assume that I is a model for T . For G0 we have L0 (vC ) = {>, C}, L0 (vC , vD ) = ∅ implying that D = C. It is trivial to see that our claim holds. For the induction step we make a case distinction according to applicable rules. v-Rule Let φ ∈ Lm (vC ) \ Lm−1 (vC ) and x ∈ C I . Then there exists C ∈ Lm−1 (vC ) and C v φ ∈ T . Since I a model of T it holds x ∈ φI . v¬ -Rule Let ¬φ ˙ ∈ Lm (v) \ Lm−1 (v) and x ∈ ∆I \ C I . Then there exists ¬C ∈ Lm−1 (vC ) and φ v C ∈ T . Since I a model of T it holds x ∈ ∆I \ φI . v∗ -Rule Let τ ∈ Lm (v) \ Lm−1 (v) and x ∈ C I . Then there exists τ ∈ Lm−1 (vC ) and C I ⊆ τ I . Since I a model of T it holds x ∈ τ I . vu -Rule Let D ∈ Lm (v) \ Lm−1 (v) and x ∈ C1I , x ∈ C2I . Then there exists C1 , C2 ∈ Lm−1 (v) and C1 u C2 v D ∈ T . Since I a model of T it holds x ∈ C1I ∩ C2I and thus x ∈ DI . v¬ I I I u -Rule Let ¬Cj ∈ Lm (v) \ Lm−1 (v) and x ∈ ∆ \ D , x ∈ Ci . Then there exists ¬D, Ci ∈ Lm−1 (v) and Ci u Cj v D ∈ T . Since I a model of T it holds x ∈ Ci ∪ (∆I \ CjI ) ∪ (∆I \ DI ) and thus x ∈ ∆I \ CjI . I fil-Rule, e-Rule Let vq ∈ Vm \ Vm−1 , r ⊆ Lm (vC , vq ) such that q ⊆ Lm (vq ) and #vq ≥ n, Q = Lm−1 (vC ) ∩ CQ T, I and let x ∈ q0 ∈Q q 0 . Due to the soundness and completeness of the ILP component and since I is T a model of T , w.l.o.g. we can assume that that a solution hr, q, ni ∈ σ(vC ) exists and we have yi with I (x, yi ) ∈ R∈r RI , yi ∈ q0 ∈q q 0 with i ∈ 1..n, and it holds ∀q 0 ∈ Q : x ∈ q 0I . T T I I I ⊥-Rule Let ⊥ ∈ Lm (vC ) \ Lm−1 (vC ), then either {A, ¬A} ⊆ Lm−1 (vT C ) and x ∈ A , x ∈ ∆ \ A or I infeasible(Lm−1 (vC )) and by the soundness of the ILP component x ∈ q∈Lm−1 (vC )∩CQ q . In both cases it T holds that x ∈ ⊥I . 119 P./ -Rule Let h{>}, {¬(./ ˙ n R.C)}i ∈ LP m (vD ) \ LP m−1 (vD ). The newly created tuple is correct. Assume for a node vF that ./ m R.E ∈ Lm−1 (vF ) and x ∈ F I . If the ILP component determines {./ m R.E, ¬(./ ˙ n R.C)} as infeasible, then it holds x ∈ (./ m R.E)I , (./ m R.E)I ⊆ (./ n R.C)I ⊆ DI because I is a model of T and ./ n R.C v D ∈ T . ¬ P./ -Rule Let h{>}, {./ n R.C}i ∈ LP m (vD ) \ LP m−1 (vD ). The newly created tuple is correct. Assume for a node vF it holds ./ m R.E ∈ Lm−1 (vF ) and x ∈ F I . If the ILP component determines the set {./ m R.E, ./ n R.C} as infeasible, then x ∈ (./ m R.E)I , ./ m R.E I ⊆ ∆I \ (./ n R.C)I ⊆ ∆I \ DI because I is a model of T and D v ./ n R.C ∈ T . P -Rule Let hp, qi ∈ LP m (vD ) \ LP m−1 (vD ), C I ⊆ DI , and w.l.o.g. let hp, qi ∈ LP m−1 (vC ). The newly created tuple is correct because I is a model of T and a subsumption condition for C is also one for D since x ∈ C I implies x ∈ DI . P ¬ -Rule Let hp, qi ∈ L¬ ¬ I I P m (vC ) \ LP m−1 (vC ), C ⊆ D , and w.l.o.g. let hp, qi ∈ LP m−1 (vD ). The newly created tuple is correct because I is a model of T and a subsumption condition for ¬D is also one for ¬C since x ∈ ∆I \ DI implies x ∈ ∆I \ C I . Pu -Rule Let hp ∪ {Ci }, qi ∈ LP m (vD ) \ LP m−1 (vD ), and w.l.o.g. let hp, qi ∈ LP m−1 (vCj ). The newly created tuple is correct because I is a model of T , Ci u Cj v D ∈ T , and if CiI ⊆ DI then a subsumption condition for Cj is also one for D. Rules vP1 , vP2 , vP3 , vP4 Let ⊥ ∈ Lm (v 0 ) \ Lm−1 (v 0 ), v 0 ∈ clone(vC , D), x ∈ C I . The rule vP1 added v 0 to Vk1 , the rules vP2 , vP3 fired T at least once and added the corresponding QCRs to Lk2 (v 0 ) with k1 < k2 ≤ m−1. We I I I define QP (v) = ∆ \ q∈Q(v,LP (vD )) q as the domain complement of all QCRs contained in Q(v, LPm (vD )) m and QI (v) = q∈Lm (v)∩ CQ q I as the domain of all QCRs contained in Lm (v). W.l.o.g. we only consider the T T case that infeasible(L(v 0 )) caused the unsatisfiability of v 0 . Due to the composition of Lm (v 0 ) and since I is a model of T , it holds x ∈ QI (vC ), QI (vC ) ⊆ QIP (vC ) ⊆ DI . The rules v¬ ¬ ¬ ¬ P1 , vP2 , vP3 , vP4 are analogous to vP1 , vP2 , vP3 , vP4 and for lack of space we omit this part of the soundness proof here. Lemma (Completeness). Let G be the saturation graph for a normalized Tbox T after the application of all saturation rules in Figure 1 has terminated, and let A ∈ CAT , B ∈ CAT ∪ {⊥}, and β ∈ {B, ¬B}. ˙ Then, β ∈ L(vA ), if T |= A v β. Proof. We show the contrapositive. We assume that if D ∈ / L(vC ), then T |= C 6v D. In the following we show that a model for C 6v D can be derived from the saturation graph G, i.e., by constructing a canonical model I(C) w.r.t. T such that x ∈ C I \ DI . I(C) is defined iteratively starting with I(C0 ). We define ∆I0 (C) := {xC } and DI0 (C) := {xC | D = C} for all D ∈ CAT . v-Rule In case φ = D then for every x ∈ (∆Ii ∩ C Ii ) \ DIi+1 add x to DIi+1 . In case φ = ./ n R.C the model construction is done in the fil- and e-Rule. v¬ -Rule In case φ = D then for every x ∈ (∆Ii \ C Ii ) \ (∆Ii+1 \ DIi+1 ) add x to ∆Ii+1 \ DIi+1 . In case φ = ./ n R.C the model construction is done in the fil- and e-Rule item below. v∗ -Rule This rule has no impact on the model construction. vu -Rule For every x ∈ (∆Ii ∩ C1Ii ∩ C2Ii ) \ DIi add x to DIi+1 . v¬u -Rule For every x ∈ (∆ Ik ∩ CiIk ) \ (CjIk ∪ DIk ) add x to DIk+1 (i, j ∈ 1..2, i 6= j). I fil-Rule, e-Rule Let rIi = R∈r RIi , q Ii = q0 ∈q q 0 i , and k ∈ 1..n. For every x ∈ ∆Ii ∩ C Ii where no tuples T T I (x, yk ) ∈ rIi+1 with yk ∈ q Ii+1 exist, introduce new individuals yk to ∆Ii+1 , for every q 0 ∈ q add yk to q 0 i+1 , and add (x, yk ) to RIi+1 for every R ∈ r. Rules vP1 , vP2 , vP3 , vP4 Let QIPi = q∈Q(v,LP (vF )) q Ii , QIPi¬ = ∆Ii \ QIPi , QIv i = q∈Lv ∩ CQ q Ii , E, F ∈ CAT , T T E T and x ∈ E Ii . By the composition rules for LP and the infeasibility result of the ILP component we know that E Ii ⊆ QIPi¬ ⊆ F Ii because E Ii ∩ QIPi = ∅. Now for every x ∈ (∆Ii ∩ E Ii ) \ F Ii+1 add x to F Ii+1 . 120 The rules v¬ ¬ ¬ ¬ P1 , vP2 , vP3 , vP4 are analogous to vP1 , vP2 , vP3 , vP4 and for lack of space we omit this part of the completeness proof here. The construction of a model is performed in a fair manner, i.e., every rule applicable to already existing elements in ∆Ii is applied before applying rules to new elements. The constructed model I(C) is indeed a model of C w.r.t T . Due to lack of space we cannot prove this in detail but we argue informally. Although our rules deal with ELQ, a subset of these deal with EL if one assumes that only QCRs of the form ≥ 1R.C are allowed. Thus, we claim that our rules are complete for EL. Due to the semantics of QCRs and their allowed occurrence on the left- and and right-hand side of axioms, these can entail subsumptions that are not possible in EL. In order to ensure completeness we introduced the labels LP and L¬ P that aggregate possible (non-)subsumption conditions caused by QCRs. In order to prove subsumption or disjointness we create corresponding QCR clones. In case a clone is satisfiable after all rules have terminated this clone can serve as a model for the non-subsumption or non-disjointness. In case additional entailed information is added to the saturation graph that causes the unsatisfiability of a QCR clone, we will add the entailed subsumption or disjointness to the sets subs and unsat that are used by the ILP component. Regarding the fil- and e-rule there could exist another possible incompleteness because a numerically satisfiable set of QCRs could eventually cause the unsatisfiability of a created anonymous node due to entailed information missing in the graph at the time of the feasibility test. However, if such an anonymous node becomes unsatisfiable, the cause of unsatisfiability is learned by adding its cause to the sets subs and unsat. This ensures that a previously computed solution is monotonically constrained until either an anonymous node is determined as satisfiable or the set of QCRs becomes eventually infeasible. Again, this ensures that no model for non-subsumption or non-disjointness is overlooked and no subsumption or disjointness is missed. Lemma (Termination). For every normalized ELQ Tbox over CT and RT the application of the saturation rules in Figure 1 will terminate in finite time. Proof. The algorithm terminates naturally because the saturation graph is finite and its number of nodes is bounded by the size of the power set of CT and RT respectively, cycles are avoided by reusing nodes in accordance to standard subset blocking. Finally, the number of concepts, edges, QCRs, and subsumption tuples that can be added to L, LP , and L¬ P is again bounded by the size of the power set of CT and RT respectively. All rules extend labels monotonically. Once the precondition of a rule is true for elements of a graph G and the rule has fired, it cannot fire again for the same set of elements, thus, any series of rule applications is finite. 6 A First Experimental Evaluation We developed a prototype system called Avalanche that implements our calculus as proof of concept.2 Its ILP component is based on IBM ILOG CPLEX Optimization Studio [IBM] that is freely available for academic research. Avalanche currently parses only ELQ ontologies expressed in RDF/XML syntax. For this first release our focus is on a sound, complete, and terminating implementation. We did not optimize Avalanche for EL ontologies yet and many of our saturation rules are implemented very inefficiently. Deciding subsumption for named concepts where LP and/or L¬ P are not empty is currently computed very naively. We generate a QCR clone for each possible subsumption or disjointness via QCRs and the number of clones is bounded by n2 if the Tbox contains n named concepts. Avalanche has been written in the Java programming language. It consists of two main components: a reasoner and an external ILP module. The ILP module is needed for feasibility testing of QCRs. The reasoner executes in the following way: First, it parses the input ontology file. The axioms in the file must conform to our ELQ syntax. If an axiom in the ontology does not conform to the ELQ syntax restrictions an exception will be raised and the system will terminate. After the parsing is completed, the input axioms are rewritten to our internal normal form. Then, we build nodes representing all concepts declared in the original ontology file as well as the ones obtained during the normalization phase. Our reasoning process is divided into two phases: an unfolding and a rule application phase. During the unfolding phase we apply the rules v, v./ , v¬ ¬ ./ , P , and P . In this phase, each rule is applied only once to each node. Afterwards, during the rule application phase, we apply all rules rules except v, v./ , and v¬ ./ . The rules do not have to be applied in any particular order. We apply all matching rules to all the nodes. The system calls the external ILP module when it needs to solve a system of inequalities. 2 Avalanche web page: https://users.encs.concordia.ca/%7Ehaarslev/Avalanche/ 121 Ontology Name #Axioms #Concepts #Roles #QCRs canadian-parliament-factions-1 48 21 6 19 canadian-parliament-factions-2 56 24 7 25 canadian-parliament-factions-3 64 27 8 30 canadian-parliament-factions-4 72 30 9 35 canadian-parliament-factions-5 81 34 10 40 canadian-parliament-full-factions-1 51 22 6 22 canadian-parliament-full-factions-2 60 25 7 30 canadian-parliament-full-factions-3 69 28 8 36 canadian-parliament-full-factions-4 78 31 9 42 canadian-parliament-full-factions-5 87 34 10 48 C-SAT-exp-ELQ 26 10 4 13 C-UnSAT-exp-ELQ 26 10 4 13 genomic-cds rules-ELQ-fragment-1 716 358 1 357 genomic-cds rules-ELQ-fragment-2 718 359 1 357 Figure 3: Metrics of ELQ benchmark ontologies (#=Number of . . . ) The experiments were performed on a MacBook Pro (2.6 GHz Intel Core i7 processor, 16GB memory) using only one core. The comparison results (average of 3 runs) are shown in Figure 4. We compared Avalanche with major OWL reasoners: FaCT++ (1.6.4) [FaC], HermiT (1.3.8) [Her], Konclude (0.6.2) [Kon], and Racer (3.0) [HM01, HHMW12, Rac], which is the only other available OWL reasoner using an ILP component for reasoning about QCRs. The algorithms implementing Racer’s ILP component are in general best-case exponential to the number of QCRs given for one concept. Some metrics about the benchmark ontologies are shown in Figure 3. The first benchmark (see top part of Figure 4) uses variants of two real-world ontologies modelling a component of the Canadian Parliament, namely the House of Commons, which is a democratically elected body that had 308 members in the last Parliament (most members elected in 2011) [Can]. For each Canadian province a faction is defined [Can] that is composed of members elected in the same province. In order to ensure subsumptions based on QCRs we defined four concepts categorizing factions as tiny, small, medium, or big, based on the number of faction members. Each faction belongs to exactly one of these faction categories. The second version adds a concept defining for the House of Commons the number of members from each province [Can]. The only reasoners that can classify all variants of the simplest of these ontologies within the given time limit are Avalanche and Racer. Avalanche still exhibits an exponential runtime increase but it is the only reasoner that can classify all variants of these ontologies. The performance of Racer for the simpler ontology is a good indication that Avalanche can achieve similar runtimes with optimized reasoning algorithms. The second benchmark (see middle part of Figure 4) uses synthetic concept templates that are similar to the example used in Section 3. The original ALCQ concepts are shown below the table. They were manually rewritten into normalized ELQ as demonstrated in Section 3. The concept templates use a variable n that is increased exponentially. The numbers used in the template are bounded by the value of 2n. The first template is satisfiable and the second one unsatisfiable. Only Avalanche and Racer can classify all variants of these small ontologies within the time limit. The third benchmark (see bottom part of Figure 4) uses two ELQ fragments of a real world ontology, genomic- cds rules [Sam13, Sam14], which was developed for pharmacogenetics and clinical decision support. It contains many concepts using QCRs of the form = 2 has.Ai . However, in these fragments the concepts (Ai ) occurring in the qualification of the QCRs do not interact with one another. This simplifies the reasoning and all reasoners except Racer perform well. Avalanche and HermiT as well as FaCT++ and Konclude have similar runtimes. These fragments are interesting because the concept <#human> contains several hundred QCRs using the same role. This is one of the reasons why Racer timed out for both fragments. 7 Summary We presented the first calculus that combines saturation and ILP-based reasoning to decide subsumption for ELQ. Our preliminary experiments indicate that this calculus offers a better scalability for qualified cardinality restrictions than approaches combining both tableaux and ILP as well as traditional (hyper)tableau methods. We already started to improve the efficiency of our implementation and expect a significant speedup for our next 122 Canadian Parliament Factions only Canadian Parliament Full #F Ava Fac Her Kon Rac Ava Fac Her Kon Rac 5 11.1 TO TO TO 0.12 375 TO TO TO TO 4 8.4 TO TO TO 0.11 22.4 TO TO TO TO 3 2.7 TO TO TO 0.07 4.1 TO TO TO TO 2 1.4 TO TO TO 0.07 2.7 TO TO TO 10.5 1 0.8 TO TO 7.3 0.05 1.1 TO TO TO 0.44 C-SAT-exp-ELQ C-UnSAT-exp-ELQ n Ava Fac Her Kon Rac Ava Fac Her Kon Rac 40 0.69 TO TO TO 0.01 0.63 TO TO TO 0.01 20 0.62 TO TO TO 0.01 0.80 TO TO TO 0.01 10 0.63 TO TO TO 0.01 0.99 TO TO TO 0.01 5 0.72 6.3 4.4 0.91 0.01 0.74 TO TO 784 0.01 3 0.62 0.17 0.18 0.33 0.01 0.75 0.25 1.15 1.18 0.01 Sat: C v (≤ n R.¬A t ≤ n−1 R.¬B) u ≥ 2n R.> u ≤ n R.A u ≤ n R.B Unsat: C v (≤ n−1 R.¬At≤ n−1 R.¬B)u≥ 2n R.>u≤ n R.Au≤ n R.B Satisfiability of concept <#human> Name Ava Fac Her Kon Rac genomic-cds rules-ELQ-fragment-1 1.13 27.7 0.87 27.7 TO genomic-cds rules-ELQ-fragment-2 2.4 28.2 1.14 28.3 TO Figure 4: Benchmark runtimes in seconds with a timeout of 1000 seconds (TO=timeout, #F=Number of Factions, Ava=Avalanche, Fac=FaCT++, Her=HermiT, Kon=Konclude, Rac=Racer) release. We plan to add a preprocessing phase that automatically rewrites ALCQ ontologies to our ELQ syntax. Our next steps are to extend our calculus to cover role hierarchies and inverse roles. References [ADF09] H. M. B. Amor, J. Desrosiers, and A. Frangioni. On the choice of explicit stabilizing terms in column generation. Discrete Applied Mathematics, 157(6):1167–1184, 2009. [BBL05] F. Baader, S. Brandt, and C. Lutz. Pushing the EL envelope. In Proc. of IJCAI, pages 364–369, 2005. [BJN+ 98] C. Barnhart, E. L. Johnson, G. L. Nemhauser, M. W. P. Savelsbergh, and P. H. Vance. Branch-and- price: Column generation for solving huge integer programs. Operations Research, 46(3):316–329, 1998. [BMC+ 16] A. Bate, B. Motik, B. Cuenca Grau, F. Simančı́k, and I. Horrocks. Extending consequence-based reasoning to SRIQ. In Proc. of KR, pages 187–196, 2016. [Can] Canadian Parliament. https://en.wikipedia.org/wiki/House of Commons of Canada. [Chv83] V. Chvatal. Linear Programming. Freeman, 1983. [DDS11] G. Desaulniers, J. Desrosiers, and S. Spoorendonk. Cutting planes for branch-and-price algorithms. Networks, 58:301–310, 2011. [DGL14] J. Desrosiers, J. Gauthier, and M. Lübbecke. Row-reduced column generation for degenerate master problems. European Journal of Operational Research, 236:453–460, July 2014. [DW60] G. B. Dantzig and P. Wolfe. Decomposition principle for linear programs. Operations research, 8(1):101–111, 1960. [FaC] FaCT++. http://owl.cs.manchester.ac.uk/tools/fact/. 123 [FH10a] J. Faddoul and V. Haarslev. Algebraic tableau reasoning for the description logic SHOQ. Journal of Applied Logic, 8(4):334–355, 2010. [FH10b] J. Faddoul and V. Haarslev. Optimizing algebraic tableau reasoning for SHOQ: First experimental results. In Proc. of DL, pages 161–172, 2010. [FH10c] N. Farsiniamarj and V. Haarslev. Practical reasoning with qualified number restrictions: A hybrid Abox calculus for the description logic SHQ. AI Communications, 23(2-3):334–355, 2010. [GG61] P. C. Gilmore and R. E. Gomory. A linear programming approach to the cutting-stock problem. Operations research, 9(6):849–859, 1961. [HB91] B. Hollunder and F. Baader. Qualifying number restrictions in concept languages. In Proc. of KR, pages 335–346, 1991. [Her] HermiT. http://www.hermit-reasoner.com/download.html. [HHMW12] V. Haarslev, K. Hidde, R. Möller, and M. Wessel. The RacerPro knowledge representation and reasoning system. Semantic Web, 3(3):267–277, 2012. [HM01] V. Haarslev and R. Möller. RACER system description. In Proc. of IJCAR, pages 701–705, 2001. [IBM] IBM. https://www.ibm.com/developerworks/downloads/ws/ilogcplex/. [Kaz09] Y. Kazakov. Consequence-driven reasoning for horn SHIQ ontologies. In Proc. of IJCAI, pages 2040–2045, 2009. [Kon] Konclude. http://www.derivo.de/en/produkte/konclude/. [Las70] L. Lasdon. Optimization Theory for Large Systems. MacMillan, New York, 1970. [LD05] M. Lübbecke and J. Desrosiers. Selected topics in column generation. Operations Research, 53:1007– 1023, 2005. [Meg87] N. Megiddo. On the complexity of linear programming. In Advances in Economic Theory, pages 225–268. Cambridge University Press, 1987. [NW88] G. L. Nemhauser and L. A. Wolsey. Integer and Combinatorial Optimization. Wiley, New York, 1988. [NW99] G. Nemhauser and L. Wolsey. Integer and Combinatorial Optimization. Wiley, 1999. reprint of the 1988 edition. [OK99] H. Ohlbach and J. Köhler. Modal logics, description logics and arithmetic reasoning. Artificial Intelligence, 109(1-2):1–31, 1999. [Rac] Racer. https://www.ifis.uni-luebeck.de/index.php?id=385. [RH12] L. Roosta Pour and V. Haarslev. Algebraic reasoning for SHIQ. In Proc. of DL, pages 530–540, 2012. [Sam13] M. Samwald. Genomic CDS: an example of a complex ontology for pharmacogenetics and clinical decision support. In 2nd OWL Reasoner Evaluation Workshop, pages 128–133. CEUR, 2013. [Sam14] M. Samwald. An update on genomic CDS, a complex ontology for pharmacogenomics and clinical decision support. In 3rd OWL Reasoner Evaluation Workshop, pages 58–63. CEUR, 2014. [SGL14] A. Steigmiller, B. Glimm, and T. Liebig. Coupling tableau algorithms for expressive description logics with completion-based saturation procedures. In Proc. of IJCAR, pages 449–463, 2014. [SMH14] F. Simančı́k, B. Motik, and I. Horrocks. Consequence-based and fixed-parameter tractable reasoning in description logics. Artificial Intelligence, 209:29–77, 2014. [Van11] F. Vanderbeck. Branching in branch-and-price: a generic scheme. Mathematical Programming, 130(2):249–294, 2011. 124