We investigate the extension of Description Logics (DL) with a notion of “substitution”. Substitutions naturally arise when reasoning about programs which modify graph structures that are characterized by DLs. They constitute also a means to express concept and role modifications such as addition or deletion of individuals (respectively, pairs of individuals) to or from concepts (respectively, roles). After a formal definition of substitutions, we conduct a systematic study of a wide range of DLs with the purpose of proving or disproving conservativity of an extension of the respective DL with substitutions. The resulting classification is a gauge of the expressiveness of description logics and their adequacy for reasoning about change of graph structures.
1 CNRS and University of Grenoble Alpes 2 Universite´ de Toulouse / IRIT
Motivation: Description Logics (DLs) [
These logics differ by their expressive power and complexity1. Besides their static
descriptions, Knowledge bases may also be amenable to evolve. Such evolutions can
be the result of arbitrary programs. This paper has been motivated by the problem of
evolving KBs and the means that may be used to guarantee their formal descriptions.
Actually, by using a program logic following a Hoare style, see e.g. [
One of the questions explored in this paper is therefore: which DLs that have proven
to be adequate for knowledge representation can also be used for reasoning about
change, particularly to specify assertions such as P re and P ost and the underlying
Hoare calculus? In other words, how do classical DLs behave when used in a Hoare
calculus where substitutions arise in the computation of assertions? Recall that to every
elementary action of a program P , is associated a substitution [
A result of this paper is that all the families of description logics considered here can be extended to a decidable program logic, with the aid of substitutions. In some cases, these substitutions are conservative (and can therefore be eliminated within the ? This research has been supported by the Climt project (ANR-11-BS02-016) 1 see, e.g., http://www.cs.man.ac.uk/~ezolin/dl/ logic itself), and in some cases, this is impossible. Providing rigorous proofs of this latter fact is one of the main aims of this paper.
Overview of the approach: Although DLs come in numerous flavors allowing to cater
to diverse needs in term of expressiveness and complexity, they are tailored to represent
”static” knowledge, that is to represent and reason about a given state of knowledge.
The need for ways to make knowledge evolve has lead to an increasingly rich field of
knowledge update and action [
The work presented in this paper is inspired by the desire to take advantage of notions of program verification.In a program verification framework, one would compute the weakest precondition associated to a postcondition P ost, say wp(P rog; P ost). wp(P rog; P ost) would then be the condition that the original knowledge base has to satisfy to be sure that we reach a knowledge base satisfying the postcondition. Computation of weakest preconditions is done stepwise, starting from the postcondition and by considering the effect of each instruction starting from the last one and going back to the first instruction. The effect of an elementary instruction, say inst, on a postcondition, say Q, is reflected by a so-called substitution, say . Substitutions are classic and central elements of Hoare Logic and the most intuitive way in such a framework to translate into logic the effect of an action. Such an approach is quite unusual in the graph transformations framework though and being able to effectively express substitutions in the case of such transformations is of utmost importance.
The task of proving the correctness of a program can thus, through the use of substitutions, be reduced to the task of determining whether or not a formula is valid. The main issue is that most logics for which there are results on the decidability or the complexity of the validity problem do not explicitly consider substitutions as a constructor. The other way round, most logics with substitutions have received very little attention and there are thus few results on their validity problems.
Note that our goal is to inspect logics and classify them depending on whether or not adding substitutions to them modifies their expressive power. We do not claim to produce efficient ways to prove that a program is correct.
The paper is structured as follows: We recall in Sect. 2 different DLs starting from ALC and introduce their extensions with substitutions. In Sect. 3 , we provide a family of DLs which are closed under substitutions, whereas Sect. 4 shows that some other DLs are not closed under substitutions. Sect. 5 discusses the case of the logic ALCO and some of its extensions. We conclude in Sect. 6. 2
In this section, we define the syntax of the description logics we consider. We start by the elementary logic ALC. ALC, and all of its extensions, are defined using a signature (C, R, I) where C is a set of concept names, R is a set of role names and I a set of individuals.
C ::= ? (empty concept) j A (concept name) j : C (negation) j C u C (conjunction) j 9R:C (exists) where c is a concept name (2 C) and R is a role. As usual, > is used for : ?, C t D for :(:C u :D) and 8R:C for :9R::C.
As an example, 9R: (c t 8R: c) is an ALC-concept satisfied by nodes having an R-neighbour which satisfies c or whose R-neighbours satisfy c.
Concepts are the basic building block of DL formulae. Usually, the problem we are interested in looks like: “Is concept C valid (or satisfiable) given some axioms?”. These axioms are split into ABoxes and TBoxes.
Definition 3 (ABox and TBox). An individual assertion IA is defined as: IA ::= a : C (concept assertion) j a = b (equality) j a 6= b (inequality) j (a; b) : R (positive role assertion) j (a; b) : :R (negative role assertion) where C and D are concepts, R is a role and a and b are individuals. An ABox is a finite set of individual assertions. A TBox is a finite set of concept inclusions of the form
Each extension of ALC we are going to focus on adds new concept or role constructors. Each constructor is associated to a letter added to the name of the logic2. The constructors that we consider in this paper are Q, O, Self , I, @ and U , defined as follows:
Q ( n R C) (at least) O fag (nominal) Self 9S:Self (local reflexivity) I R (inverse role) @ @aC (concept assertion) U U (universal role) where a is an individual, S is a role, different from U, R is a role and C is a concept. (< n R C) is a shorter way to write :( n R C).
From now on, as there are numerous logics that are considered, we will introduce new notations. ALCL1 : : : Ln[Ln+1 : : : Lm] denotes the family of description logics with all constructors corresponding to L1 : : : Ln and any combination of those corresponding to Ln+1 : : : Lm.
? = ; (C u D)I = CI \ DI (9R:C)I = f 2 Ij#(RCI ( )) 1g (9R:Self )I = f 2 Ij( ; ) 2 RIg ( n R C)I = f 2 Ij#(RCI ( )g) ng (R )I = f( ; 0) 2 I Ij( 0; ) 2 RIg Definition 4 (Interpretation). An interpretation I is a pair f I; Ig where I is the universe (set of elements) and I, the valuation, is a function that maps each concept name to a subset of I, each role name to a subset of I I and each individual to an element of I.
Below, we define the valuation of roles and concepts:
I (: C)I = InCI, written CI (U)I = I I fagI = faIg (@aC)I = I if aI 2 CI ; otherwise 2 see, e.g., http://www.cs.man.ac.uk/~ezolin/dl/ where RCI ( ) is f 0 2 V .
j( ; 0) 2 RI ^ 0 2 CIg and #(V ) stands for the cardinal of Definition 5 (Model). We say that an interpretation I satisfies an assertion a : C (resp. a = b, a 6= b, (a; b) : R, (a; b) : :R) if aI 2 CI (resp. aI = bI, aI 6= bI, (aI; bI) 2 RI, (aI; bI) 62 RI). We say that an interpretation I is a model of an ABox
inclusion C v D if CI DI. We say that an interpretation I is a model of a TBox
a concept C if CI 6= ;.
Now we introduce the notion of substitution that allows one to modify the valuation of concepts and roles by adding or removing elements.
Definition 6 (Substitution). Given a role name R, a concept name c and individuals a and b, a substitution is defined as follows: ::= (empty substitution) j R := R (a; b) (deletion of role instance) j R := R + (a; b) (insertion of role instance) j A := A a (deletion of concept instance) j A := A + a (insertion of concept instance)
Substitutions define an additional concept constructor. We use in logic names to signify that substitutions are allowed as constructors. It is important to note that this constructor can only be used to build the concept part of the considered formulae and not in assertions nor in concept inclusions.
C (explicit substitution) where L is a concept of L and is a substitution.
For instance, C[R := R + (a; b)] means that C is satisfied after adding the pair (a; b) to the valuation of R. The interpretation is thus modified accordingly. Definition 8 (Valuation of explicit substitutions). Let A be a concept name, a and b be individuals, C be a concept and R be a role name, the valuation of explicit substitutions is defined as follows: – (C )I = CI – (C[A := A + a])I = CK where K = I, 8B 2 C; B 6= A; BK = BI, 8R 2 R; RK = RI, 8o 2 I; oK = oI and AK = AI [ faIg. – (C[A := A a])I = CK where K = I, 8B 2 C; B 6= A; BK = BI, 8R 2 R; RK = RI, 8o 2 I; oK = oI and AK = AI \ faIg – (C[R := R + (a; b)])I = CK where K = I, 8A 2 C; AK = AI, 8P 2 R; P 6=
R; P K = P I, 8o 2 I; oK = oI and RK = RI [ f(aI; bI)g – (C[R := R (a; b)])I = CK where K = I, 8A 2 C; AK = AI, 8P 2 R; P 6= R; P K = P I, 8o 2 I; oK = oI and RK = RI \ f(aI; bI)g The definition of the valuation for roles and concepts are conserved.
For instance, the valuation of ( 3 R C)[C := C + a][R := R (b; d)] is f 2 j#(f 0 2 j( ; 0) 2 RL ^ 0 2 CKg) 3g where CK = CI [ faIg and RL = RI \ f(bI; dI)g.
In this paper, we are interested in how the addition of substitutions to concepts affects the expressive power of a given Description Logic. For now, explicit substitutions can only be used in the definition of a concept (and thus are forbidden in ABoxes and TBoxes). To be more precise, ABoxes and TBoxes are usually allowed but their treatment is not what we are interested in. The reason why it is so is that, in the most expressive logics we consider, they can be simulated into the concept itself. For the least expressive logics, we look at whether or not allowing substitutions in ABoxes and TBoxes is sufficient to close the gap between the logics with and without substitutions.
To be able to evaluate the expressiveness of a logic, we define an equivalence relation on logics.
Definition 9 (Equivalence). Two concepts C and D are said to be equivalent if, for every interpretation I, CI = DI. A logic L1 is at most as expressive as a logic L2 wrt. concepts written L1 C L2 if every concept in L1 has an equivalent concept in L2.
Definition 10 (Closure under substitutions). A logic L is said to be closed under substitutions if L and L are concept-equivalent. 3
In this section we prove that DLs in ALCU O[QI@Self ] are closed under substitutions. Let us notice first that in ALCQU IO@Self some constructs are rendundant. In particular, when a DL includes O (nominals), assertions can be rewritten as concept inclusions. When a DL includes U (universal role), concept inclusions can be rewritten as mere concepts. Additionally, as the concept @aC is equivalent to the assertion a : C, all @-concepts can be removed in presence of both O and U . Finally, in presence of both O and @, all ABox assertions can be rewritten as concepts.
As both O and U are part of ALCQU IO@Self , we consider for this chapter that the TBox and the ABox are empty.
The proof of Theorem 1 is done by providing a terminating rewriting system consisting of rules which translate concepts of ALCQU IO@Self into concepts of ALCQU IO@Self (without substitutions). The idea is to associate to each possible concept constructor coupled with a substitution constructor an equivalent substitutionfree concept 0. The rules thus have the form: . is a concept of ALCQU IO@Self equivalent to such that substitutions are applied to “simpler” concepts. The rules are made so that they are orthogonal, thus ensuring that the rewriting system is confluent. Furthermore, we have shown that the considered rules constitute a terminating rewrite system. Therefore each formula rewrites to a unique substitution free normal form 0 ( 0).
Reporting all rules in here would be burdensome. Thus, to illustrate our point, we give the example of a rule for the ALCQU IO@Self -concept where the left-hand side is such that = ( n R C) and = [R := R (a; b)]. The right-hand side of the rule is a concept equivalent to , that is to say a concept such that for every node , satisfies iff satisfies ( n R C)[R := R (a; b)]. A possible concept for is given below : ((fag u 9U:(fbg u C[R := R (a; b)]) u 9R:fbg) )
( (n + 1) R C[R := R (a; b)])) u ((:fag t 8U:(:fbg t :C[R := R (a; b)]) t 8R::fbg) )
( n R C[R := R (a; b)])). – If the current node is a and b is an R-neighbour of a satisfying C[R := R (a; b)] (that is if fag u 9U:(fbg u C[R := R (a; b)]) u 9R:fbg is satisfied), then a will actually lose exactly one R-neighbour satisfying C after the substitution and it will thus have at least n remaining R-neighbours satisfying C after the substitution if it had at least n + 1 before and thus ( (n + 1) R C[R := R (a; b)]). – If either the current node is not a, b does not satisfy C[R := R (a; b)] or b is not an R-neighbour (that is if :fag t 8U:(:fbg t :C[R := R (a; b)]) t 8R::fbg is satisfied) then the removal of the edge (a; b) from R doesn’t affect the current node and thus ( n R C[R := R (a; b)]) must be satisfied.
By following the same proof technique used for Theorem 1, we can show that the following DLs are also closed under substitutions.
One can easily see from the one rule presented that the rewriting system risks causing an exponential blow-up in the size of the concept whose satisfiability is tested. In a worst case scenario, this could change the complexity of the satisfiability problem to 2NEXPTIME.
Another noteworthy observation is that the constructors @ and U are both used to access remote nodes. A quick check of the rules shows that all occurrences of U in T are of the form 9U:(fag u C) or 8U:(:fag t C) which are both equivalent to @aC. Hence:
4
In this section, we give a family of Description Logics which are strictly less expressive
than their extension with substitutions. In addition to the purely technical interest of
sorting logics depending on whether or not they have the property of being closed
under substitutions, studying less expressive logics is meaningful as the more expressive
logics are known to have a greater complexity[
We first consider the Description Logic ALC. ALC does not contain O nor U or @, thus ABoxes and TBoxes need to be used. Yet, we still require that no substitution appears in them.
More formally, to prove that the addition of substitutions to ALC strictly increases
its expressiveness, we use a result from [
and I2, for every bisimulation relation Z between I1 and I2, if an element x1 of I1 satisfies C and there is an element x2 of I2 such that x1Zx2, then x2 satisfies C. The same can be said for the satisfiability of ABox and T Box assertions. Definition 11 (Bisimulation). Given a signature (C, R, I) and two interpretations I1 and I2, a non-empty binary relation Z ( 1I 2I) is a bisimulation if it satisfies: (ALC1) d1Zd2 =) for all A 2 C; (d1 2 AI1 , d2 2 AI2 ) (ALC2) For all R 2 R; (d1Zd2 ^ d1RI1 e1 =) 9e2:d2RI2 e2 ^ e1Ze2) (ALC3) For all R 2 R; (d1Zd2 ^ d2RI2 e2 =) 9e1:d1RI1 e1 ^ e1Ze2) (ALC4) For all a 2 I; aI1 ZaI2
The idea of the proof of Theorem 2 consists in building an interpretation I1 such that an ALC-concept C containing substitutions holds and I2 bisimilar to I1 where C does not hold, thus proving that ALC is not as expressive as ALC . Fig. 1 depicts such interpretations.
Let’s check that I1 and I2 are bisimilar. As the only concept in C is A and R is empty, we verify the four axioms given in Def 11: (ALC1) d1Zd3 (d1 2 AI1 , d3 2 AI2 )X ALC2 R = ; X.
d2Zd3 (d2 2 AI1 , d3 2 AI2 )X (ALC2 R = ; X. (ALC3) R = ; X. (ALC4) aI1 ZaI2 X So I1 and I2 are bisimilar.
However, after the removal of the individual a from the concept A, the concept A still holds in d2 and does not hold in d3. This shows that there is no equivalent concept to A[A := A a] in ALC, which is enough to show that ALC is not closed under substitution.
One could wonder whether it is possible to find a way, using a TBox and an ABox to find something that would be equivalent to A[A := A a] in ALC. As the signature is (fAg; ;; fag), there are only few choices available as individual assertions or concept inclusions. A rapid analyses of these choices shows that there is no way to build an ABox nor a TBox that would provide an equivalent for A[A := A a].
In [
I1 ; there exists d0 2
I2 :dZd0 (U2) For all d0 2 I2 ; there existsd 2 I1 :dZd0 (I1) For all R 2 R; (d1Zd2 ^ d1R I1 e1 =) there exists e2:d2R I2 e2 ^ e1Ze2) (I2) For all R 2 R; (d1Zd2 ^ d2R I2 e2 =) there exists e1:d1R I1 e1 ^ e1Ze2) (O) For all a 2 I; d1Zd2 =) (d1 = aI1 , d2 = aI2 ) (Q) For all R 2 R; (d1Zd2 =) there is a bijection h : fyj(d1; y) 2 RI1 g ! fy0j(d2; y0) 2 RI2 g such that h Z. (IQ) For all R 2 R; (d1Zd2 =) there is a bijection h : fyj(y; d1) 2 RI1 g ! fy0j(y0; d2) 2 RI2 g such that h Z. (Self ) For all R 2 R; d1Zd2 =) (d1RI1 d1 , d2RI2 d2).
One could see that there is no rule for @. Actually, it is easy to prove that (ALC4) is enough for @.
The same example allows to prove that the DLs given in the following corollary are not closed under substitutions. The reader may verify that the axioms of bisimulations corresponding to these logics are satisfed by Z.
If a DL contains O, the example of Fig. 1 no longer is a counter-example because Z is not a bisimulation anymore. Indeed d2Zd3 but d3 = aI2 whereas d2 6= aI2 contradicting (O).
I1
Up to now, in this section, we have considered that the only part of the logic where substitutions where allowed was the concept whose satisfiability or validity we wanted to prove. Usually, the problem when DLs are considered is not the satisfiability or the validity of a concept, though, but whether or not the association of an ABox and a TBox can yield a model.
Another interesting question then is whether or not, for an ABox and a TBox both
possibly containing substitutions, it is possible to find a equivalent couple ABox-TBox
without substitutions. It is not. Indeed, the ABox (a : A)[A := A+b] is satisfied in only
two possible cases: either a : A before the substitution occurs or a = b. None of these
two cases can be expressed using TBox assertions and, using an ABox, you can only
express them as a Boolean ABox[
The case of ALCO The technique we used in the previous section cannot be applied directly in the case of the logic ALCO. Indeed, we can show the following result.
concepts are stable under ALCO-bisimulations.
To show this theorem, we assume given two interpretations I1 = f I1 ; :I1 g and I2 = f I2 ; :I2 g, x1 2 I1 and x2 2 I2 , Z an ALCO-bisimulation between I1 and I2 such that x1 Z x2 and prove for any ALCO -concept C, x1 2 CI1 , x2 2 CI2 .
As the complete proof is quite long, only a summary will be reported here.
We will mostly reuse the rewriting system intropduced in Sect. 3. Given an ALCO concept, the rules for atomic concepts give an equivalent ALCO-concept which is invariant for ALCO-bisimulations.
For the other rules, we will reason by induction. We assume that the concept whose invariance we want to show is (C t D) . The correct translation is C t D . Let’s prove that x1 2 (C t D )I1 ) x2 2 (C t D )I2 . We know that x1 2 (C t D )I1 . That is, x1 2 (C )I1 or x1 2 (D )I1 . Then, by induction, x2 2 (C )I2 or x2 2 (D )I2 . Thus x2 2 (C t D )I2 . The same way, we can show that x2 2 (C t D )I2 ) x1 2 (C t D )I1 . Showing (C u D) and (:D) are invariant is done mutatis mutandis.
The concepts using the constructors 9 and 8 are handled by going back to the definition of the interpretations and bisimulations. Let’s prove that (9R:C)[R := R+(a; b)] is invariant for ALCO-bisimulations. Once again, we start assuming x1 2 ((9R:C)[R := R+(a; b)])I1 . That means x1 2 fy j 9z such that (y; z) 2 (R[R := R+(a; b)])I1 ^z 2 (C[R := R + (a; b)])I1 g. Then, by replacing (R[R := R + (a; b)])I1 by its expression, one gets x1 2 fy j 9z such that (y; z) 2 (R [ f(a; b)g)I1 ^ z 2 (C[R := R + (a; b)])I1 g. Thus, x1 2 fy j 9z such that (y; z) 2 RI1 ^ z 2 (C[R := R + (a; b)])I1 g[faI1 ; bI1 2 (C[R := R+(a; b)])I1 g. As x1 belongs to at least one of those sets: either there exists z1 2 1 such that (x1; z1) 2 RI1 ^z1 2 (C[R := R+(a; b)])I1 which means that, by (ALC3), there exists z2 2 2 such that (x2; z2) 2 RI2 and, by induction, z2 2 (C[R := R + (a; b)])I2 . Thus x2 2 ((9R:C)[R := R + (a; b)])I2 , or x1 = aI1 and bI1 2 (C[R := R+(a; b)])I1 which means that, by (O), x2 = aI2 and, by induction, bI2 2 (C[R := R + (a; b)])I2 . Thus x2 2 ((9R:C)[R := R + (a; b)])I2 .
The exact same reasoning can be done in the other direction to prove that this is an equivalence.
Theorem 4 could lead us to think that the addition of substitutions to ALCO does not increase the expressiveness of the logic. This is not true. We propose below another kind of binary relations that are able to distinguish between ALCO and ALCO . The only difference is the last axiom (rALC4). To put it simply, it checks that the interpretation agree on the connected subgraph containing the root instead of agreeing on all connected subgraphs containing at least one nominal.
Definition 12. Given two interpretations I1 and I2, a rooted-bisimulation between I1 and I2 rooted in (x,x0) is a binary relation Z ( I1 I2 ) such that: (ALC1) d1Zd2 =) for all A 2 C; (d1 2 AI1 , d2 2 AI2 ) (ALC2) For all R 2 R; (d1Zd2 ^ d1RI1 e1 =) 9e2:d2RI2 e2 ^ e1Ze2) (ALC3) For all R 2 R; (d1Zd2 ^ d2RI2 e2 =) 9e1:d1RI1 e1 ^ e1Ze2) (rALC4) xZx0
bisimulations. Definition 13. A concept C is stable under rooted-bisimulations if, for any interpretations I1, I2, any rooted-bisimulation Z between I1, I2 rooted in (x,x0) and any y reachable from x, there exists y0 such that yZy0 and y 2 CI1 , y0 2 CI2 .
Once again, the proof is done by induction on the length of the concepts. It is obvious for concept names due to rule (ALC) and for nominals due to rule (O).
Fig. 2 provides a counter-example illustrating Theorem 6. The results of Theorems 5 and 6 can be extended to the logics in ALCO[IQSelf ].
Let’s check that I1 and I2 are (d1,d3)-bisimilar. As the only concept in C is A and there is no role in R, we verify the four axioms given in Def 12: (ALC1) d1Zd3 (d1 2 AI1 , d3 2 AI2 )X (ALC2)] R = ; X. (ALC3) R = ; X. (rALC4) d1I1 Zd3I2 X (O) d1Zd3 d1 = aI1 , d3 = aI2 X
So I1 and I2 are (d1,d3)-bisimilar.
I1
I2 d2 : b
Even in the presence of ABoxes and TBoxes, ALCO is still not closed under substitutions. Indeed, no ABox or TBox allows to express the concept (fag ^ 9R:A)[R := R + (a; b)] as it can only express one of the two possible “templates” of models at a time: the concept fag ^ 9R:A is satisfied or the concept fag together with the ABox b : A is satisfied. It is possible to express any of the two alone, the intersection of the two but not their union, which is the one we are looking for.
Once again, one may want to look at the problem of whether or not there exist an
equivalent couple ABox-TBox without substitutions for any ABox-Tbox with
substitutions. Once again, it is not possible. The ABox assertion a : (9R:A)[R := R + (a; b)]
yields the same possible models given previously. Once more the solution would be to
use a Boolean ABox [
We tackled the problem of adding substitutions to concepts in various DLs. We have described different situations where substitutions increase the expressive power of DLs and where they do not. In the latter situations, proving concept satisfiability in presence of substitutions can be carried out using the same proof procedures tailored for DLs without substitutions. However, when the expressive power of the logics are altered by substitutions, new proof procedures are to be devised. We have shown that the most expressive logics we considered are closed under substitutions. Moreover, as they allow to define the Abox and the Tbox directly as a part of the concept, it is possible to represent this way knowledge representation bases. On the other hand, logics without nominals, are strictly extended with the introduction of substitutions. Adding Abox or Tbox assertions is not enough to cover the gap in expressiveness either. Finally, logics with nominals are a borderline case where there is no equivalent formula without substitutions allowing to express the formula with substitutions but it is possible to find a disjunction of such formulae. A solution, that we didn’t consider here, for these logics would be to allow role constructors that would be the union and difference of roles.
This paper presents a systematic study of the closure under substitutions of various families of DLs. We are not aware of similar work in the literature.
This paper only concentrates on DLs. There are other approaches to deal with graph
or pointer transforming programs, such as separation logic [
DLs have been investigated in various areas with dynamic structures. For instance,
Dynamic Description Logics [
Knowledge update is a field that has been widely studied be it as database update
[
In [
Only few approaches use action languages with updates in the form of substitutions.
[
[
Last but not least, Hoare style program verification for graph transformation has
already been proposed in the literature (see, e.g., [