Description logics (DLs) [3] are a family of knowledge representation formalisms with numerous practical applications. SHIQ is a particularly important DL as it provides the formal underpinning for the Web Ontology Language (OWL). DLs model a domain of interest using concepts (i.e., unary predicate symbols) and roles (i.e., binary predicate symbols). DL applications often rely on subsumption-the problem of checking logical entailment between concepts-and so the development of practical subsumption procedures for DLs such as SHIQ has received a lot of attention. Most DLs are fragments of the guarded fragment [1] of first-order logic; however, SHIQ provides a restricted form of counting that does not fall within the guarded fragment. Moreover, most DLs, including SHIQ, can be captured using the two-variable fragment of first-order logic with counting (C2) [11], but this provides us with neither a practical nor a worst-case optimal reasoning procedure (C2 and SHIQ are NEXPTIME- and EXPTIME-complete, respectively). Algorithms for more general logics thus do not satisfy the requirements of DL applications, and so numerous alternatives specific to DLs have been explored. Many DLs can be decided in the framework of resolution [18, 13], including SHIQ [14]. These procedures are usually worst-case optimal and can be practical, but, as we discuss in Section 3, in even very simple cases they can draw unnecessary inferences. Practically successful SHIQ reasoners, such as FaCT++ [26], HermiT [9], Pellet [25], and Racer [12], use variants of highly-optimised (hyper)tableau algorithms [6]-model-building algorithms that ensure termination by a variant of blocking [7]. Although worst-case optimal tableau algorithms are known [10], practical implementations are typically not worst-case optimal. While generally very effective, tableau algorithms still cannot process certain ontologies; for example, the GALEN ontology1 has proved particularly challenging, mainly because tableau calculi tend to construct very large models. A breakthrough in practical ontology reasoning came in the form of consequencebased calculi. Although not originally presented in the consequence-based framework, the algorithm for the DL E L [2] can be seen as the first such calculus. This algorithm was later reformulated and extended to Horn-SHIQ [15] and Horn-SROIQ [19]DLs that support functional roles, but not disjunctive reasoning. Recently, consequencebased calculi were also developed for the DLs ALCH [24] and ALCI [23], which support disjunctive reasoning, but not counting. Consequence-based calculi can be seen as
a combination of resolution and hypertableau (see Section 3 for details). As in resolution, they describe ontology models by systematically deriving certain ontology consequences; and as in hypertableau, the ontology axioms can be used to guide the derivation process, and to avoid drawing unnecessary inferences. Moreover, consequence-based calculi are not just refutationally complete, but can classify an ontology in a single pass, which greatly reduces the overall work. These advantages allowed the CB system to be the first to classify all of GALEN [15].
Existing consequence-based algorithms can handle either disjunctions or counting, but not both. As we discuss in detail in Section 4, it is challenging to extend these algorithms to DLs such as S HIQ that combine both kinds of construct: counting quantifiers require equality reasoning, which together with disjunctions can impose complex constraints on ontology models. Unlike in existing consequence-based calculi, these constraints cannot be captured using DLs themselves; instead, a more expressive first-order fragment is needed, which makes the reasoning process much more involved.
In Section 5 we present a consequence-based calculus for S HIQ. Borrowing ideas from resolution theorem proving, we encode the required consequences using a special kind of first-order clause; and to handle equality effectively, we base our calculus on ordered paramodulation [17]—a state of the art calculus for equational theorem proving used in modern systems such as E [22] and Vampire [20]. To make the calculus efficient on E L, we have carefully constrained the rules so that, on E L ontologies, it mimics existing E L calculi. Thus, although a practical evaluation of our calculus is still pending, we believe that it is likely to perform well in practice on ‘mostly-E L’ ontologies due to is close relationship with existing and well-proven calculi. 2
First-Order Logic. To simplify matters technically, it is common practice in equational theorem proving to encode atoms as terms. An atomic formula P (~s) can be encoded as P (~s) t, where t is a new special constant, and P is considered as a function symbol rather than as a predicate symbol. Note however that, in order to avoid meaningless expressions in which predicate symbols occur at proper subterms, a multi-sorted type discipline on terms in the encoding is adopted. Thus, the set of symbols in the signature is partitioned into a set P of predicate symbols (which includes t), and a set F of function symbols.
A term is constructed as usual using variables and the signature symbols. Terms containing predicate symbols as their outermost symbol are called P -terms, while all other terms are F -terms. For example, for P a predicate and f a function symbol, both f (P (x)) and P (P (x)) are malformed; P (f (x)) is a well-formed P -term; and f (x) is a well-formed F -term. An (in)equality is an expression of the form s t (s 6 t) where s and t are both either F - or P -terms. We assume that and 6 are implicitly symmetric—that is, s ./ t and t ./ s are one and the same expression, for ./ 2 f ; 6 g. A literal is an equality or an inequality. An atom is an equality of the form P (~s) t, and we write it simply as P (~s) whenever it is clear from the context whether P (~s) is intended to be a P -term or an atom. A clause is an expression of the form ! where is a conjunction of atoms called the body, and is a disjunction of literals called the head. We often treat conjunctions and disjunctions as sets; and we write the empty conjunction (disjunction) as > (?). We use the standard notion of subterm positions; then, sjp is the subterm of s at position p; moreover, s[t]p is the term obtained from s by replacing the subterm at position p with t; finally, position p is proper in t if tjp 6= t.
Orders. A term order is a strict order on the set of all terms. The multiset extension mul of compares multisets M and N on a universe U such that M mul N if and only if M 6= N and, for each n 2 N n M , some m 2 M n N exists such that m n, where n is the multiset difference. We extend to literals by identifying each s 6 t with the multiset fs; s; t; tg and each s t with the multiset fs; tg, and by comparing the result using mul . Given an order , element b 2 U , and subset S U , the notation S b abbreviates 9a 2 S : a b.
Description Logic SHIQ. In this paper, a SHIQ ontology is represented as a set of DL-clauses, which we define next. Let P1 and P2 be countable sets of unary and binary predicate symbols, and let F be a countable set of unary function symbols. DLclauses are constructed using the central variable x and variables zi. A DL-F -term has the form x, zi, or f (x) with f 2 F ; a DL-P-term has the form B(zi), B(x), B(f (x)), S(x; zi), S(zi; x), S(x; f (x)), S(f (x); x) with B 2 P1 and S 2 P2; and a DL-term is a DL-F - or a DL-P-term. A DL-literal has the form A t with A a DL-P-term (called a DL-atom), or f (x) ./ g(x), f (x) ./ zi, or zi ./ zj with ./ 2 f ; 6 g. A DL-clause contains only DL-atoms of the form B(x), S(x; zi), and S(zi; x) in the body and only DL-literals in the head, and where each variable zi occurring in the head also occurs in the body. An ontology O is a finite set of DL-clauses. A query clause is a DL-clause in which all atoms are of the form B(x). Given an ontology O and a query clause ! , the query clause entailment problem is to decide whether O j= 8x:( ! ) holds; we often leave out 8x and write the latter as O j= ! .
SHIQ ontologies are commonly written using a DL-style syntax, but we can always transform such ontologies into DL-clauses without affecting the entailment of query clauses. Transitivity is encoded away as described in [21, 8], and the resulting axioms are normalised to the forms shown on the left-hand side of Table 1 as described in [15, 23]. The normalised axioms are translated to DL-clauses as shown in Table 1.
O1 = f
Bi v 9Sj :Bi+1 for 0
Bn v Cn
Ci+1 v 8Sj :Ci for 0
i < n and 1
i < n and 1
j
j
2 (
(
Bn(x)
vBn
Succ[: : : ]: > ! Bn (
Hyper[3+13]: > ! 8Sj :C0 (
To prove, say, O j= B0 v C0, a (hyper)tableau calculus constructs in a forwardchaining manner a tree-shaped model of depth n and of fanout two, where nodes at depth i are labelled by Bi and Ci. Forward chaining ensures that reasoning is goaloriented and thus amenable to practical implementation. However, all nodes labelled with Bi are of the same type and behave in the same way, which reveals a weakness of (hyper)tableau calculi: the constructed model can be large (exponential in our example) and highly redundant. Techniques such as caching [10] or anywhere blocking [16] can be used to constrain model construction, but their effectiveness often depends on the order of rule applications. Thus, model size has proved to be a key limiting factor for (hyper)tableau-based reasoners in practice [16].
In contrast, resolution describes models using universally quantified clauses that
‘summarise’ the model. This prevents redundancy and ensures worst-case optimality of
many resolution decision procedures. Nevertheless, resolution can still derive
unnecessary clauses. In our example, axioms (
Bi(x) ! Sj (x; fi;j (x)) for i 2 f1; : : : ; ng and j 2 f1; 2g
(
Sj (z1; x) ^ Ck+1(x) ! Ck(z1)
Bi(x) ^ Ck+1(fi;j (x)) ! Ck(x)
for k 2 f1; : : : ; ng and j 2 f1; 2g (
Consequence-based calculi combine the goal-directed reasoning of (hyper)tableau calculi with the ‘summarisation’ of resolution. In [23], we presented a very general framework for ALCI ontologies that captures the key elements of consequence-based calculi such as [2, 15, 19, 24]. We use this framework as basis for our extension to SHIQ so, before presenting our extension, we explain the main concepts on O1. Due to space restrictions we cannot reproduce in full the inference rules from [23]; however, these are similar in spirit to our inference rules for SHIQ presented in Table 2.
Our calculus constructs a context structure D = hV; E ; S; core; i—a graph whose vertices V are called contexts and whose directed edges are labelled with concepts of the form 9S:B. Let I be a model of O. Instead of representing each element of I individually as in (hyper)tableau calculi, we ‘summarise’ all elements of a certain kind using a single context v. Each context v 2 V is associated with a (possibly empty) set corev of core concepts that hold in all domain elements that v represents; thus, corev determines the kind of context v. We use a set Sv of clauses to capture additional constraints that the elements represented by v must satisfy; in ALCI, we can do so using clauses over DL concepts of the form d Bi v F Bj t F 9Sk:Bk t F 8S`:B`. Thus, unlike in resolution where all consequences belong to a single set, we assign a consequence a particular set in order to reduce the number of inferences. Clauses in Sv are ‘relative’ to corev: for each v 2 Sv, we have O j= corev u v —that is, we choose not to include corev in clause bodies since corev always holds. Finally, provides each context v 2 V with a concept order v that restricts resolution inferences in the presence of disjunctions.
Consequence-based calculi are not just refutation-complete: they actually derive
the required consequences. Figure 1 shows how this is achieved for O1 j= B0 v C0;
the core and the clauses are shown, respectively, above and below a context. To prove
B0 v C0, we introduce context vB0 with corevB0 = fB0g and clause (
Next, the Succ rule satisfies the existential quantifiers in (
We construct contexts vB2 ; : : : ; vBn in a similar way, finally deriving (
Thus, like resolution, consequence-based calculi ‘summarise’ models to prevent redundant computation, and, like (hyper)tableau calculi, they differentiate elements in a model of O to prevent the derivation of consequences such as (18).
B0(x) ! S(f1(x); x) (19) B1(x) ! S(x; fi(x)) for 2
B0(x) ! B1(f1(x)) (20) B1(x) ! Bi(fi(x)) for 2 B2(x) ^ B3(x) ! ? (21) Bi(x) ! B4(x) for 2
B1(x) ^ V1 j 3 S(x; zi) ! W1 j<k 3 zj zk 3 (22) 3 (23) 3 (24) (25) g We now present an example before formalising the calculus. Due to an interaction between counting quantifiers and inverse roles, a SHIQ ontology can impose more complex constraints on model elements than ALCI . Let O2 be the SHIQ ontology shown in Figure 2; we argue that O2 j= B0(x) ! B4(x) holds. To see why, consider an equality Herbrand interpretation I constructed from B0(a). Then, (19) and (20) derive S(f1(a); a) and B1(f1(a)); moreover, (22) and (23) derive S(f1(a); f2(f1(a))) and B2(f2(f1(a))), and S(f1(a); f3(f1(a))) and B3(f3(f1(a))). Due to (24) we derive B4(f2(f1(a))) and B4(f3(f1(a))). Finally, from (25) we derive (52). f2(f1(a)) a _ f3(f1(a)) a _ f3(f1(a)) f2(f1(a)) (52) We must satisfy at least one disjunct in (52). Disjunct f3(f1(a)) f2(f1(a)) cannot be satisfied due to (21); but then, regardless of whether we satisfy f3(f1(a)) a or f2(f1(a)) a, we derive B4(a); hence, the inference holds.
To prove this in our consequence-based framework, we must capture constraint (52) and its consequences. However, this cannot be done using standard description logic notation because DL concepts cannot identify specific successors and predecessors of f1(a)—that is, they cannot say ‘either the first or the second successor is equal to the predecessor’. Thus, our main challenges are to devise a method for representing all the relevant constraints that can be induced by SHIQ ontologies, and to ensure that such constraints are correctly propagated between adjacent contexts.
To address these challenges, we Skolemise existential quantifiers and transform axioms into DL-clauses. Skolemisation introduces function symbols that act as names for successors. Our clauses thus contain terms of the form x, fi(x), and y which have a special meaning in our setting: variable x represents the elements that a context stands for; fi(x) represents a successor of x; and y represents the predecessor of x. This allows us to represent constraint (52) as f2(x) y _ f3(x) y _ f3(x) f2(x): (53)
Table 2 shows the inference rules of our calculus that are applicable to such a clausal representation. In each clause, literals are ordered from the smallest to the largest, and so the maximal literal is always on the right; moreover, clause numbers correspond to the order of clause derivation. In the rest of this section, we discuss the rules on our running example and show how they verify O2 j= B0(x) ! B4(x); for brevity, we present only the inferences needed to produce the desired conclusion.
We first create context v1 and initialise it with (26); this ensures that each interpretation represented by the context structure contains an element for which B0 holds. Next, we derive (27) and (28) using hyperresolution. At this point, we could hyperresolve (22) and (28) to obtain > ! S(f1(x); f2(f1(x))); however, such inferences could easily lead to nontermination of the calculus due to increased term nesting. Therefore, we require hyperresolution to map variable x in the DL-clauses to variable x in the context clauses; thus, in each context, hyperresolution derives only consequences about x.
Function symbol f1 in clauses (27) and (28) is akin to an existential quantifier; consequently, the Succ rule introduces a fresh context v2. Due to Skolemisation, edges in our context structure are labelled with function symbols, rather than concepts of the form 9S:B as in [23]. The rule uses an expansion strategy analogous to the E L strategy from Section 3. To determine which information to propagate to a successor, Definition 2 given below introduces a set Su(O) of successor triggers. In our example, DL-clause (25) contains atoms B1(x) and S(x; zi) in its body, where zi can be mapped to a predecessor or a successor of x, so a context in which hyperresolution is applied to (25) will be interested in information about its predecessors; we reflect this by adding B1(x) and S(x; y) to Su(O). Thus, the Succ rule introduces context v2, sets its core to B1(x) and S(x; y), and initialises the context with (30) and (31).
We next introduce (32)–(35) using hyperresolution, at which point we have sufficient information to apply hyperresolution to (25) to derive (36). Please note how the presence of (30) is crucial for this inference. We use paramodulation to deal with equality in clause (36). As is common in resolution-based theorem proving, we order the literals in a clause and apply inferences only to maximal literals; thus, we derive (37).
Clauses (32), (33), and (37) contain function symbol f2, so we again apply the Succ rule and introduce context v3. Due to clause (33), we know that B2(x) must always hold in v2, so we add B2(x) to corev2 . However, B3(f2(x)) occurs in clause (37) in a disjunction, so it holds only conditionally in v2; we reflect this by including B3(x) in the body of clause (41). This allows us derive (42) using hyperresolution.
Clause (42) essentially says ‘B3(f2(x)) should not hold in the predecessor’, so the Pred rule propagates this information to v2. This produces clause (46); one can intuitively understand this inference as hyperresolution of (37) and (42), where we take into account that term f2(x) in context v2 is represented as variable x in context v3.
After two paramodulation steps, we derive clause (48), which essentially says ‘the predecessor must satisfy B2(x) or B3(x)’. The set Pr(O) of predecessor triggers from Definition 2 identifies this information as relevant to v1: the DL-clauses in (24) contain B2(x) and B3(x) in their bodies, which are represented in v2 as B2(y) and B3(y). Hence Pr(O) contains B2(y) and B3(y), which allows the Pred rule to derive (49).
After two more hyperresolution steps, we finally derive our target clause (51). Please note, however, that we cannot derive this if B4(x) were maximal in (50); thus, for completeness we require all atoms in the head of a query clause to be smallest. A similar observation applies to Pr(O): if B3(y) were maximal in (47), we would not derive (48) and propagate it to v1; thus, we require all atoms in Pr(O) to be smallest too. 5
Formalising the Consequence-Based Algorithm for S HI Q Our calculus manipulates context clauses, which are constructed from context terms and context literals as described in Definition 1. Unlike in general resolution, we restrict context clauses to contain only variables x and y, which have a special meaning in our setting: variable x represents a point (i.e., a term) in the model, and y represents the predecessor of x; this naming convention is important for the rules of our calculus. This is in contrast to the DL-clauses of an ontology: these can contain variables x and zi, and the latter can refer to either the predecessor or a successor of x.
Definition 1. A context F -term is a term of the form x, y, or f (x) for f 2 F ; a context P-term is a term of the form B(y), B(x), B(f (x)), S(x; y), S(y; x), S(x; f (x)), or S(f (x); x) for B; R 2 P and f 2 F ; and a context term is an F -term or a P-term. A context literal is a literal of the form A t (called a context atom), f (x) ./ g(x), or f (x) ./ y, for A a context P-term and ./ 2 f ; 6 g. A context clause is a clause with only function-free context atoms in the body, and only context literals in the head.
Definition 2 introduces sets Su(O) and Pr(O), that identify the information that must be exchanged between adjacent contexts. Intuitively, Su(O) contains atoms that are of interest to a context’s successor, and it guides the Succ rule whereas Pr(O) contains atoms that are of interest to a context’s predecessor and it guides the Pred rule. Definition 2. Let O be an ontology. The set Su(O) of successor triggers of O is the smallest set of atoms such that, for each clause ! 2 O, we have (i) B(x) 2 implies B(x) 2 Su(O), (ii) S(x; zi) 2 implies S(x; y) 2 Su(O), and (iii) S(zi; x) 2 implies S(y; x) 2 Su(O). The set Pr(O) of predecessor triggers is defined as
Pr(O) = f Afx 7! y; y 7! xg j A 2 Su(O) g [ f B(y) j B occurs in O g: Similarly to resolution, our calculus uses a term order to restrict its inferences. Definition 3 specifies the conditions that the order must satisfy. Conditions 1 and 2 ensure that F -terms are compared uniformly across contexts; however, P-terms can be compared in different ways in different contexts. Conditions 1 through 4 ensure that, when grounded with x and y mapping to a term its predecessor, respectively, the order is a simplification order [4]—a kind of term order commonly used in equational theorem proving. Finally, condition 5 ensures that atoms that might be propagated to a context’s predecessor via the Pred rule are smallest, which is important for completeness. Definition 3. Let m be a total, well-founded order on function symbols. A context term order is an order on context terms satisfying the following conditions: 1. for each f 2 F , we have f (x) x y; 2. for all f; g 2 F with f m g, we have f (x) g(x); 3. for all terms s1, s2, and t and each position p in t, if s1 s2, then t[s1]p 4. for each term s and each proper position p in s, we have s sjp; and 5. for each atom A t 2 Pr(O) and each context term s 62 fx; yg, we have A 6 s. t[s2]p; Order
is extended to literals, also written , as described in Section 2.
A lexicographic path order (LPO) [4] over context F -terms and context P-terms, in which x and y are treated as constants such that x y, satisfies conditions 1 through 4. Furthermore, Pr(O) contains only atoms of the form B(y), S(x; y), and S(y; x), which can always be smallest in the order; thus, condition 5 does not contradict the other conditions. Hence, an LPO that is relaxed for condition 5 satisfies Definition 3. In addition to orders, redundancy elimination techniques have proven crucial to the practical effectiveness of resolution calculi. We now define a criterion compatible with our setting. Definition 4. A set of clauses U contains a clause ! 2^ U , if ! up to redundancy, written 1. terms s and s0 exist such that s s 2 2. a clause 0 ! 0 2 U exist such that 0 or fs
s0; s 6 s0g and 0 .
, or Proposition 1. For U a set of clauses and C 2 U a clause such that C 2^ U n fC g, for each clause C0 with C0 2^ U , we have C0 2^ U n fC g.
Proposition 1 shows that our calculus is compatible with backward subsumption (which is captured in the Elim rule). Note that tautologies of the form A ! A are not necessarily redundant since they can be used to initialise contexts. However, if our calculus were to derive both A ! A and A ! A _ A0 then the latter is always redundant.
We now formalise the notion of a context structure, and define soundness for a context structure. The latter captures the fact that corev is not contained in the body of any context clause in Sv.
Definition 5. A context structure for an ontology O is a tuple D = hV; E ; S; core; i, where V is a finite set of contexts, E V V F is a finite set of edges labelled with function symbols, function core assigns to each context v a conjunction corev of atoms over the P-terms from Su(O), function S assigns to each context v a finite set Sv of context clauses, and function assigns to each context v a context term order v. A context structure D is sound for O if the following conditions both hold: S1. O j= corev ^ ! for each context v 2 V and each clause ! S2. O j= coreu ! corevfx 7! f (x); y 7! xg for each edge hu; v; f i 2 E . 2 Sv, and
Definition 6 introduces an expansion strategy—a parameter of our calculus that determines when and how to reuse contexts in order to satisfy existential restrictions. We have discussed the roles of expansion strategies in Section 3; moreover, in [23] we presented several expansion strategies for the DLs contained in ALCI, and adapting these to SHIQ is straightforward. c c u S i 6 u Ai for 1 i m + n, i m, hVuim;=v1; Afii 2!EW,im=+mn+1 Ai 2 Sv,
i ! i _ Ai 2 Su with Ai 2 Pr(O) for each m + 1 and Vim=1 i ! Wim=1 ii __ WWiimm==++mmnn++11 AAii t62^o SSuu,; then add Vim=1 i ! Wim=1 where = fx 7! f (x); y 7! xg.
If ! _ A 2 Su where 6 u A and A contains f (x), and
no edge hu; v; f i 2 E exists such that A ! A 2^ Sv for each A 2 K2 n corev, then let hv; core0; 0i := strategy(K1; D); if v 2 V, then let v := v \ 0, and otherwise let V := V [ fvg, corev := core0, v := 0, and Sv := ;; add the edge hu; v; f i to E; and add A ! A to Sv for each A 2 K2 n corev; where = fx 7! f (x); y 7! xg,
K1 = f A 2 Su(O) j > ! A 2 Su g, and
K2 = f A 2 Su(O) j 0 ! 0 _ A 2 Su and 0 6 u A g.
Definition 6. An expansion strategy is a polynomial-time computable function strategy that takes a set of atoms K and a context structure D = hV; E ; S; core; i. The result of strategy(K; D) is a triple hv; core0; 0i where core0 is a subset of K; either v 2= V is a fresh context, or v 2 V is an existing context in D such that corev = core0; and 0 is a context term order.
We now present the main theorems. Full proofs of all technical results can be found in [5]. Theorem 1 proves that all clauses derived by our calculus are indeed conclusions of the input ontology, and Theorem 2 is our statement of completeness. Theorem 1. For any strategy, applying a rule from Table 2 to an ontology O and a context structure D that is sound for O produces a context structure that is sound for O. Theorem 2. Let O be an ontology, and let D = hV; E ; S; core; i be a context structure such that no inference rule from Table 2 is applicable to O and D. Then, for each query clause Q ! Q and each context q 2 V that satisfy all of the following conditions, we have Q ! Q 2^ Sq.
C1. O j= Q ! Q.
C2. For each atom A
we have s t 2 C3. For each A 2 t 2 Q and each context term s 62 fx; yg such that A
Q [ Pr(O).
Q, we have Q ! A 2^ Sq. q s, Q.
Theorems 1 and 2 result in the following algorithm for deciding O j= Q ! 1. Create an empty context structure D, introduce a context q, and, for each A 2 add Q ! A to Sq in order to satisfy condition C3. 2. Initialise q in a way that satisfies condition C2, and select an expansion strategy. 3. Saturate D and O using the inference rules from Table 2. 4. Q ! Q holds if and only if Q ! Q 2^ Sv.
Q, Proposition 2. For each expansion strategy that introduces at most exponentially many contexts, the consequence-based calculus for SHIQ is worst-case optimal. Proof. The number } of different context clauses that can be generated using the symbols in O is clearly at most exponential in the size of O, and the number m of clauses participating in each inference is linear in the size of O. Hence, with k contexts, the number of inferences is bounded by (k })m; if k is at most exponential in the size of O, the number of inferences is exponential as well. Thus, if at most exponentially many contexts are introduced, our algorithm runs in exponential time, which is worst-case optimal for SHIQ [3]. tu 6
We have presented the first consequence based calculus for SHIQ, a DL that includes both disjunction and counting quantifiers. Our calculus combines ideas from state of the art resolution and (hyper)tableau calculi, including the use of ordered paramodulation for efficient equality reasoning. In spite of its increased complexity, the calculus mimics existing and well proven E L calculi on E L ontologies. Thus, although implementation and evaluation remain as future work, we believe that the calculus is likely to work well on ‘mostly-E L’ ontologies—a type of ontology that occurs commonly in practice. 18. H. De Nivelle, R. A. Schmidt, and U. Hustadt. Resolution-Based Methods for Modal Logics.
Logic Journal of the IGPL, 8(