Optimizing Inconsistency-tolerant Description Logic Reasoning

Abstract

The study of inconsistency-tolerant description logic reasoning is of growing importance for the Semantic Web since knowledge within it may not be logically consistent. The recently developed quasi-classical description logic has proved successful in handling inconsistency in description logic. To achieve a high level of performance when using tableau-based algorithms requires the incorporation of a wide range of optimizations. In our previous work, we developed a naive inconsistency-tolerant reasoner that can handle inconsistency directly. Here, we investigate a set of well known, state-ofthe-art optimization techniques for inconsistency-tolerant reasoning. Our experimental results show significant performance improvements over our naive reasoner for several well-known ontologies. To the best of our knowledge, this is the first attempt to apply optimizations for inconsistency-tolerant tableau-based reasoning.

Introduction

the former approach, the latter one is better for large and complex ontologies [ 10 ]. Moreover, in the first class of approaches, we may lose useful information during the process of removing inconsistencies [ 3 ]. In this work we focus on the second class of approaches.

In the last decades, a number of researchers have extended DL in different ways in order to cope with inconsistency [ 3, 8, 10 ]. Nguyen et al. studied three-valued DL based on Kleene’s three-valued semantics [ 8 ]. Another three-valued DL is paradoxical DL [ 11 ] based on Priest’s paradoxical semantics. Kaminski et al. presented a paraconsistent version of the three-valued semantics for hybrid knowledge bases which allows full paraconsistent reasoning [ 12 ]. Indeed, three-valued DLs are usually appropriate for handling the inconsistency but not the incompleteness of a KB. In many KBs, information is not only inconsistent but is also incomplete. Four-valued DL, based on four-valued logic [ 13 ], is studied by Ma et al. in [ 3 ] and has received a lot of attention. Though it can handle both inconsistent and incomplete KBs, it is not widely accepted due to its weak inference power [ 10 ]. For example, four-valued DL does not fully support a few important properties about inference such as modus tollens (MT), disjunctive syllogism (DS), resolution, etc. Recently, Zhang et al., proposed a paraconsistent version of DL, called QCDL, in [ 10 ], based on quasi-classical propositional logic (QC-logic) originally presented in [ 14 ]. Weak inference power, one of the common problems of the family of paraconsistent logics, is overcome by QCDL. Most inference rules like MT, DS are valid in QCDL.

In the previous work [ 15 ], we presented a sound, complete, and decidable tableau algorithm for QCDL and implemented a tableau based paraconsistent reasoner called QC-OWL based on this algorithm. However, we did not address any optimization techniques in QC-OWL. Most modern reasoners implement a set of state-of-the-art optimization techniques and these techniques are the keys to the enhanced performance of a modern tableau-based reasoner. Here, we extend a set of state-of-the-art optimization techniques for classical tableau based reasoner, namely normalization and simplification, unfolding, absorption, semantic branching, and dependency directed backtracking, to paraconsistent reasoning (background and motivation of these well-known techniques may be found in [ 16 ]). We implement those techniques on top of QC-OWL and compare the performance with that of our previous work, where no optimizations were addressed.

The rest of this paper is organized as follows: Section 2 briefly introduces the syntax and semantics of QCDL, Section 3 describes the optimization techniques, Section 4 presents the implementation and evaluation of those optimizations, Section 5 outlines some related works and future research directions, and finally, Section 6 concludes the paper. 2

Preliminaries

In this section we briefly introduce the syntax and semantics of QCDL. We focus on an expressive DL fragment, SHIQ, and call it quasi-classical SHIQ (in short, QC-SHIQ). We assume that the readers are familiar with the basic DL formalism; for more comprehensive background knowledge of DLs and QCDL, the reader is referred to [ 10, 15, 16 ]. 2.1

QCDL syntax and semantics

The syntax and semantics of QCDL is presented in [ 10 ] by extending the semantics of quasiclassical logic (QC-logic) proposed in [ 14 ]. The syntax of QC-SHIQ is slightly different from the syntax of classical SHIQ. In QC-SHIQ, the negation of a concept, i.e., ¬C, is taken as a different concept from C, rather than the complement of C. QC-negation, denoted by C, is used to represent the complement (set-theoretic complement) concept of C [ 10 ]. For a comprehensive background and motivation of QC-negation, the reader is referred to [ 10, 17 ].

Let NC , NR and NI be non-empty and pair-wise disjoint sets of concept names, role names, and individual names, respectively. Let R be a set of role names with a subset R+ ⊆ R of transitive role names. The set of roles is R ∪ {R− | R ∈ R}. The function Inv(.) is defined on roles such that Inv(R) = R− and Inv(R−) = R, where R is a role name.

Let R1, R2 ∈ R. A role axiom is a role inclusion of the form R1 v R2. An RBox or role hierarchy R is a finite set of role axioms. For a role hierarchy R, the relation v∗ is defined to be the transitive-reflexive closure of v on R ∪ {Inv(R) v Inv(S) | R v S ∈ R}. A role R is called sub-role (respectively, super-role) of a role S if R v∗ S (respectively, S v∗ R). A role S is simple if it is neither transitive nor has any transitive sub-roles.

The set of complex concepts is the smallest set such that • each concept name A ∈ NC is a concept; • if C, D are concepts, R is a role, S is a simple role, and n is a nonnegative integer, then C u D | C t D | ¬C | C | ∀R.C | ∃R.C | > nS.C | 6 nS.C are also concepts.

A general concept inclusion (GCI) is an expression in the form C v D, where C, D are concepts. A TBox is a finite set of GCIs. An assertion is of the form C(a) (concept assertion), R(a, b) (role assertion), or a 6=· b (inequality assertion), where a, b ∈ NI . An ABox contains a finite set of assertions. A QC-SHIQ KB is a triple K = (T , R, A) where T , A, and R are the TBox, ABox, and RBox, respectively.

Two types of interpretations, called weak interpretations and strong interpretations, are proposed by QCDL semantics. The former is the reformulation of that for four-valued logic. Before introducing these two types of interpretations, we first define a notion called base interpretations [ 10 ].

A base interpretation I is a pair (ΔI , .I ) where the domain ΔI is a set of individuals and the assignment function, .I , assigns: • each concept name A to an ordered pair h+A, −Ai where ±A ⊆ ΔI ; • each role R to an ordered pair h+R, −Ri where ±R ⊆ ΔI × ΔI ; • each inverse role R− to an ordered pair h+R−, −R−i where ±R− = {(y, x) | (x, y) ∈ ±R}; Note that each base interpretation maps an object X, when X ∈ {A, R, R−}, to a pair of sets of elements, unlike classical interpretation where an object is mapped to a set of elements. +X and −X are not necessarily disjoint. Intutively, +X is the set of elements known to be in X while −X is the set of elements known to be not in X.

A weak interpretation I is a base interpretation (ΔI , .I ) such that the assignment function .I satisfies the following conditions [ 15 ], where #M denotes the cardinality of a set M : >I = h ΔI , ∅ i; ⊥I = h ∅, ΔI i; (¬C)I = h −C, +C i; (C)I = h ΔI \ + C, ΔI \ − C i; (C u D)I = h +C ∩ +D, −C ∪ −D i; (C t D)I = h +C ∪ +D, −C ∩ −D i; (∀R.C)I = h {x ∈ ΔI | ∀y ∈ ΔI : (x, y) ∈ +R implies y ∈ +C},

{x ∈ ΔI | ∃y ∈ ΔI : (x, y) ∈ +R and y ∈ −C} i; (∃R.C)I = h {x ∈ ΔI | ∃y ∈ ΔI : (x, y) ∈ +R and y ∈ +C},

{x ∈ ΔI | ∀y ∈ ΔI : (x, y) ∈ +R implies y ∈ −C} i; (> nS.C)I = h {x ∈ ΔI | #{y ∈ ΔI : (x, y) ∈ +S and y ∈ +C} > n},

{x ∈ ΔI | #{y ∈ ΔI : (x, y) ∈ +S and y ∈ (ΔI \ − C)} < n} i; (6 nS.C)I = h {x ∈ ΔI | #{y ∈ ΔI : (x, y) ∈ +S and y ∈ (ΔI \ − C)} 6 n}, {x ∈ ΔI | #{y ∈ ΔI : (x, y) ∈ +S and y ∈ +C} > n} i.

Let I be a weak interpretation. A weak satisfaction relation, denoted by |=w, is defined as follows: I |=w C(a) if aI ∈ +C; I |=w R(a, b) if (aI , bI ) ∈ +R; I |=w C v D if +C ⊆ +D; I |=w R1 v R2 if +R1 ⊆ +R2; and I |=w a 6 =· b if aI 6= bI ; where XI = h+X, −Xi for any X ∈ {C, D, R, R1, R2} [ 15 ].

A strong interpretation is as similar to a weak interpretation except that the conjunction and disjunction of concepts are interpreted as follows [ 15 ]: (C u D)I = h+C ∩ +D, (−C ∪ −D) ∩ (−C ∪ +D) ∩ (+C ∪ −D)i; (C t D)I = h(+C ∪ +D) ∩ (−C ∪ +D) ∩ (+C ∪ −D), −C ∩ −Di.

The definition of strong satisfaction relation, denoted by |=s, is the same as that of the weak satisfaction relation except for GCIs [ 15 ]. For GCIs, |=s is defined as I |=s C v D if −C ⊆ +D, +C ⊆ +D, −D ⊆ −C.

Let K be a KB and φ be an axiom. K quasi-classically entails (QC entails) φ, denoted by K |=Q φ, if for every base interpretation I, I |=s K implies I |=w φ. In this case, |=Q is called QC-entailment. A base interpretation I is a QC-model of K if for all axioms ϕ in K, I |=s ϕ. K is QC-consistent if there exists some QC-model I of K, else it is QC-inconsistent [ 15 ]. 2.2

A tableau algorithm for QC-S HIQ Abox State of the art DL systems typically use tableaux algorithms [ 18 ] to decide the consistency of a KB, i.e., to determine whether a given KB has a model. Consistency checking is one of the main inference problems to which all other inferences can be reduced [ 16 ]. A sound, complete and decidable tableau algorithm (called QC-tableau) for checking the QC-consistency of an ABox is proposed in [ 15 ] by modifying and extending the standard tableau algorithm for SHIQ [ 19 ]. We outline the main steps as follows.

First we note that, in order to work efficiently, the TBox is reduced to an empty TBox with the internalization technique and the ABox is transformed into Negation Normal Form (NNF).

Internalization: Let U be a universal role, that is, a transitive super role consisting of all roles occurring in T together with their respective inverses. The base interpretation of U is defined as follows: U I = hΔI × ΔI , ∅i for any base interpretation I. Given T , a concept CT is defined as

CT := l

(¬Ci t Di).

CivDi ∈ T Any individual x in any model of T will be an instance of CT . Let RU = R∪{R v U, Inv(R) v U | R occurs in C, D, T , A or R}. Now, A is QC-consistent w.r.t. R and T iff A ∪ {CT u ∀U.CT (a) | a occurs in A} is QC-consistent w.r.t. RU .

Negation Normal Form (NNF): A concept expressions is in NNF if all the negations directly precede concept names. Let C, D be two concepts. We say C is equivalent to D, denoted by C ≡s D, if for any strong interpretation I, CI = DI . That is, +C = +D and −C = −D where CI = h+C, −Ci and DI = h+D, −Di. Each QCDL concept is equivalent to a QCDL concept in NNF. NNF of a concept expression in QCDL can be computed by applying the equivalences from Table 1.

The QC-tableau algorithm works on a data structure called a completion forest. The algorithm starts with the input ABox, A, and applies consistency preserving expansion rules from Table 2 (due to space limitation only five rules are presented here; for the remaining rules the reader is referred to [ 15, 17 ]) until no more rules are applicable (the tableau is complete) or an obvious contradiction (called a clash) is found in every branch. If a complete and clashfree completion forest is obtained, A is QC-consistent; otherwise it is QC-inconsistent. In the completion forest, the label of a node x is denoted by L(x). ≡s ≡s ≡s ≡s ≡s ≡s ≡s

C ¬C ¬C u ¬D ∀R.¬C ∀R.C > n + 1 S.C > (n + 1) S.¬C

¬¬C ¬(C u D) ¬∀R.C

∀R.C ¬(> n + 1 S.C) (> n + 1) S.C ≡s ≡s ≡s ≡s ≡s ≡s

C ¬C t ¬D ∃R.¬C ∃R.C 6 n S.C 6 n S.¬C The basic algorithm for inconsistency-tolerant reasoning discussed in the previous section is too slow for use in practice. We have investigated and employed a range of optimizations that improve the performance of standard tableau algorithms. These optimizations include: normalization and simplification, unfolding, absorption, semantic branching search, dependency directed backtracking. The first three techniques are performed directly on the input which serve to pre-process and simplify the input into a form more amenable to later processing, while the remaining techniques are applied during the search for a model. In the following subsections, each of these techniques will be revised for QCDL by modifying and extending the techniques presented in [ 16 ] for classical DLs. 3.1

Normalization and Simplification

Normalization is an optimization technique performed in pre-processing. It allows the detection of contradictions involving complex concepts early during tableaux expansion. Theoretical descriptions of tableau algorithms generally assume that the concept expression to be tested is in negation normal form. Though it simplifies the algorithm, this means that a contradiction will be detected only when an atomic concept and its negation occur in the same node label.

Example 1 Consider the concept expression ∃R.(C u D) u ∃R.C, where C is an atomic concept. When the algorithm creates an R-successor using the ∃-rule and applies the ∃-rule to ∃R.C, a clash will be detected due to the fact that {C, C} ∈ L(y). However, if C is a concept expression then C will be transformed into NNF. Thence, the clash would not be detected immediately. If C is a complex concept this may cause a lot of unnecessary expansion. It is possible to detect contradictions caused by non-atomic concepts early by transforming all concepts into a syntactic normal form, which we define here.

Logics that include full negation often provide pairs of operators, either one of which can be eliminated in favor of the other, by using negation. In syntactic normal form, all concepts are transformed so that only one of each such pair appears in the KB. In QC-SHIQ, as in classical SHIQ, all concepts could be transformed into atomic concepts, negations, conjunctions, value restrictions and QC-negations. For example, ∃R.C is transformed into ¬∀R.¬C. It is important to note that within the normalization process, conjunctions are considered as sets; this simplifies the elimination of redundant conjuncts. For example, ¬C t ¬D is transformed into ¬ u {C, D}. The normalization process can also include a range of simplifications that detect obvious clashes during the normalization process and also gets rid of redundant elements of a concept expression.

N orm(A) = N orm(¬C) =

N orm(C) = N orm(C1 u ... u Cn) = N orm(C1 t ... t Cn) =

N orm(∀R.C) =

N orm(∃R.C) = N orm(> n R.C) = N orm(6 n R.C) =

Simp(A) = Simp(¬C) =

Simp(C) =

Simp(uS) =

Simp(∀R.C) = Simp(> n R.C) =

A for an atomic concept A

Simp(¬(N orm(C))) Simp(N orm(C)) Simp(u({N orm(C1)} ∪ ... ∪ {N orm(Cn)})) N orm(¬(¬C1 u ... u ¬Cn)) Simp(∀R.N orm(C)) N orm(¬∀R.¬C) Simp(> n R.N orm(C)) N orm(¬ > (n + 1) R.C) A for an atomic concept A  Simp(D) if C = ¬D 

Simp(¬D) if C = D  ¬C otherwise.

Simp(D) if C = D

C otherwise.  Simp(uP ∪ S\{u{P}}) 

clash  uS ∀R.C > n R.C if u {P} ∈ S if {C, C} ⊆ S otherwise. [S, P are sets of concepts] Expression ¬¬C ¬C C1 u C2 C1 t C2 ∀R.C ∃R.C > n R.C > n R.C

Normalized & Simplified C ¬C u{C1, C2} ¬ u {¬C1, ¬C2} ∀R.C ¬∀R.¬C > n R.C > n R.C

Expression

Normalized & Simplified

C C1 u C2 C1 t C2 ∀R.C ∃R.C 6 n R.C 6 n R.C

C u{C1, C2} ¬ u {¬C1, ¬C2} ∀R.C ¬∀R.¬C ¬ > (n + 1) R.C ¬ > (n + 1) R.C successor using the ∃-rule whose label contains both C and C (by applying the ∃-rule to the term ¬∀R.¬C). Since the two occurrences of C are in the syntactic normal form, a clash will be detected immediately, regardless of the structure of C. Unfolding is a recursive substitution procedure that allows the testing of the satisfiability of a given concept C w.r.t. T by eliminating from C all concept names occurring in T [ 16 ]. If A ≡ D is an axiom in T , where A is a non-primitive (defined in T ) concept name, the procedure simply substitutes (i.e., unfolds) A with D wherever it occurs in C, and then recursively unfolds D in the same manner. If A v D is an axiom in T , where A is a primitive concept name, A is substituted by A0 u D, where A0 is a new concept name that does not occur in T or C. The concept name A0 represents the primitiveness of A, i.e., the unspecified characteristics that differentiate A from D. Unfold(C, T ) denotes the concept C after unfolding w.r.t. T [ 16 ].

Subsumption testing can be made independent of T using the same technique. The problem of determining if C is subsumed by D w.r.t. a TBox T is the same as the problem of determining if Unfold(C, T ) is subsumed by Unfold(D, T ) w.r.t. an empty TBox; in other words, T |= C v D iff ∅ |= Unfold(C, T ) v Unfold(D, T ) [ 16 ].

Generally there are two problems regarding concept unfolding: (1) an unrestricted recursive unfolding could possibly produce a resulting concept expression of exponential size; (2) unfolding would not be possible if T contains (i) multiple definitions for some concept name A, e.g., if {A ≡ C, A ≡ D} ⊆ T , or (ii) cyclical axioms, e.g., if (A v ∃R.A) ∈ T . The former problem can be addressed by a technique called lazy unfolding which unfolds concepts only when required during the progress of the algorithm. In other words, lazy unfolding does not expand the occurrences of concept names which follow ∃ or ∀. For example, when testing the satisfiability of an expression ∃R.E, where E is a concept name, the unfolding of E can be delayed until the ∃-rule has created an R-successor y with L(y) = {E}. By imposing this restriction, lazy unfolding may prevent the exponential increase of a concept expression.

Example 3 Consider, testing the satisfiability of the concept expression: ∃R.E u ∀R.E. The optimized algorithm will detect a contradiction immediately when the ∃-rule creates an R-successor y and applies the ∀-rule because {E, E} ⊆ L(y). This may save a lot of unnecessary work if unfolding E produces a large and complex expression.

As we have just noticed, all axioms in an arbitrary TBox are not amenable to unfolding. The solution to this problem is to divide the Tbox T into two components, a general part Tg and an unfoldable part Tu such that T = Tu ∪Tg; where Tu contains unique, acyclical, definition axioms and Tg contains the rest of T . This can be achieved easily by initializing Tu to ∅, then for each axiom X in T , adding X to Tu if Tu ∪ X is still unfoldable, adding X to Tg otherwise. In this way, reasoning tasks w.r.t. T can be considered as reasoning tasks w.r.t. Tu and Tg: use lazy unfolding to deal with Tu and internalization to deal with Tg [ 16 ]. 3.3

Absorption

As we have seen in the previous section, an arbitrary TBox T is divided into two parts, Tu and Tg; unfolding is applied to Tu and internalization is applied to Tg. The reasoning performance for Tu can be very good, while the reasoning performance for Tg might be bad, because internalization may introduce many disjunctions which increases the search space exponentially. For example, if a Tg contains 10 GCIs with 10 nodes, there are already 100 disjunctions, and they can be non-deterministically expanded in 2100 different ways. Therefore, it is a good strategy to eliminate as many GCIs from Tg as possible.

Absorption is a technique that tries to eliminate GCIs by absorbing them into primitive definitions. By considering Tu and Tg, if one can move axioms from Tg to Tu while keeping the semantics of T unchanged, one should be able to improve the reasoning performance. The absorption technique presented here is analogous to that of classical DL described in [ 16 ] except for handling the QC-negations. The basic idea is that a GCI of the form C v D, where C may be a non-atomic concept, is transformed into the form of a primitive definition A v D0, where A is an atomic concept, using the axiom equivalences (1) and (2) below. Then, A v D0 together with an existing primitive definition A v C0 may be replaced by A v C0 u D0.

C1 u C2 v D ⇐⇒ C1 v D t ¬C2 C v D1 u D2 ⇐⇒ C v D1 and C v D2 (1) (2)

Given Tu and Tg, absorbing the axioms from Tg into the primitive definitions in Tu can be done according to the following procedure. First, each axiom of the form C ≡ D is replaced by an equivalent pair of axioms C v D and ¬C v ¬D, and Tg0 is set to ∅. Then for each axiom (C v D) ∈ Tg [ 16 ]: (A) Initialize a set G = {¬D, C}, which represents the axiom in the form T v ¬ u {¬D, C} (i.e., T v D t ¬C). (B) If there is a primitive definition axiom (A v C) ∈ Tu for some A ∈ G, then absorb the general axiom into the primitive definition axiom so that it becomes A v u{C, ¬ u (G\{A})}, and exit. (C) If there is a primitive definition axiom (A ≡ D) ∈ Tu for some A ∈ G, then substitute A with D, G → {D} ∪ G\{A}, and return to step (B). (D) If there is a primitive definition axiom (A ≡ D) ∈ Tu for some ¬A ∈ G, then substitute ¬A with ¬D, G → {¬D} ∪ G\{¬A}, and return to step (B). (E) If there is a primitive definition axiom (A ≡ D) ∈ Tu for some A ∈ G, then substitute A with D, G → {D} ∪ G\{A}, and return to step (B). (F) If there is some C ∈ G such that C is of the form uS, then use associativity to simplify G, G → S ∪ G\{uS}, and return to step (B). (G) If there is some C ∈ G such that C is of the form ¬ u S, then for every D ∈ S determine if C can be absorbed (recursively) in G, {¬D} ∪ G\{¬ u S}, and exit. (H) Otherwise, the axiom could not be absorbed, so add ¬ u G to Tg0, Tg0 → Tg0 ∪ ¬ u G, and exit.

In the above absorption technique, step (E) is new and has been added to the technique in [ 16 ] to handle QC-negations. 3.4

Semantic branching

Standard tableau algorithms are inherently inefficient because they use a search technique based on syntactic branching. When expanding the label of a node x, L(x), syntactic branching works by choosing an unexpanded disjunction (C1 t C2 t ... t Cn) in L(x) and searching the different models obtained by adding each of the disjuncts C1, C2, ..., Cn to L(x) [ 16 ]. Since the alternative branches of the search tree are not disjoint, the recurrence of an unsatisfiable disjunct in different branches can occur. This can lead to a lot of wasted expansions. For example, consider the tableau expansion of a node x, where L(x) = {(C t D1), (C t D2)} and C leads to a clash. The syntactic branching technique could lead a wasted expansion as shown in Figure 1, where a clash due to C must be demonstrated twice. This problem can be dealt with by using a semantic branching technique analogous to that of classical DL [ 16 ].

L(x) ∪ {C}

... ⇒ clash

L(x) = {(C t D1), (C t D2)} t t

L(x) ∪ {C}

... ⇒ clash

L(x) ∪ {D1} t

t

L(x) ∪ {D2} ⇒ OK

With semantic branching, a single disjunct D is chosen from one of the unexpanded disjunctions in L(x). The two possible sub-trees obtained by adding either D or D to L(x) are then searched (recall, D is the QC-negation of D, i.e., D ∩ D = ∅ w.r.t. the domain, and {D, D} is the clash). Now we have two disjoint subtrees and the possibility of wasted expansions such as in syntactic branching is avoided. As shown in Figure 2, with the semantic branching, only one exploration of the expression C was needed whereas, with the syntactic branching, two explorations are needed.

L(x) = {(C t D1), (C t D2)} t t L(x) ∪ {C} ⇒ clash

... ⇒ clash t

L(x) ∪ {C, D1}

t L(x) ∪ {C} ⇒ clash

L(x) ∪ {D2} ⇒ OK If a sub-problem leads to a clash, this clash can be detected only when the sub-problem is expanded. So inherent unsatisfiability concealed in sub-problems can lead to large amounts of unproductive backtracking search known as thrashing. The problem becomes worse when blocking is used to guarantee termination, because blocking may require that sub-problems be expanded only after all other forms of expansions have been performed. For example, expanding a node x, where L(x) = {(C1 t D1), ..., (Cn t Dn), ∃R.(A u B), ∀R.A} could lead to the fruitless exploration of 2n possible R successors of x until the inherent unsatisfiability is discovered. The search tree created by tableau algorithm (using semantic branching) is presented in Figure 3. This problem can be addressed by adopting a form of dependency-directed backtracking called backjumping. The technique is essentially the same as that for classical DL presented in [ 16 ]; here we review the techniques for handling the QC-negations.

Backjumping is a crucial optimization technique that can effectively prune irrelevant alternatives of non-deterministic branching decisions. If a branching point is not involved in a clash, other alternatives of the branching point may be bypassed, because they cannot eliminate the cause of clash. So the challenge is to locate the cause of a clash which will allow one to downsize the search space. In order to identify the branching point involved in a clash, all concepts are labeled with a dependency set containing information about the branching points on which they depend. A concept C ∈ L(x) depends on a branching point if C was added to L(x) at the branching point or if C depends on another concept D and D depends on that branching point. A concept C ∈ L(x) depends on a concept D when C was added to L(x) by the application of a deterministic expansion rule that used D. For example, if A ∈ L(x) was derived from the expansion of (A u B) ∈ L(x), then A ∈ L(x) depends on (A u B) ∈ L(x) [ 16 ].

When a concept is added to a node by applying the tableau expansion rules, it inherits the dependencies from the concepts it was generated by. If the concept is added by the application of a non-deterministic rule, a dependency from the new branching point is also added. When a clash is discovered, a new dependency set is created by the union of dependency sets of the clashing concepts and backtracking is initiated. In the backtracking, each branching point is checked against the dependency set to see whether it is in the dependency set. If a branching point is not in the dependency set, then the other branching points are ignored and backtracking continues. If the branching point is in the dependency set, and the other branches are not explored yet, then backtracking stops and searching proceeds with the exploration of the other branches. When all branches of a branching point are explored, the union of the dependency sets from the branches is taken and backtracking continues [ 16 ].

For example, consider the previous example; when expanding a node x, where L(x) = {(C1 t D1), ..., (Cn t Dn), ∃R.(A u B), ∀R.A}, by using backjumping we could reduce the search space dramatically. In the search algorithm, after creating n branches, the label of the nth node xn will contain {∃R.(A u B), ∀R.A}. When ∃R.(A u B) is expanded, the algorithm creates an R-successor y1 with L(y1) = {(A u B)} using the ∃-rule, and then applies the ∀-rule to ∀R.A which results with L(y1) = {(A u B), A}. Now, applying the u-rule to A u B leads to a clash, because {A, A} ⊂ L(y1). Since neither A nor A in L(y1) depend on the branching point from x to xn, the algorithm backtracks to the most recent branching point on which one of A or A did depend without exploring alternative branches at any branching point between x to xn. We show in Figure 4 how the search tree below x is pruned by backjumping, and thus the number of R-successors explored is reduced by 2n - 1. 4

Evaluation

To check the effectiveness of the optimization techniques discussed in the previous section for inconsistency-tolerant reasoning, i.e., QCDL, we implemented those techniques top of QC-OWL. QC-OWL [ 17 ] is an inconsistency-tolerant reasoner that can handle inconsistency directly with reasonable inference power. It can perform reasoning over both consistent and inconsistent ontologies with acceptable performance for the DL SHIQ. It was designed and developed by following the Strategy Pattern, a behavioral design pattern, and is based on the core framework of Pellet [ 20 ], a widely used complete OWL-DL reasoner.

In this section, we compare our results with those of our previous version of QC-OWL. The benchmark ontologies used in the experiments are presented in Table 5. The first 12 ontologies (ID# 1 to ID# 12) were found in [ 15 ] while 13 (ID# 13) was found in [ 10 ]. The ontologies 14, 15, 16, 17, 18 (ID# 14 to ID# 18) were collected from the TONES Ontology Repository [ 21 ] while the remaining two (ID# 19 to ID# 20) were collected from ISG Ontology Repository [ 22 ]. For the experiments each ontology was processed five times and the time required to perform QC-consistency test was recorded. The average time of the five independent runs is displayed in the table. In the table, the column Con is for the consistency and Opt with optimizations in QC-OWL. All experiments were performed on a Notebook with Intel Core i7 CPU and 8G

KB name

DL expressivity 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 amino-acid heart bad-food buggyPolicy tambis-patched uma-025-arctan 0.01-arctan 0.03-arctan 0.01-arctan-inc 0.03-arctan-inc 0.04-arctan-inc 0.07-arctan-inc chem-a goslim transportation economy numerics yowl-complex 00390 00786

ALCF(D)

SHI ALCO(D) ALCHO

SHIN ALCRIF(D) ALCRF(D) ALCRIF(D) ALCRIF(D) ALCRIF(D) ALCRF(D) ALCRIF(D) ALCHOF(D)

AL ALCH(D) ALCH(D) SHIF(D) SHIF(D)

SHIF SH(D)

Concept count memory on Windows 8 platform. The maximum allocated memory for JVM was 512M.

The experiments were conducted in two steps. In the first step, QC-consistency tests were performed for the same set of ontologies as found in [ 15 ]. The results are presented in Table 6 and Table 7 for consistent and inconsistent ontologies, respectively. As it is shown in Table 6, QC-OWL(Opt) marginally outperforms QC-OWL for consistent ontologies. Since QC-OWL already shows good performance for this set of ontologies, the performance improvement is not significant. Indeed, the search spaces of these ontologies are small due to the characteristics of these ontologies. However, the results presented in Table 7 show that QC-OWL(Opt) significantly outperforms QC-OWL for inconsistent ontologies. For example, in the case of the 0.04arctan-inc ontology, QC-OWL takes around 20 seconds whereas QC-OWL(Opt) takes only 32 milliseconds. It is important to note that the performance improvement through optimization is greater for inconsistent ontologies than consistent ontologies. The reason is, for an inconsistent ontology, every branch must be explored before returning the result. However, in the case of a consistent ontology, a model can be found before exploring all alternative branches. When a model is found in a branch, the algorithm returns immediately without exploring the remaining branches. Therefore in general, the performance improvement for inconsistent ontologies can be expected to be greater than that for consistent ontologies.

In the second step, QC-consistency test were performed for another set of popular ontologies and the results are presented in Table 8. For this experiments, the maximum allocated memory for JVM was 2G and mem-out stands for OutOfMemoryError in Java. The results presented in Table 8 show that optimizations play a significant role for the performance improvement. As an example, for the transportation ontology, QC-OWL takes 470 milliseconds whereas QCOWL(Opt) takes only 45 milliseconds. It is motivating to note for the 00786 ontology, QCOWL gets mem-out while QC-OWL(Opt) gets result in 325 milliseconds. The performance improvement in Table 8 is significant because the search spaces of these ontologies are larger than the ontologies in Table 6 (i.e., the ontologies in Table 8 contain more individuals than the ontologies in Table 6).

KB name chem-a.owl goslim.owl transportation.owl economy.owl numerics.owl yowl-complex.owl 00390.owl 00786.owl

Con

N Y Y Y Y Y Y Y

QC-OWL 94 260 470 661 2075 12262 mem-out mem-out

Related and Future Work

In the past decades, numerous techniques have been developed for optimizing standard tableaubased reasoning, but none of them are directed to inconsistency-tolerant reasoning. In this section, we outline some work that is related to optimizing the tableau-based reasoning for classical DLs and discuss some future research directions for improving the performance of an inconsistency-tolerant tableau-based reasoner.

Most state-of-the-art optimization techniques in tableau-based DL reasoning have been discussed in [ 16 ]. Apart from optimizing the tableau algorithm, a few researchers also attempted to parallelize the tableau algorithm itself by applying a thread-based strategy in a shared-memory environment (see, for example [ 17 ]). Although thread-based strategies such as multi-threading in a multi-cored processor are often the easiest and simplest way to achieve high performance, speed gain via thread-level parallelism is limited by the number of available cores. A processbased strategy discussed in [ 17 ] is another option for achieving scalable performance.

In order to provide efficiency in reasoning, 3 profiles for OWL 2 offer important advantages depending on the application scenario: OWL 2 EL, OWL 2 QL and OWL 2 RL [ 23 ]. For example, OWL 2 EL is useful for ontologies that contain very large numbers of properties and/or classes, while OWL 2 QL is useful for dealing with ontologies with very large volumes of instance data, and where query answering is the most important reasoning task. OWL 2 RL is aimed at applications that require scalable reasoning without sacrificing expressivity [ 23 ].

For the experiments, our reasoner has been implemented on top of Pellet using Java. Although Java has many appealing features, it is not strongly recommended for high performance computing due to some design features associated with this language, such as garbage collection, etc. Better performance can be achieved by implementing this algorithm in C or C++. Prolog, a general purpose logic programming language, could be another good choice. Prolog’s backtracking strategy may be well suited implementing the dependency-directed backtracking.

Recently, Faddoul and MacCaull [ 24 ] investigated algebraic tableau reasoning for the DL ALCQ. Preliminary results motivate the application of algebraic reasoning for paraconsistent reasoning. However, in order to work with an algebraic reasoning component, a standard tableau calculus needs to be modified and extended. 6

Conclusion

In this work, we discuss a set of widely used optimization techniques developed for classical tableau-based reasoners which we implemented on top of QC-OWL, our inconsistency-tolerant reasoner, and compare its performance with our naive implementation. The experimental results show a significant runtime improvement for a wide range of both consistent and inconsistent ontologies. While it is possible to measure the performance of each optimization individually, we did not do so, as these optimizations are benchmarked for classical DLs. In future, we shall investigate other optimizations for QC-OWL, e.g., boolean constraint propagation, heuristic guided search, etc. We also plan to parallelize the QC-tableau algorithm itself incorporating a set of optimization techniques which is hoped to significantly improve the performance of the QC-tableau algorithm.

Acknowledgments: The second author wishes to thank the Natural Sciences and Engineering Research Council of Canada for financial support.

References

[1] M. Horridge , B. Parsia , and U. Sattler, “ Explaining inconsistencies in OWL ontologies ,” in Proceedings of the 3rd International Conference on Scalable Uncertainty Management . Berlin, Heidelberg: Springer-Verlag, 2009 , pp. 124 - 137 .

[2] D. Bell , G. Qi, and W. Liu, “ Approaches to inconsistency handling in description-logic based ontologies,” in On the Move to Meaningful Internet Systems 2007 : OTM 2007 Workshops, ser . Lecture Notes in Computer Science, R. Meersman , Z. Tari , and P. Herrero, Eds. Springer Berlin Heidelberg, 2007 , vol. 4806 , pp. 1303 - 1311 .

[3] F. Maier , Y. Ma , and P. Hitzler , “ Paraconsistent OWL and related logics,” Semantic Web , vol. 4 , no. 4 , pp. 395 - 427 , 2013 .

[4] N. Kamide , “ A comparison of paraconsistent description logics ,” International Journal of Intelligence Science , vol. 3 , no. 2 , pp. 99 - 109 , 2013 .

[5] J. Fang and Z. Huang , “ Reasoning with inconsistent ontologies,” Tsinghua Science and Technology , vol. 15 , no. 6 , pp. 687 - 691 , 2010 .

[6] C. Cocos , F. Imam , and W. MacCaull, “ Ontology merging and reasoning using paraconsistent logics ,” International Journal of Knowledge-Based Organizations (IJKBO) , vol. 2 , pp. 35 - 51 , 2012 .

[7] G. Qi , W. Liu, and D. A. Bell , “ A revision-based approach for handling inconsistency in description logics ,” in Proceedings of the 11th International Workshop on NonMonotonic Reasoning (NMR06) , 2006 .

[8] L. Nguyen and A. Szalas , “ Three-valued paraconsistent reasoning for Semantic Web agents,” in Agent and Multi-Agent Systems: Technologies and Applications, ser . Lecture Notes in Computer Science, P. Jdrzejowicz, N. Nguyen , R. Howlet , and L. Jain, Eds. Springer Berlin Heidelberg, 2010 , vol. 6070 , pp. 152 - 162 .

[9] S. Odintsov and H. Wansing , “ Inconsistency-tolerant description logic. part ii: A tableau algorithm for CALCC,” Journal of Applied Logic , vol. 6 , no. 3 , pp. 343 - 360 , 2008 .

[10] X. Zhang , G. Xiao, Z. Lin , and J. Van Den Bussche , “ Inconsistency-tolerant reasoning with OWL DL,” International Journal of Approximate Reasoning , vol. 55 , no. 2 , pp. 557 - 584 , 2014 .

[11] X. Zhang , Z. Lin , and K. Wang , “ Towards a paradoxical description logic for the Semantic Web,” in Foundations of Information and Knowledge Systems, ser . Lecture Notes in Computer Science, S. Link and H. Prade, Eds. Springer Berlin Heidelberg, 2010 , vol. 5956 , pp. 306 - 325 .

[12] T. Kaminski , M. Knorr , and J. Leite , “ Efficient paraconsistent reasoning with ontologies and rules ,” in Proceedings of the 24th International Conference on Artificial Intelligence (IJCAI 2015 ), 2015 , pp. 3098 - 3105 .

[13] J. Belnap , Nuel D., “ A useful four-valued logic,” in Modern Uses of Multiple-Valued Logic, ser . Episteme, M. Dunn and G. Epstein, Eds. Springer Netherlands, 1977 , vol. 2 , pp. 5 - 37 .

[14] A. Hunter , “ Reasoning with contradictory information using quasi-classical logic , ” Journal of Logic and Computation , vol. 10 , pp. 677 - 703 , 1999 .

[15] X. Zhang , Z. Feng , W. Wu, M. Hossain , and W. MacCaull, “ On the satisfiability of qasi-classical description logics , ” Computing and Informatics , 2015 , to appear. [Online]. Available: http://cs.tju.edu.cn/faculty/zhangxiaowang/publication/CAI15.pdf

[16] F. Baader , D. Calvanese , D. L. McGuinness , D. Nardi , and P. F. Patel-Schneider , Eds., The Description Logic Handbook: Theory , Implementation, and Applications . New York, NY, USA: Cambridge University Press, 2003 .

[17] M. Hossain , “ Inconsistency-tolerant description logic reasoning ,” M.Sc. thesis, St. Francis Xavier University, 2016 .

[18] F. Baader and U. Sattler, “ An overview of tableau algorithms for description logics , ” Studia Logica , vol. 69 , no. 1 , pp. 5 - 40 , 2001 .

[19] I. Horrocks , U. Sattler , and S. Tobies , “ Reasoning with individuals for the description logic SHIQ ,” in Proceedings of the 17th International Conference on Automated Deduction. London , UK: Springer-Verlag, 2000 , pp. 482 - 496 .

[20] E. Sirin , B. Parsia , B. C. Grau , A. Kalyanpur , and Y. Katz , “ Pellet: A practical OWL-DL reasoner,” Web Semantics: Science, Services and Agents on the World Wide Web , vol. 5 , no. 2 , pp. 51 - 53 , 2007 .

[21] ( 2008 ) TONES: Ontology repository . University of Manchester. [last accessed: December 2015 ]. [Online]. Available: http://owl.cs.manchester.ac.uk/repository/

[22] Information Systems Group: Ontology repository. University of Oxford. [last accessed: April 2016 ]. [Online]. Available: http://www.cs.ox.ac.uk/isg/ontologies/

[23] P. Hitzler , M. Kro¨tzsch, B. Parsia , P. F. Patel-Schneider , and S. Rudolph, Eds., OWL 2 Web Ontology Language: Primer. W3C Recommendation , 27 October 2009 . [Online]. Available: http://www.w3.org/TR/owl2-primer/.

[24] J. Faddoul and W. MacCaull, “ Handling non-determinism with description logics using a fork/join approach ,” International Journal of Networking and Computing , vol. 5 , no. 1 , pp. 61 - 85 , 2015 .