Description Logics with Refreshing Variables. Concepts with variables (also called patterns) have been introduced in description logics since the midnineties [1, 10, 12] and led to a highly interesting research stream on the so-called non-standard reasoning, speci cally matching [6, 4] and uni cation [3]. As an example to brie y recall these notions, consider the following pattern: P1 Y u 9x:U niversity. Here, the variable x, called a role variable, takes its values from a set of possible atomic role names while the variable Y , called concept variable, takes its values among all possible concept descriptions. The concept description F emaleStudent P ersonuF emaleu9studyIn:U niversity matches the pattern P1. Indeed, if we consider a variable substitution that assigns the role studyIn to the variable x (i.e., (x) = studyIn) and assigns the concept description P erson u F emale to the variable Y (i.e., (Y ) = Person u Female), the concept (P1) (Y )u9 (x):U niversity obtained by replacing the variables x and Y by their respective values given by the substitution , is equivalent to the concept F emaleStudent. Hence, given a description C and a pattern P , a matching problem modulo equivalence (respectively, modulo subsumption) asks then whether there is a variable substitution such that C (P ) (respectively, C v (P )). Uni cation extends matching to the case where C is itself a pattern. Matching and uni cation have shown to be useful to lter unimportant aspects of large concepts [11], to detect redundancies in knowledge bases [7] and to support integration of knowledge bases [9]. Most of existing works regarding these two inference tasks deal with concept variables. Matching between F L0 terms with concept variables has been shown polynomial [1] while considering general TBox induces a blow up in complexity leading to EXPTIME [4]. On the other hand, matching in E L in presence or not of TBox is NP-complete. Uni cation in F L0 is EXPTIME-complete [7] while it is NP-complete in E L [5] and stays in NP for E L in presence of cycle-restricted TBoxes [3]. Role variables have been studied in [10, 11] for F L0. In [11], it has been shown that matching between F L0-terms with both concept and role variables is NP-Complete. Our work explores a new class of variables, called refreshing variables. More precisely, we support cyclic pattern de nitions and consider a new semantics for variables, called refreshing semantics in contrast to the classical (non refreshing ) semantics used in the literature. The main di erence between these two kinds of semantics lies in the valuation of variables that appear in the scope of a terminological cycle. A classical semantics requires to have a unique val-
uation of such variables while a refreshing semantics enables to assign di erent values for the same variable for each unfolding of a cycle. To illustrate the refreshing semantics, let us consider the following pattern Academic P erson u 9x:U niversity u 9y:Academic. According to this pattern, an Academic is de ned as a person having certain relationships with a U niversity and an Academic. Consider now the following partial unfolding of this pattern : Academic P erson u 9x1:U niversity u 9y1:(9x2:U niversity u 9y2:Academic) where indices are used to distinguish di erent occurrences of the same variable during the unfolding process. In classical semantics, a variable substitution assigns a unique value to all the occurrences of a given variable x (i.e., (xi) = (xj ); 8i; j). In contrast, refreshing semantics permits substitutions that may assign di erent values to di erent occurrences of a given variable (i.e., we may have (xi) 6= (xj ) for i 6= j). Intuitively, refreshing semantics enables a variable to be refreshed at each cycle of the unfolding process.
Considering matching or uni cation in the context of a refreshing
semantics leads to the following practical bene ts: (i) some matching (or uni cation)
problems that are unsolvable under the classical semantics have a solution under
the refreshing semantics, and (ii) for some matching (or uni cation) problems,
the refreshing semantics provides solutions that are more general w.r.t. the
subsumption relation and hence are of practical interest [
9f ormerly:F renchP hDStudent
We consider the following classical matching problem w.r.t a Tbox in the setting of the E L description logic: Doctor ?T Academic. In this setting, x; y are non refreshing role variables and hence they have a nite number of possible values (i.e., the role names that appear in the Tbox T ). One can check that none of the possible substitutions leads to a solution to our matching problem. Hence, the matching problem Doctor ?T Academic is unsolvable in the context of a non refreshing semantics. This is not the case, however, if we consider refreshing semantics (i.e., when x and y can be refreshed). Let xi denotes the ith occurrence of a variable x during an unfolding process. Under refreshing semantics, it is then possible to de ne a variable substitution that alternates the values assignment to x and y as follows : { (xi) = getPhDIn and (yi) = formerly, for odd i, and { (xi) = studyIn and (yi) = supervisedBy for even i.
The resulting concept, (Academic) P erson u 9getP hDIn:U niversity u 9f ormerly:(9studyIn:U niversity u 9supervisedBy:(:::)) matches the de nition of Doctor (i.e., Doctor T (Academic)). Therefore, the matching problem Doctor ?T Academic is unsolvable under the non refreshing semantics while it has a solution under the refreshing semantics. Note that, reasoning (e.g., matching or uni cation) in description logics with refreshing variables is not an easy Weak Subsumption in the EL-Description Logic with Refreshing Variables task. Indeed, as illustrated in our example, it amounts to reasoning on patterns with an in nite number of variables.
To illustrate the second issue, we consider the pattern Academic2 P ersonu 9getP hdIn:X u9f ormerly:(P ersonu9studyIn:X u9supervisedBy:Academic2) and the following matching problem modulo subsumption: Academic2 v?T FrenchDoctor. Under the non refreshing semantics, the best matcher is given by the substitution de ned as: (X) = F renchU niv which leads to (Academic2) v F renchDoctor (and more precisely, (Academic2) @ F renchDoctor). Under the refreshing semantics, it is possible to nd a solution that is more general than (Academic2). Such a solution is given by a substitution de ned as follows: (X1) = F renchU niv and (Xi) = U niversity, for i > 1. The resulting concept would achieve equivalence with FrenchDoctor. This later solution is interesting since it is closer to the original concept F renchDoctor. Indeed, we have: (Academic2) @ (Academic2) F renchDoctor.
Our goal is to study a new reasoning mechanism, called weak-subsumption,
in description logics with refreshing variables. Given a description logic L, weak
subsumption is informally de ned as follows: let T be an L-TBox and let P; Q
be two L-patterns with variables. Then, P is weakly subsumed by Q i there
exists two substitutions 1 and 2 s.t 1(P ) is subsumed by 2(Q).
Preliminary Results. In [
Our main technical result is to show that testing weak-subsumption between
E LRV -patterns is EXPTIME-complete. Our reasoning procedure to test weak
subsumption between E LRV concepts exploits the link between subsumption
and the simulation relation between the so-called description graphs introduced
in [