Non-Standard Reasoning Services for the Debugging of Description Logic Terminologies

1 Introduction

Our work was motivated by the development of the DICE 1 terminology. DICE implements frame-based definitions of diagnostic information for the unambiguous and unified clas­ sification of patients in Intensive Care medicine. The repre­ sentation of DICE is currently being migrated to an expres­ sive Description Logic (henceforth DL) to facilitate logical inferences. Figure 1 shows an extract of the DICE terminol­ ogy. In [Cornet and Abu-Hanna, 2002] the authors describe the migration process in more detail. The resulting DL ter­ minology (usually called a "TBox") contains axioms such as the following, where classes (like BoovPART) are translated as concepts, and slots (like REGION) as roles:

Brain ~ Centra!NervousSystem n 3systempart.NervousSystem n BodyPart n 3region.HeadAndNeck n Vregion.HeadAndNeck Centra!NervousSystem ~ NervousSystem

Developing a coherent terminology is a time-consuming and error-prone process. DICE defines more than 2400 con­ cepts and uses 45 relations. To illustrate some of the prob­ lems, take the definition of a "brain" which is incorrectly specified, among others, as a "central nervous-system" and "body-part" located in the head. This definition is contradic­ tory as nervous-systems and body-parts are declared disjoint in DICE. Fortunately, current Description Logic reasoners,

1 DICE stands for "Diagnoses for Intensive Care Evaluation". The development of the DICE terminology has been supported by the NICE foundation.

Ronald Cornet

Academic Medical Center Universiteit van Amsterdam, Netherlands R. Cornet@amc. uva.nl

such as RACER [Haarslev and Moller, 2001] or FaCT [Hor­ rocks, 1998], can detect this type of inconsistency and the knowledge engineer can identify the cause of the problem. Unfortunately, many other concepts are defined based on the erroneous definition of "brain" forcing each of them to be erroneous as well. In practice, DL reasoners provide lists of hundreds ofunsatisfiable concepts for the DICE TBox and the debugging remains a jigsaw to be solved by human experts, with little additional explanation to support this process.

By debugging we understand the identification and elimi­ nation of modelling errors when detecting logical contradic­ tions in a knowledge base. Debugging requires an explana­ tion for the logical incorrectness and, as a second step, its correction. In this paper we will focus on the former as the latter requires an understanding of the meaning of represented concepts. We define a number of new non-standard reasoning services to explain incoherences through pinpointing.

Our experience with debugging DICE provides some hands-on examples for the problem at hand: take the con­ tradictory definition of brains in the DICE anatomy specifica­ tion. What information is useful for correcting the knowledge base? First, we have to identify the precise position of errors within a TBox; that is, we need a procedure to single out the axioms causing the contradiction. The axioms for Brain and CentralNervousSystem form such a minimal incoherent sub­ set of the DICE terminology. Formally, we introduce minimal unsatisfiability-preserving sub-TBoxes (abbreviated MUPS) and minimal incoherence-preserving sub-TBoxes (MIPS) as the smallest subsets of axioms of an incoherent terminology preserving unsatisfiability of a particular, respectively of at least one unsatisfiable concept. Secondly, we highlight the el­ ements of these definitions containing the faulty specification. An axiom, e.g. , Brain(;;BodyPart n NervousSystem points to the core of the erroneously modelled knowledge. For this purpose we define generalised incoherence-preserving termi­ nologies (GIT) as sets of incoherent axioms, which are syn­ tacticly related to the original axioms, more general and have minimal structural complexity.

The remainder of this paper is organised as follows : Sec­ tion 2 introduces the relevant DL concepts to make the paper self-contained. In Section 3 we introduce the new reasoning services and provide algorithms in Section 4. The paper fin­ ishes with a discussion of the results we obtained with our new methods on the terminology DICE.

Consider the following (incoherent) TBox Ti., where A, B and Care primitive and A1, . .. , A1 defined concept names:

The set of unsatisfiable concept names as returned by a DL reasoner is {A1 , A3, A6, A1 }. Although this is still of man­ ageable size, it hides crucial information, e.g., that unsatisfia­ bility of A1 depends on unsatisfiability of A3, which is inco­ herent because of the contradictions between A4 and A5 · We will use this example to explain our debugging methods.

Minimal unsatisfiability-preserving sub-TBoxes (MUPS) Unsatisfiability-preserving sub-TBoxes of a TBox T and an unsatisfiable concept A are subsets ofT in which A is unsat­ isfiable. In general there are several of these sub-TBoxes and we select the minimal ones, i.e., those containing only axioms that are necessary to preserve unsatisfiability.

Definition 3.1 Let A be a concept which is unsatisfiable in a TBox T A set T' ~ T is a minimal unsatisfiability­ preserving sub-TBox (MUPS) ofT if A is unsatisfiable in T', and A is satisfiable in every sub-TBox T" C T'.

We will abbreviate the set of MUPS of T and A by mups(T, A). MUPS for our example TBox Ti. and its un­ satisfiable concepts are:

MUPS are useful for relating unsatisfiability to sets of axioms but we will also use them in Section 4 to calculate MIPS.

Minimal incoherence-preserving sub-TBoxes (MIPS) MIPS are the smallest subsets of an original TBox preserving unsatisfiability of at least one atomic concept.

Definition 3.2 LetT be an incoherent TBox. A TBox T' ~ Tis a minimal incoherence-preserving sub-TBox (MIPS) of T if T' is incoherent, and every sub-TBox T" C T' is co­ herent.

We will abbreviate the set of MIPS ofT by mips(T) . ForTi. we get three MIPS:

mips(Ti) = { {ax1, ax2}, {ax3, ax4, axs}, {ax4, ax1}} It can easily be checked that each of the three incoherent TBoxes in mips(Ti.) is indeed a MIPS as taking away a sin­ gle axiom renders each of the three coherent. The first one signifies, for example, that the first two axioms are already contradictory without reference to any other axiom, which suggests a modelling error already in these two axioms.

2 Description Logics

We shall not give a formal introduction into Description Log­ ics here, but point to the new handbook [Baader et a!., 2003 ]. Briefly, DLs are set description languages with concepts (usu­ ally denoted by capital letters), interpreted as subsets of a do­ main, and roles which are binary relations, which we denote by small letters. In a terminological component T (called TBox) the interpretations of concepts can be restricted to the models ofT by defining axioms of the form C~D . 2 Based on this formal model-theoretic semantics, a TBox can be checked for incoherence, i.e., whether there are unsatisfiable concepts: concepts which are necessarily interpreted as the empty set in all models of the TBox. Other standard reason­ ing services include subsumption of two concepts C and D (a subset relation w.r.t. all models ofT). Subsumption with­ out reference to a TBox is called concept subsumption and we write C ~ D. Recently, a number of non-standard rea­ soning services have been defined, such as the least common subsumer of concepts or the minimal rewriting of concepts (see [Kiisters, 200 1] for an overview).

A.CC is a simple yet relatively expressive DL with conjunc­ tion (C n D), disjunction (CUD), negation (·C) and uni­ versal ('Vr.C) and existential quantification (3r.C). A TBox is called unfoldable if the left-hand sides of the axioms (the defined concepts) are atomic, and if the right-hand sides (the definitions) contain no direct or indirect reference to the de­ fined concept [Nebel, 1990].

3 Explaining Logical Incoherences

In this section we study ways of explaining incoherences in DL terminologies. We propose to simplify a terminology T in order to reduce the available information to the root of the incoherence. More concretely we first exclude axioms which are irrelevant to the incoherence and then provide simplified definitions highlighting the exact position of a contradiction within the axioms of this reduced TBox. We will call the former axiom pinpointing, the latter concept pinpointing.

In this section we will formally introduce axiom and con­ cept pinpointing for a general TBox without restrictions on the underlying representation language. In Section 4 we will give algorithms for the case ofunfoldable A.CC-TBoxes.

3.1 Axiom Pinpointing

Axiom pinpointing means identifying debugging-relevant ax­ ioms, where an axiom is relevant if a contradictory TBox be­ comes coherent once the axiom is removed or if, at least, a particular, previously unsatisfiable concept turns satisfiable.

2 We will not consider assertional components in this paper.

Cores

Minimal incoherence-preserving sub-TBoxes identify small­ est sets of TBox axioms causing the original TBox to be incoherent. In terminologies such as DICE, which are cre­ ated through migration from other representation formalisms, there are several such sub-TBoxes, each corresponding to a particular contradictory terminology. Cores are now sets of axioms occurring in several of these incoherent TBoxes. The more MIPS such a core belongs to, the more likely its axioms will be the cause of contradictions.

Definition 3.3 Let T be a TBox. A non-empty intersection of n different MIPS in mips(T) (with n 2: 1) is called a MIPS-core of arity n (or simply n-ary core) forT

Every set containing precisely one MIPS is, at least, a 1-ary core. The most interesting cores of a TBox, T, are those with axioms that are present in as many MIPS ofT as possible, i.e., having maximal arity. On the other hand, the size of a core is also significant, as a bigger size points to clusters of axioms causing contradictions in combination only.

In our running example, axiom ax4 occurs both in { ax3, ax4, ax5 } and { ax4, ax7}, which makes { ax4} a core of arity 2 forTi_, which is the core of maximal arity in this example.

3.2 Concept Pinpointing

The next step in the debugging process is to simplify the def­ initions in order to obtain more concise descriptions of errors within an incoherent TBox.

Generalised Terminologies

Incoherence of a TBox can be regarded as an over­ specification of one or more concepts in the relevant defi­ nitions. Generalised terminologies are terminologies where some of the definitions have been generalised. 3 Furthermore, we require generalised definitions to be syntactically related to the original axioms. For different representation languages and types of knowledge bases we will have to formally spec­ ify what we consider to be syntactically related concepts. For the time being let us keep the definition abstract and assume that there is such a relation rel ( C, C') denoting that two con­ cepts C and C' are related. Formally, a concept C' is then a syntactic generalisation of a concept C if rel(C, C') and C !;;;; C' (independent ofT). Note that we have to take care of the case when Cis unsatisfiable w.r.t. T Then Cis equiv­ alent to l.., and everything is more general. Therefore we generalise C without referencing to the original terminology T, i.e., we check for simple concept subsumption, only.

Now, generalised incoherence-preserving terminologies (GITs) are TBoxes where the defining concepts of the axioms are maximally generalised without losing incoherence.

Definition 3.4 Let T = { CI!~D1, .. . , Cn~Dn} be an in­ coherent TBox. An incoherent TBox T' = { C1 ~D~, ... , Cn~D~} is a generalised incoherence-preserving terminol­ ogy (G/T) ofT if, and only if,

• each D~ is a syntactic generalisation of Di (1 :::; i :::; n),

3 To simplify matters we generalise the right-hand side of axioms only as we are currently working with unfoldable TBoxes anyway.

• every TBox T" = { C1 ~D~, ... , Cn~D~} with a syn­ tactic generalisation D~' of Di where D~ !;;;; D~' and D~' 'l D~ (for some 1 :::; i :::; n) is coherent.

We abbreviate the set of generalised incoherence-preserving terminologies of a TBox T by git(T). Note that the set of GITs of a TBox T is equivalent to the union of GITs for the MIPS of T Take a simple syntactic relation relating a con­ cept with the syntactic sub-concepts of its unfolded version with the same polarity and quantifier depth. 4 As this particu­ lar definition of a syntactic relation depends on unfolding the related concepts, all but one axiom per GIT can be trivially generalised to Ai~T. Of all possible GITs we conjecture that the simplest ones, e.g., those with syntactically minimal generalisations, are most likely to be useful for the identifica­ tion of errors. In our experiments we use two alternative for­ malisations, the first with respect to minimal size of axioms, the second with respect to the number of concept names oc­ curring in the GIT. Three minimal sized GITs exist for our example TBox Ti_, where we only show the non-trivial ax­ ioms:

4 Debugging Unfoldable A.CC-TBoxes

Practical experience has shown that applying our methods on a simplified version of DICE can already provide valuable debugging information. We will therefore only provide al­ gorithms for unfoldable A.CC-TBoxes [Nebel, 1990] as this significantly improves both the computational properties and the readability of the algorithm.

4.1 Algorithms for Axiom Pointing

The calculation of MIPS depends on the MUPS only, and we will provide an algorithm to calculate these minimal unsatisfiability-preserving sub-TBoxes based on Boolean minimisation of terminological axioms needed to close a standard tableau ([Baader et al., 2003] Chapter 2).

Usually, unsatisfiability of a concept is detected with a fully saturated tableau (expanded with rules similar to those in Figure 2) where all branches contain a contradiction (or close, as we say). The information which axioms are rele­ vant for the closure is contained in a simple label which is added to each formula in a branch. A labelled formula has the form (a : c)z where a is an individual name, c a con­ cept and x a set of axioms, which we will refer to as label. A labelled branch is a set of labelled formulas and a tableau is a set of labelled branches. A formula can occur with different labels on the same branch. A branch is closed if it contains a clash, i.e. if there is at least one pair of formulas with con­ tradictory atoms on the same individual. The notions of open branch and closed and open tableau are defined as usual and do not depend on the labels. We will always assume that any formula is in negation normal form (nnt) and newly created formulas are immediately transformed. We usually omit the prefix "labelled".

4 The polarity of a concept name A specifies whether A occurs within odd or even numbers of negations, the quantifier depth is the sequence of roles over which the concept is quantified. Such a relation will formally be defined for unfoldable A.CC-TBoxes in Definition 4.3.

To calculate a minimal unsatisfiability-preserving TBox for a concept name A w.r.t. an unfoldable TBox T we construct a tableau from a branch B initially containing only (a : A) 0 (for a new individual name a) by applying the rules in Figure 2 as long as possible. The rules are standard A.CC-tableau rules with lazy unfolding, and have to be read as follows : assume that there is a tableau T = { B, B i, .. . , Bn} with n+ 1 branches. Application of one of the rules on B yields the tableau T' := {B', Bi, ... , Bn} for the (n), (3) and (Ax)- rule, T" := { B', B", Bi, ... , Bn} in case of the (U)-rule.

Once no more rules can be applied, we know which atoms are needed to close a saturated branch and can construct a minimisation function for A and T according to the rules in Figure 3. A propositional formula <p is called a minimisa­ tionfunctionfor A and T if A is unsatisfiable in every subset ofT containing the axioms which are true in an assignment making <p true. In our case axioms are used as propositional variables in <p. As we can identify unsatisfiability of A w.r.t. a set S of axioms with a closed tableau using only the axioms in S for unfolding, branching on a disjunctive rule implies that we need to join the functions of the appropriate sub-branches conjunctively. If an existential rule has been applied, the new branch B' might not necessarily be closed on formulas for both individuals. Assume that B' closes on the individual a but not on b. In this case minjunction(a, B, T) = 1_, which means that the related disjunct does not influence the calcula­ tion of the minimal incoherent TBox.

Based on the minimisation function min junction( a, { (a : A) 0 }, T) (let us call it <p) which we calculated using the rules in Figure 3 we can now calculate the MUPS for A w.r.t. T The idea is to use prime implicants of <p. A prime impli­ cant axi 1\ ... 1\ axn is the smallest conjunction of literals 5 implying <p [Quine, 1952]. As <pis a minimisation function every implicant of <p must be a minimisation function as well and therefore also the prime implicant. But this implies that the concept A must be unsatisfiable w.r.t. the set of axioms { axi, ... , axn}. As axil\ . . . I\ axn is the smallest implicant we also know that { axi, ... , axn} must be minimal, i.e. a MUPS. Theorem 4.1 captures this result formally.

5 Note that in our case all literals are non-negated axioms.

Theorem 4.1 Let A be a concept name, which is unsatisfi­ able w.r.t. an unfoldable ACC-TBox T The set of prime im­ plicants of the minimisation function minjunction(a, {(a : A) 0 }, T) is the set mups(T, A) of minimal unsatisfiability­ preserving sub-TBoxes of A and T

Proof: We first prove the claim that the propositional formula <p := minjunction(a, {(a: A) 0 }, T) is indeed a minimisa­ tion function for the MUPS problem w.r.t. an unsatisfiable concept A and a TBox T We show that a tableau starting on a single branch B := {(a : A) 0 } closes on all branches by unfolding axioms only, that are evaluated as true in an assign­ ment making <p true. This saturated tableau Tab* is a particu­ lar sub-tableau of the original saturated tableau Tab which we used to calculate min-function( a, {(a: A) 0 }, /),and it is this connection that we make use of to prove our first claim. Every branch in the new tableau is a subset of a branch oc­ curring in the original one and we define visible formulas as those labelled forinulas occurring in both tableaux. By induc­ tion over the rules applied to saturate Tab we can then show that each branch in the original tableau closes on at least one pair of visible formulas. If A is unsatisfiable w.r.t. T, the tableau starting with the branch {(a : A) 0 } closes w.r.t. T As we have shown that this tableau closes w.r.t. Ton visi­ ble formulas, it follows that Tab* is closed on all branches, which proves the first claim. By another induction over the application of the rules in Figure 3 we can prove that <p is a maximal minimisation function, which means that 1/J -+ <p for every minimisation function 1/J. This proves the first part of the proof; the first claim (and the argument from above) im­ plies that every implicant of a minimisation func~ion _ide~ti­ fies an unsatisfiability-preserving TBox, and max1mahty Im­ plies that prime implicants identify the minimal ones.

To show that the conjunction of every MUPS { axi, .. . , axn} is a prime implicant of minjunction(a, {(a : A) 0 } , T) is trivial as ax1 1\ . . . I\ axn is a minimisation function by defini­ tion. But as we know that minjunction(a, {(a: A) 0 }, T) is maximal we know that axil\· . . 1\axn-+minjunction(a, {(a: A) 0 } , T) which implies that axi 1\ ... I\ axn must be prime as otherwise { axi, ... , axn} would not be minimal. ·

Satisfiability in ACC is PSPACE-complete, and calculating MUPS does not increase the complexity as we can construct the minimisation function in a depth-first way, allowing us to keep only one single branch in memory at a time. However,

if rule = (n) has been applied to (a: C1 n C2)tabet and B' is the new branch return min-function( a, B', T) ; if rule = (U) has been applied to (a : C1 U C2)tabet and B' and B" are the new branches return min-function( a, B', T) 1\ min-function( a, B", T); if rule = (:3) has been applied to (a : :JR.C) 1 "bet, B' is the new branch and b the new variable return min-function( a, B', T) V min-function(b, B', T); if rule= (Ax) has been applied and B' is the new branch return min .function( a, B', T); if no further rule can be applied return: V (a , A)z E B , (a , ~A)· E 8 (1\axEx ax 1\ 1\axEy ax);

we calculate prime implicants of a minimisation function the size of which can be exponential in the number of axioms in the TBox. Therefore, approximation methods have to be considered in practice avoiding the construction of fully satu­ rated tableaux in order to reduce the size of the minimisation functions .

From MUPS we can easily calculate MIPS, but we need an additional operation on sets of TBoxes, called subset­ reduction. Let M = {7i, ... , Tm} be a set ofTBoxes. The subset-reduction of M is the smallest subset sr(M) ~ M such that for all T E M there is a set T' E sr(M) such that T' ~ T A simple algorithm for the calculation of MIPS for T now simply follows from Theorem 4.2, which is a direct consequence of the definitions of MIPS and MUPS.

Theorem 4.2 LetT be an incoherent TBox with unsatisfiable concepts D.T. Then, mips(T) = sr(UAEtlT mups(T, A)) .

Checking elements ofmips(T) for cores of maximal arity requires exponentially many checks in the size of mips(T). In practice, we therefore apply a bottom-up method searching for maximal cores of increasing size stopping once the arity of the cores is smaller than 2.

4.2 Algorithms for Concept Pinpointing

Calculating GITs depends on the definition ofrel(C, C'). In our case we will define this syntactic relation described in Footnote 4 including quantifier depth and polarity.

Definition 4.3 LetT be an unfoldable A.CC-TBox. A con­ cept C' is syntactically related to a concept C (notation: rel(C, C')) if C' ~ qsT(C) , where the set of qualified sub­ concepts, qsT(C), is defined inductively:

Moreover, qST(C) also contains .land T for all concepts C.

Note that we include terminological information from un­ folded TBox axioms in the definition of syntactic relatedness. This choice allows us to create smaller and more concise GITs but is non-essential. As the TBox is finite and cycle­ free, and as the concept size decreases in every recursion step, qsT( C) is finite. Therefore there is only a finite set of con­ cepts related to any axiom A~C. A simple algorithm to cal­ culate GITs for an incoherent unfoldable A.CC-TBox Tis therefore:

For all MIPS ME mips(T) (with lmips(T)I = m)

1. Let T' be the TBox where all axioms A~C (/. M in T have been replaced by A~T.
2. Calculate different TBoxes T" where an arbitrary num­ ber of axioms Ai ~Ci E M have been replaced in T' by generalised axioms Ai~C~, i.e., where q E qsT(Ci) andCi ~ CI forsomei E {l, ... ,m}.
3. Return those incoherent TBoxes T" with minimal syn­ tactic generalisations according to the subsumption rela­ tion, and the size or number of concept names.

The algorithm described above is a naive algorithm which might not terminate in reasonable time on large terminolo­ gies with complex definitions as the number of syntactically related concepts for a given concept C is exponential in the size of C. A more efficient algorithm to calculate GITs is based on the fact that the syntactically related concepts can be created ordered by size starting with atomic concepts. To find GITs of minimal size we therefore apply a bottom-up strategy checking more and more complex terminologies for coherence in Step 2 stopping once we find an incoherent one.

5 Evaluation

The algorithms for axiom pinpomtmg have been imple­ mented in JAVA using RACER, which provides the set ofun­ satisfiable concepts. We evaluated the methods on both the anatomy fragment of DICE and the full DICE terminology. The fragment defines 529 concept names, 76 of which were unsatisfiable at first. 6 There are 5 MIPS containing 2 axioms each, but no axiom occurs in all MIPS. However, there is a core of arity 3 and size I: the axiom defining "central ner­ vous system" as a "nervous system". Note that the defini­ tion of "nervous system" is not contradictory but that its use is erroneous, e.g., the concept brain should be defined as a "part of' and not as a subconcept of the concept nervous sys­ tem. For each of the 5 MIPS minimal size GITs have been calculated, and they point to the exact position of the logi­ cal incorrectness. For the MIPS related to the error described in the introduction the minimal size GIT is simply Brain ~ NervousSystem n Body Part which, with the information that Body Part and NervousSystem are disjoint concepts, identifies the erroneous specification.

6 The high number of unsatisfiable concepts is due to the fact that the DL terminology for DICE has been created by migration from a frame-based terminological system. In order to make the semantics as explicit as possible a very restrictive translation has been chosen to highlight as many ambiguities as possible. Moreover, many con­ cepts were defined as sub-concepts of unsatisfiable concepts. See [Comet and Abu-Hanna, 2002] for details.

The full DICE terminology defines more than 2400 con­ cepts, of which more than 750 were unsatisfiable given the chosen migration method. Our implemented algorithms found the MUPS for all but 7 unsatisfiable concepts. In these seven cases the algorithm failed on the calculation of the prime implicants as we use a naive method in our current implementation. Based on the correctly calculated MUPS we approximated the set of MIPS which contained more than 350 TBoxes. We implemented an iterative approach, calculating the core Max of size l with maximal arity for mips(Tdice ), then the same for the remaining TBoxes in mips(Tdice) \Max and so on. This way we identified 10 cores of size 1 with an arity of25 to 10, covering almost half of the errors. For some of these cores we calculated GITs (by hand) which lead to the identification of a number of modelling errors. Even though the developed reasoning services are not yet fully integrated into the knowledge modelling environment, they are useful to pinpoint to the core of the logical contradiction, which is then investigated and eliminated by a domain expert.

Although the theoretical complexity of the MUPS problem is exponential in the size of the TBox the calculation of most MUPS for DICE was not problematic due to the relatively simple structure of the tableaux for the unsatisfiability proofs. Runtime analysis suggests that most CPU-time is spent by RACER identifying the unsatisfiable concepts, whereas com­ puting MUPS usually takes less than 10 percent of the overall runtime 7 .

6 Conclusion & Further Work

Explanation has been a research topic right from the first days of research in Artificial Intelligence (e.g., introducing TMS [Doyle, 1979] or Diagnosis [Reiter, 1987]) and The­ orem Proving (recently [Fiedler, 2001]). Despite a signifi­ cant interest in explanation of DL reasoning recently shown in the DL community (as [DIG, 2002] suggests) relatively lit­ tle work has been published on the subject. One exception is [McGuinness, 1996] where the author provides explanation for subsumption and non-subsumption. Her approach, based on explanation as proof fragments, uses structural subsump­ tion for CLASSIC and has been extended to A.CC-tableau reasoning in [Borgida et a!., 1999]. In contrast to this ap­ proach, our non-standard reasoning services for axiom and concept pinpointing focus on the reduction of information, and are independent of particular calculi or implementations.

We have introduced non-standard reasoning services facil­ itating the debugging of logically incoherent DL terminolo­ gies and algorithms to calculate them. Whereas the ideas for axiom pinpointing are more evolved and efficiently im­ plemented, only a relatively naive algorithm for concept pin­ pointing has been developed as yet. We are currently working on more efficient methods and alternative debugging services, and tests are under way on the DICE terminology.

7 For the full DICE terminology the overall runtime to calculate MIPS is currently about 40 minutes on a PC with a I GHz Pentium.

As our methods are developed for the particular applica­ tion of the DICE terminology some restrictions apply, most importantly to use A.CC and to consider unfoldable TBoxes, only. Neither is essential, and we conjecture that it is not too hard to extend our algorithms to find MIPS and GITs both for more expressive languages and for general TBoxes. Both is­ sues will be addressed in future investigations. Further work must also extend the application domain to other terminolo­ gies as we believe that the success we have with debugging DICE is not tied to the structure of this particular represen­ tation. Of particular interest should be applications related to the Semantic Web effort as our methods are particularly geared to support the debugging of existing terminologies and logical contradictions <.:a used by migration or merging of ter­ minologies.