An Algorithm for Adapting Cases Represented in ALC

1 Introduction

Case-based reasoning (CBR [Riesbeck and Schank, 1989]) consists in reusing past experiences, called source cases, in order to solve a new problem, the target case. The CBR inference is made of a retrieval step, consisting is selecting a source case in a case base and an adaptation step, that consists in modifying the retrieved source case to solve the target case.

An approach to adaptation consists in using a belief revision operator, i.e., an operator that modifies minimally a set of beliefs in order to be consistent with some actual knowledge [Alchourrón et al., 1985]. The idea is to consider the belief "The source case solves the target case" and then to revise it with the constraints given by the target case and the domain knowledge. This has been studied for cases represented in propositional logic in [Lieber, 2007]. Then, it has been studied in a more expressive formalism, including numerical constraints and after that extended to the combination of cases (i.e., adaptation of several retrieval cases to solve a single target case) in this formalism [Cojan and Lieber, 2009].

In this paper, this approach to adaptation is studied for cases represented in ALC, an expressive description logic (DL). The choice of DLs as formalisms for CBR can be motivated in several ways. First, they extend the classical attribute-value formalisms, often used in CBR (see, e.g., [Kolodner, 1993]) and they are similar to the formalism of memory organization packets (MOPs) used in early CBR applications [Riesbeck and Schank, 1989]. More generally, they are designed as trade-offs between expressibility and practical tractability. Second, they have a well-defined semantics and have been systematically investigated for several decades, now. Third, many efficient implementations are freely available, offering services that can be used for CBR systems, in particular for case retrieval and case base organization.

The rest of the paper is organized as follows. Section 2 presents the DL ALC, together with the tableau algorithm, at the basis of its deductive inferences for most current implementations. An example is presented in this section, for illustrating notions that are rather complex for a reader not familiar with DLs. This tableau algorithm is extended for performing an adaptation process, as shown in section 3. Section 4 discusses our contribution and relates it to other studies on the use of DLs for CBR. Section 5 concludes the paper and presents some future work.

2 The Description Logic ALC

Description logics [Baader et al., 2003] form a family of classical logics that are equivalent to decidable fragments of firstorder logic (FOL). They have a growing importance in the field of knowledge representation. ALC is the simplest of expressive DLs, i.e., DLs extending propositional logic.

Syntax. Representation entities of ALC are concepts, roles, instances, and formulas.

A concept, intuitively, represents a subset of the interpretation domain. A concept is either an atomic concept (i.e., a concept name), or a conceptual expression of one of the forms ¬C, C ⊓ D, C ⊔ D, ∃r.C, and ∀r.C, where C and D are concepts (either atomic or not) and r is a role. A concept can be mapped into a FOL formula with one free variable x. For example, the concept

can be mapped to the first-order logic formula

The concept ⊤, which represents the whole interpretation domain is an abbreviation of A ⊔ ¬A, where A is an atomic concept.

A role, intuitively, represents a binary relation on the interpretation domain. Roles in ALC are atomic: i.e., role names. Their counterpart in FOL are binary predicates. The role appearing in (1) is ing.

An instance, intuitively, represents an element of the interpretation domain. Instances in ALC are atomic: i.e., instance names. Their counterpart in FOL are constants.

There are four types of formulas in ALC (1) C ⊑ D (C is more specific than D), (2) C ≡ D (C and D are equivalent concepts), (3) C(a) (a is an instance of C), and (4) r(a, b) (r relates a to b), where C and D are concepts, a and b are instances, and r is a role. Formulas of types (1) and (2) are called terminological formulas. Formulas of types (3) and (4) are called assertional formulas, or assertions.

An ALC knowledge base KB is a set of ALC formulas. The terminological box (or TBox) of KB is the set of its terminological formulas. The assertional box (or ABox) of KB is the set of its assertions.

For example, the following TBox represents the domain knowledge (DK) of our example:

meaning that the pome fruits are apples and pears. This is a simplification as actually there are other pome fruits than apples and pears.

In our running example, the only cases considered are the source and target cases. They are represented in the ABox:

Thus, the source case is represented by the instance σ, which is a pie with the types of ingredients pastry and apple. The target case is represented by the instance θ specifying that a pie without apple is requested.

Reusing the source case without adaptation for the target case amounts to add the assertion Source(θ). However this may lead to contradictions like here between ∃ing.Apple(θ) and ∀ing.¬Apple(θ): the source case needs to be adapted before being applied to the target case.

Semantics. An interpretation is a pair I = (ΔI, ·I ) where ΔI is a non empty set (the interpretation domain) and where ·I maps a concept C into a subset CI of ΔI, a role r into a binary relation rI over ΔI (for x, y ∈ ΔI, x is related to y by rI is denoted by (x, y) ∈ rI ), and an instance a into an element aI of ΔI.

Given an interpretation I, the different types of conceptual expressions are interpreted as follows:

This entails that ⊤I = (A ⊔ ¬A)I = ΔI .

For example, if PieI , AppleI , PastryI , and CinnamonI denote the sets of tarts, apples, pastries, and cinnamon, and if ingI denotes the relation "has the ingredient", then the concept of equation (1) denotes the set of the tarts with apples and pastries, but without cinnamon.

Given a formula f and an interpretation I, "I satisfies f" is denoted by I |= f. A model of f is an interpretation I satisfying f. The semantics of the four types of formulas is as follows: I |= C ⊑ D if CI ⊆ DI , I |= C ≡ D if CI = DI , I |= C(a) if aI ∈ CI , and I |= r(a, b) if (aI , bI ) ∈ rI .

Given a knowledge base KB and an interpretation I, I satisfies KB -I |= KB- if I |= f for each f ∈ KB. A model of KB is an interpretation satisfying KB. A knowledge base KB entails a formula f -denoted by KB |= f- if every model of KB is a model of f. A tautology is a formula f satisfied by any interpretation. "f is a tautology" is denoted by |= f. Two knowledge bases are said to be equivalent if every model of one of them is a model of the other one and vice-versa.

Inferences. Let KB be a knowledge base. Some classical inferences on ALC consist in checking if KB |= f, for some formula f. For instance, checking if KB |= C ⊑ D is called the subsumption test: it tests whether, according to the knowledge base, the concept C is more specific than the concept D, and thus is useful for organizing concepts in hierarchies (e.g., index hierarchies of CBR systems).

The concept classification consists, given a concept C, in finding the atomic concepts A appearing in KB such that KB |= C ⊑ A (the subsumers of C) and the atomic concepts B appearing in KB such that KB |= B ⊑ C (the subsumees of C). The instance classification consists, given an instance a, in finding the atomic concepts A appearing in KB such that KB |= A(a). These two inferences can be used during the case retrieval in a CBR system.

The ABox satisfiability consists in checking, given an ABox, whether there exists a model of this ABox, given a knowledge base KB. Some other important inferences can be reduced to it, for instance:

where a is a new instance (not appearing neither in C, nor in KB). ABox satisfiability is also used to detect contradictions. It can be computed thanks to the most popular inference mechanism for ALC presented below.

A classical deduction procedure in ALC: the tableau method. The following presentation of this procedure is inspired from [Baader et al., 2003], with some modifications that do not alter its results, but make it easier to extend into the adaptation algorithm.

Let KB be a knowledge base, T0, be the TBox of KB and A0, be the ABox of KB. The procedure aims at testing whether A0 is satisfiable or not, given KB.

Preprocessing. The first step of the preprocessing consists in substituting T0 by an equivalent T ′ 0 of the form {⊤ ⊑ K}, for some concept K. This can be done by first, substituting each formula C ≡ D by two formulas C ⊑ D and D ⊑ C. The resulting TBox is of the form {Ci ⊑ Di}1 ≤ i ≤ n and it can be shown that it is equivalent to {⊤ ⊑ K}, with

The second step of the preprocessing is to put T0 and A0 under negative normal form (NNF), i.e., by substituting each concept appearing in them by an equivalent concept such that the negation sign ¬ appears only in front of atomic concepts. It is always possible to do so, by applying, as long as possible, the following equivalences (from left to right): ¬¬C ≡ C, ¬(C ⊓ D) ≡ ¬C ⊔ ¬D, ¬(C ⊔ D) ≡ ¬C ⊓ ¬D, ¬∃r.C ≡ ∀r.¬C, and ¬∀r.C ≡ ∃r.¬C.

For example, the concept ¬(∀r.(¬A ⊔ ∃s.B)) is equivalent to the following concept under NNF: ∃r.(A ⊓ ∀s.¬B).

The TBox of DK given in equation (2) is equivalent to {⊤ ⊑ K} under NNF with

Main process. Given T0 = {⊤ ⊑ K} a TBox and A0 an ABox, both under NNF, the tableau method handles sets of ABoxes, starting with the singleton D0 = {AK0 }, with

Such a set of ABoxes D is to be interpreted as a disjunction: D is satisfiable iff at least one A ∈ D is satisfiable.

Each further step consists in transforming the current set of ABoxes D into another one D′ , applying some transformation rules on ABoxes: when a rule ϱ, applicable on an ABox A ∈ D, is selected by the process, then D′ = (D \ {A}) ∪ {A1 , . . . ,Ap } where the Ai are obtained by applying ϱ on A (see further, for the description of the rules).

The process ends when no rule is applicable.

An ABox is closed when it contains a clash, i.e. an obvious contradiction given by two assertions of the form A(a) and (¬A)(a). Therefore, a closed ABox is unsatisfiable. An open ABox is a non-closed ABox. An ABox is complete if no transformation rule can be applied on it.

Let Dend be the set of ABoxes at the end of the process, i.e. when each A ∈ D is complete. It has been proven (see, e.g, [Baader et al., 2003]) that with some adequate transformation rules, the process always terminates, and that A0 is satisfiable given T0 iff Dend contains at least one open ABox.

The transformation rules. There are four transformations rules for the tableau method applied to ALC: -→⊓, -→⊔, -→∀, and -→K∃ . None of these rules are applicable on a closed ABox. The order of these rules affects only the performance of the system, with the exception of rule -→K∃ that must be applied only when no other rule is applicable on the current set of ABoxes (to ensure termination). These rules roughly corresponds to deduction steps: they add assertions deduced from existing assertions. 1

1 To be more precise, each of them transforms a disjunction of ABoxes D into another disjunction of ABoxes D′ such that, given T0, D is satisfiable iff D′ is satisfiable.

The rule -→⊓ is applicable on an ABox A if this latter contains an assertion of the form (C1 ⊓ . . . ⊓ Cp)(a), and is such that at least one assertion Ck(a) (1 ≤ k ≤ p) is not an element of A. The application of this rule returns the ABox A′ defined by

The rule -→⊔ is applicable on an ABox A if this latter contains an assertion of the form (C1 ⊔ . . . ⊔ Cp)(a) but no assertion Ck(a) (1 ≤ k ≤ p). The application of this rule returns the ABoxes A1 , . . . , Ap defined, for 1 ≤ k ≤ p, by:

The rule -→∀ is applicable on an ABox A if this latter contains two assertions, of respective forms (∀r.C)(a) and r(a, b) (with the same r and a), and if A does not contain the assertion C(b). The application of this rule returns the ABox A′ defined by

The rule -→K∃ is applicable on an ABox if

• (i) A contains an assertion of the form (∃r.C)(a);
• (ii) A does not contain both an assertion of the form r(a, b) and an assertion of the form C(b) (with the same b, and with the same C and a as in previous condition);
• (iii) There is no instance c such that {C | C(a) ∈ A} ⊆ {C | C(c) ∈ A}. 2

If these conditions are applicable, let b be a new instance. The application of this rule returns the ABox A′ defined by

Note that the TBox T0 = {⊤ ⊑ K} is used here: since a new instance b is introduced, this instance must satisfy the TBox, which corresponds to the assertion K(b).

Remark 1 After the application of any of these rules on an ABox of D, the resulting D′ is equivalent to D.

Example. Let us consider the example given previously. Pretending that the source case represented by the instance σ can be applied to the target case represented by the instance θ amounts to identify these two instances, e.g., by substituting σ by θ. This leads to the ABox A0 = {Source(θ), Target(θ)} (with Source and Target defined in (4)). The figure 1 represents this process. The entire tree represents the final set of ABoxes Dend: each of the two branches represents a complete ABox A ∈ Dend. At the beginning of the process, the only nodes of this tree are Source(θ), Target(θ), and K(θ): this corresponds to D0 = {AK0 }. Then, the transformation rules are applied. Note that only the rule -→⊔ leads to branching. When a clash is detected in a branch (e.g. {Apple(a), (¬Apple)(a)}) the branch represents a closed ABox (the clash is symbolized with □). Note that the two final ABoxes are closed, meaning that {Source(θ), Target(θ)} is not satisfiable: the source case needs to be adapted for being reused in the context of the target case.

2 This third condition is called the set-blocking condition and is introduced to ensure the termination of the algorithm.

-→⊓

3 An Algorithm of Adaptation in ALC

As seen above, the reuse of the source case without adaptation may lead to a contradiction between Source(θ) and Target(θ). The adaptation algorithm presented in this section aims at solving this contradiction by weakening (generalizing) Source(θ) so as to restore consistency, to apply to the target case θ what can be kept from Source.

3.1 Parameters and Result of the Algorithm

The parameters of the algorithm are DK, Aσsrce , Aθtgt , and cost. Its result is D.

DK is a knowledge base in ALC representing the domain knowledge. In the running example, its ABox is empty, but in general, it may contain assertions.

The source and target cases are represented by two ABoxes that are satisfiable given DK: Aσsrce and Aθtgt , respectively. More precisely, the source case is reified by an instance σ and Aσsrce contains assertions about it. In the example above, Aσsrce contains only one assertion, Source(σ). Similarly, the target case is represented by an instance θ and Aθtgt contains assertions about θ (only one assertion in the example: Target(θ)).

The parameter cost is a function associating to a literal ℓ a numerical value cost(ℓ) > 0, where a literal is either an atomic concept (positive literal) or a concept of the form ¬A where A is atomic (negative literal). Intuitively, the greater cost(ℓ) is, the more difficult it is to give up the truth of an assertion ℓ(a).

The algorithm returns D, a set of ABoxes A solving the target case by adapting the source case: A |= Aθtgt and A reuses "as much as possible" Aσsrce . It may occur that D contains several ABoxes; in this situation, the knowledge of the system, in particular the cost function, is not complete enough to make a choice, thus it it up to the user to select an A ∈ D

3.2 Steps of the Algorithm

The algorithm is composed of the following steps:

Preprocessing. Let TDK and ADK be the TBox and ABox of DK. Let K be a concept under NNF such that TDK is equivalent to {⊤ ⊑ K}. ADK is simply added to the ABoxes:

Then, Aσsrce and Aθtgt are put under NNF.

Pretending that the source case solves the target problem. Reusing Aσsrce for the instance θ reifying the target case is done by assimilating the two instances σ and θ. This leads to the ABox Aθsrce , obtained by substituting σ by θ in Aσsrce . Let Aθsrce,tgt = Aθsrce ∪ Aθtgt . If Aθsrce,tgt is satisfiable given DK, then the straightforward reuse of the source case does not lead to any contradiction with the specification of the target case, so it just adds information about it. For example, let Aσsrce = {Source(σ)} given by equation (3), let Aθtgt = {Pie(θ), ing(θ, p), FlakyPastry(p)} (i.e., "I want a pie with flaky pastry"), and the domain knowledge be DK′ = DK ∪ {FlakyPastry ⊑ Pastry}, with DK defined in (2). With this example, it can be shown that Aθsrce,tgt is satisfiable given DK′ and it corresponds to an apple pie with flaky pastry.

In many situations, however, Aθsrce,tgt is not satisfiable given DK. This holds for the running example. The principle of the adaptation algorithm consists in repairing Aθsrce,tgt . "Repairing" Aθsrce,tgt means modifying it so as to make it complete and clash-free, and thus consistent. Removing clashes is not enough for that, the formulas from which they were generated should be removed too. This motivates the introduction of the AGraphs that extend ABoxes by keeping track of the application of rules (see below). Moreover, to have a more fine-grained adaptation, Aθsrce and Aθtgt are completed by tableau before being combined.

Applying the tableau method on Aθsrce and on Aθtgt , with memorization of the transformation rule applications. In order to implement this step and the next ones, the notion of assertional graph (or AGraph) is introduced. An AGraph G = (Nod (G), Edg (G)) is a simple graph whose set of nodes, Nod (G), is an ABox, and whose edges are labeled by transformation rules: if (α, β) ∈ Edg (G), then λG(α, β) = ϱ indicates that β has been obtained by applying ϱ on α and, possibly, on other assertions (λG is the labeling function of the graph G). The tableau method on AGraphs is based on the transformation rules =⇒⊓, =⇒⊔, =⇒∀, and =⇒K∃ . They are similar to the transformation rules on ALC ABoxes, with some differences.

The rule =⇒⊓ is applicable on an AGraph G if

• (i) G contains a node α of the form (C1 ⊓ . . . ⊓ Cp)(a);
• (ii) G ̸= G ′ (i.e., Nod (G) ̸= Nod (G ′ ) or Edg (G) ̸= Edg (G′ )) with G ′ defined by

Under these conditions, the application of the rule returns G ′ . The main difference between rule -→⊓ on ABoxes and rule =⇒⊓ on AGraphs is that the latter may be applicable to α = (C1 ⊓ . . . ⊓ Cp)(a) even when Ck(a) ∈ Nod (G) for each k, 1 ≤ k ≤ p. In this situation, Nod (G ′ ) = Nod (G) but Edg (G ′ ) ̸= Edg (G): a new edge (α, Ck) indicates here that α |= Ck(a) and thus, if Ck(a) has to be removed, then α has also to be removed (see further, the repair step of the algorithm).

The rules =⇒⊔, =⇒∀, and =⇒K∃ are modified respectively from -→⊔, -→∀, and -→K∃ similarly. They are detailed in figure 2.

The tableau method presented in section 2 can be applied, given the TBox {⊤ ⊑ K} and an ABox A0. The only difference is that AGraphs are manipulated instead of ABoxes, which involves that (1) an initial AGraph G0 has to be built from A0 (it is such that Nod (G0) = A0 and Edg (G0) = ∅), (2) the rules =⇒· are used instead of the rules -→·, and (3) the result is a set of open and complete AGraphs (which

• is empty iff G0 is not satisfiable given {⊤ ⊑ K}).

Let {Gi}1 ≤ i ≤m and {Hj}1 ≤ j ≤ n be the sets of open and complete AGraphs obtained by applying the tableau method respectively on A0 = Aθsrce and A0 = Aθtgt . If Aθsrce and Aθtgt are satisfiable, then m ̸= 0 and n ̸= 0. If m = 0 or n = 0, the algorithm stops and returns the value D = {Aθtgt }.

Generating explicit clashes from Gi and Hj. A new kind of assertion, reifying the notion of clash, is considered: the clash assertion □±A(a) reifies the clash {A(a), (¬A)(a)}. The rule =⇒□ generates them. It is applicable on an AGraph G if

• (i) G contains two nodes A(a) and (¬A)(a) (with the same A and the same a);
• (ii) G ̸= G′ with G ′ defined by

Under these conditions, the application of the rule returns G ′ . The next step of the algorithm is to apply the tableau method on each Gi ∪ Hj, for each i and j, 1 ≤ i ≤ m, 1 ≤ j ≤ n, using the transformation rules =⇒⊓, =⇒⊔, =⇒∀, A necessary condition for =⇒⊔ to be applicable on an AGraph G is that G contains a node α of the form (C1 ⊔ . . . ⊔ Cp)(a). If this is the case, then two situations can be considered:

• (a) G contains no assertion Ck(a) (1 ≤ k ≤ p). Under these conditions, the application of the rule returns the AGraphs G 1 , . . . , G p defined, for 1 ≤ k ≤ p, by

• (b) G contains one or several assertions βk = Ck(a) such that (α, βk) ̸∈ Edg (G). In this condition, =⇒⊔ returns the AGraph G ′ obtained by adding to G these edges (α, βk), with λG′ (α, βk) = =⇒⊔.

The rule =⇒∀ is applicable on an AGraph G if

• (i) G contains a node α1 of the form (∀r.C)(a) and a node α2 of the form r(a, b);

Under these conditions, the application of the rule returns G ′ .

The rule =⇒K∃ is applicable on an AGraph G if

• (i) G contains a node α of the form (∃r.C)(a);
• (ii) (a) Either G does not contain both r(a, b) and C(b), for any instance b;
• (b) Or G contains two assertions β1 = r(a, b) and β2 = C(b), such that (α, β1) ̸∈ Edg (G) or (α, β2) ̸∈ Edg (G);
• (iii) There is no instance c such that {C | C(a) ∈ Nod (G)} ⊆ {C | C(c) ∈ Nod (G)} (set-blocking condition, introduced for ensuring termination of the algorithm).

If condition (ii-a) holds, let b be a new instance. The application of the rule returns G ′ defined by

Under condition (ii-b), the application of the rule returns G ′ defined by

Figure 2: The transformation rules =⇒⊔, =⇒∀, and =⇒K∃ .

=⇒K∃ , and =⇒□. A difference with the tableau method presented above is that it was useless to apply rules on closed ABoxes (or closed AGraphs). Here, when a rule is applicable to an AGraph containing an assertion clash, it is applied, which may lead to several clashes in the same AGraph.

Remark 2 If an assertion clash □±A(a) is generated, then this clash is the consequence of assertions of both Gi and Hj , otherwise, it would have been a clash generated at the previous step of the algorithm (since these two AGraphs are complete and open).

Repairing the assertion clashes. The previous step has produced a non-empty set Sij of AGraphs, for each Gi ∪ Hj . The repair step consists in repairing each of these AGraphs Γ ∈ Sij and keeping only the ones that minimize the repair cost. 3 Let Γ ∈ Sij. If Γ contains no assertion clash, this involves that Gi ∪ Hj is satisfiable and so is Aθsrce,tgt : no adaptation is needed. If Γ contains δ ≥ 1 assertion clashes, then one of them is chosen and the repair according to this clash gives a set of repaired AGraphs Γ′ containing δ - 1 clashes. Then, the repair is resumed on Γ′ , until there is no more clash. 4 The cost of the global repair is the sum of the costs of each repair. In the following, it is shown how one clash of Γ is repaired.

The principle of the clash repair is to remove assertions of Γ in order to avoid this assertion clash to be re-generated by re-application of the rules. Therefore, the repair of all the assertion clashes must lead to satisfiable AGraphs (this is a consequence of the completeness of the tableau algorithm on ALC). For this purpose, the following principle, expressed as an inference rule, is used:

where β is an assertion and ϕ is a minimal set of assertions such that ϕ |= β (ϕ is to be understood as the conjunction of its formulas). Removing ϕ amounts to forget one of the assertions α ∈ ϕ: when card(ϕ) ≥ 2, there are several ways to remove ϕ, and thus, there may be several AGraphs Γ′ obtained from Γ. The relation |= linking ϕ and β is materialized by the edges of Γ. Thus, on the basis of (5), the removal will be propagated by following these edges (α, β), from β to α.

3 In our prototypical implementation of this algorithm, this has been improved by pruning the repair tasks when their costs exceed the current minimum.

4 Some additional nodes may have to be removed as some clashes may have been "hidden" by the set-blocking condition (=⇒K∃, condition (iii)). Set-blocking prevents the application of the rule =⇒K∃ on a node (∃r.C)(a) in an AGraph G if there exists some instance c such that {C | C(a) ∈ Nod (G)} ⊆ {C | C(c) ∈ Nod (G)}. This condition, that is needed to ensure termination, stands on the fact that, up to the renaming of instances, the set of nodes Na that would be generated from {C(a) | C(a) ∈ Nod (G)} in included in the set of nodes Nc generated from {C(c) | C(c) ∈ Nod (G)}. Thus, if Nc is clash-free, Na is also clash-free and needs no repair. Otherwise, Na needs to be computed to check if it contains clashes and make the appropriate repairs. This can be done by keeping track of the nodes of Nc that correspond to nodes of Na, the repairs over Nc must then be propagated to {C(a) | C(a) ∈ Nod (G)}.

Let β = □±A(a), the assertion clash of Γ to be removed. Let α+ = A(a) and α= ¬A(a). At least one of α+ and αhas to be removed. Hj being an open and complete AGraph, either α+ /∈ Hj or α- /∈ Hj (see remark 2). Three types of situation remain:

• If α+ ∈ Hj then α+ cannot be removed: it is an assertion generated from Aθtgt . Then, α- has to be removed.
• If α- ∈ Hj then α+ has to be removed.
• If α+ ̸∈ Hj and α- ̸∈ Hj, then the choice of removal is based on the minimization of the cost. If cost(A) < cost(¬A) then α+ has to be removed. If cost(A) > cost(¬A) then α- has to be removed. If cost(A) = cost(¬A), then two AGraphs are generated: one by removing α+, the other one, by removing α-.

If an assertion β has to be removed, the propagation of the removal for an edge (α, β) such that λG(α, β) ∈ {=⇒⊓, =⇒⊔, =⇒K∃ } consists in removing α (and propagating the removal from α).

Let β be an assertion to be removed that has been inferred by the rule =⇒∀. This means that there exist two assertions such that λG(α1, β) = λG′ (α2, β) = =⇒∀. In this situation, two AGraphs are generated, one based on the removal of α1, the other one, on the removal of α2 (when α1 or α2 is in Hj, only one AGraph is generated).

At the end of the repair process, a non empty set {Γk}1 ≤ k ≤ p of AGraphs without clashes has been built. Only the ones that are the result of a repair with a minimal cost are kept. Let Ak = Nod (Γk). The result of the repair is D = {Ak}1 ≤ k ≤ p .

Transforming the disjunction of ABoxes D. If A, B ∈ D are such that A |= B, then the ABoxes disjunctions D and D \ {A} are equivalent. This is used to simplify D by removing such A. 5 After this simplifying test, each A ∈ D is rewritten to remove the instances i introduced during a tableau process. First, the i's not related, neither directly, nor indirectly, to any non introduced instance by assertions r(a, b) are removed, meaning that the assertions with such i's are removed (this may occur because of the repair step that may "disconnect" i from non-introduced instances). Then, a "de-skolemization" process is done by replacing the introduced instances i by assertions of the form (∃r.C)(a). For instance, the set {r(a, i1), A(i1), s(i1, i2), ¬B(i2)} is replaced by {(∃r.(A ⊓ ∃s.¬B))(a)}. The final value of D is returned by the algorithm.

Example. Consider the example given at the end of section 2. Giving all the steps of the algorithm is tedious, thus only the repairs will be considered.

Several AGraphs are generated and have to be repaired but they all share the same clash □±Apple(a). Two repairs are possible and the resulting D depends only on the costs cost(Apple) and cost(¬Apple).

5 In our tests, we have used necessary conditions of A |= B based on set inclusions, with or without the renaming of one introduced instance. This has led to a dramatic reduction of the size of D, which suggests that the algorithm presented above can be greatly improved, by pruning unnecessary ABox generation.

If cost(Apple) < cost(¬Apple), then D = {A} with A equivalent to (Pie⊓∃ing.Pear)(θ). The proposed adaptation is a pear pie.

If cost(Apple) ≥ cost(¬Apple), then D = {A}, with Aequivalent toAθtgt . Nothing is learned from the source case for the target case.

3.3 Properties of the Algorithm

The adaptation algorithm terminates. This can be proven using the termination of the tableau algorithm on ABoxes [Baader et al., 2003]. Repair removes at least one node from finite AGraphs at each step, thus it terminates too.

Every A ∈ D satisfies Target constraints: A |= Aθtgt . And thus, D consists in the addition of some information to the target case.

Provided that Aθtgt is satisfiable, every A ∈ D is satisfiable. In other words, unless the target case is in contradiction with the domain knowledge, the adaptation provides a consistent result. When Aθsrce is not satisfiable, D is equivalent to {Aθtgt }. This means that when a meaningless Aθsrce is given, Aθtgt is not altered.

If the source case is applicable under the target case constraints (Aθsrce,tgt = Aθsrce ∪ Aθtgt is satisfiable) then D contains a sole ABox which is equivalent to Aθsrce,tgt : the source case is reused without modification to solve the target case.

The adaptation presented here can be considered as a generalization and specialization approach to adaptation. The ABoxes A ∈ D are obtained by "generalizing" Aθsrce into A′ : some formulas of Aθsrce are dropped for weaker consequences to obtain A′ thus A |= A′ , then A′ is "specialized" into A = A′ ∪ Aθtgt . Indeed, A |= B can be read as "A is generalized into B" since the set of models of A is included in the set of models of B.

4 Discussion and related work

Beyondmatching-based adaptationprocesses? There are two types of algorithms for the classical deductive inferences in DLs: the tableau algorithm presented above and the structural algorithms. The former is used for expressive DLs (i.e., for ALC and all the DLs extending ALC). The latters are used for the other DLs (for which at least some of the deductive inferences are polynomial).

A structural algorithm for the subsumption test KB |= C ⊑ D consists, after a preprocessing step, in matching descriptors of D with some descriptors of C.

This matching procedure is rather close to the matching procedures used by most of the adaptation procedures, explicitly or not (if the cases have a fixed attribute-value structure, usually, the source and target cases are matched attribute by attribute, and the matching process does not need to be made explicit).

Structural algorithms appear to be ill-suited for expressive DLs and tableau algorithms are used instead. The adaptation algorithm presented in this paper, based on tableau method principles, has no matching step (even if one can a posteriori match descriptors of source case and adapted target case).

From those observations, we hypothesize that beyond a certain level of expressivity of the representation language, it becomes hardly possible to use matching techniques for an adaptation taking into account domain knowledge.

Other work on CBR and description logics. Despite the advantages of using DLs in CBR, as motivated in the introduction, there are rather few research on CBR and DLs.

In [Koehler, 1996], concepts of a DL are used as indexes for retrieving plans of a case-based planner, and adaptation is performed in another formalism.

In [Salotti and Ventos, 1998], a non expressive DL is used for retrieval and for case base organization. This work uses in particular the notion of least common subsumer (LCS) to reify similarity of the concepts representing the source and target cases: the LCS of concepts C and D is the most specific concept that is more general than both C and D and thus points out their common features. Therefore the LCS inference can be seen as a matching process (that might be used by some adaptation process). In an expressive DL, the LCS of C and D is C ⊔ D (or an equivalent concept), which does not express anything about similar features of C and D.

To our knowledge, the only attempts to define an adaptation process for DLs are [Gómez-Albarrán et al., 1999] and [d'Aquin et al., 2005]. [Gómez-Albarrán et al., 1999] presents a modeling of the CBR life cycle using DLs. In particular, it presents a substitution approach to adaptation which consists in matching source and target case items by chains of roles (similar to chains of assertions r(a1, a2), r(a2, a3), etc.) in order to point out what substitutions can be done.

[d'Aquin et al., 2005] uses adaptation rules (reformulations) and multi-viewpoint representation for CBR, including a complex adaptation step. By contrast, the algorithm presented in this paper uses mainly the domain knowledge to perform adaptation: a direction of work will be to see how these approaches can be combined.

Other work on ontology change. Several studies on semantic web and ontology management focus on the problem of repairing ontologies and merging ontologies that may be contradictory. A review can be found in [Flouris et al., 2008]. In particular, [Kalyanpur et al., 2007] gives a "glass box" algorithm to compute the formulas to be removed in the purpose of ontology debugging [Kalyanpur et al., 2006]. This algorithm is similar to the tableau on AGraphs since it uses a tableau algorithm that keeps traces of the deductions. It would be interesting to compare precisely the two approaches. Note however that, unlike the approach presented in this paper, [Kalyanpur et al., 2006] only provides a subset of the initial knowledge base, ignoring the consequences that could be kept.

5 Conclusion and FutureWork

This paper presents an algorithm for adaptation dedicated to case-based reasoning systems whose cases and domain knowledge are represented in the expressive DL ALC. The first question raised by an adaptation problem is: "What has to be adapted?" The way this question is addressed by the algorithm consists in first pretending that the source case solves the target problem and then pointing out logical inconsistencies: these latters correspond to the parts of the source case to be modified in order to suit the target case. These principles are then applied to ALC, for which logical inconsistencies are reified by the clashes generated by the tableau method. The second question raised by an adaptation problem is: "How will the source case be adapted?" The idea of the algorithm is to repair the inconsistencies by removing (temporarily) some knowledge from the source case, until the consistency is restored. This adaptation approach can be classified as a transformational one since it does not use explanations or justifications associated with the source case, as would a derivational (or generative) approach do [Carbonell, 1986].

Currently, only a basic prototype of this adaptation algorithm has been implemented, and it is not very efficient. A future work will aim at implementing it efficiently and in an extendable way, taking into account the future extensions presented below. This might be done by reusing available DL inference engines, provided their optimization techniques do not interfere with the extension into an adaptation procedure. It can be noted that the research on improving the tableau method for DLs has led to dramatic gains in term of computing time (see, in particular, [Horrocks, 1997]).

The second direction of work will be to extend the algorithm to other expressive DLs. In particular, we plan to extend it to ALC(D), where D is the concrete domain of real number tuples with linear constraint predicates. This means that cases may have numerical features (integer or real numbers) and domain knowledge may contain linear constraints on these features. This future work will also extend [Cojan and Lieber, 2009].

The algorithm of adaptation presented above can be considered as a generalization and specialization approach to adaptation (cf. section 3.3). By contrast, the algorithm of [d'Aquin et al., 2005] is a rule-based adaptation, a rule specifying a relevant substitution to a given class of source case. A lead to integrate these two approaches is to use the adaptation rules during the repair process: instead of removing assertions leading to a clash, such a rule, when available, could be used to propose substitutes.

As written in the introduction, this algorithm follows work on adaptation based on belief revision, though it cannot be claimed that this algorithm, as such, implements a revision operator for ALC (e.g., it does not enable the revision of a TBox by an ABox). In [Cojan and Lieber, 2009], revisionbased adaptation is generalized in merging-based case combination. Such a generalization should be applicable to the algorithm defined in this paper: the ABox Aθsrce is replaced by several ABoxes and the repairs are applied on these ABoxes. Defining precisely this algorithm and studying its properties is another future work.