A Framework for Reasoning about Dynamic Axioms in Description Logics

1 Introduction

Nowadays, more and more digital information is stored but to make use of such data, it is common to employ logical formalisms to reason about knowledge and data. Description logics (DLs) [Baader et al., 2017] are among such formalisms that are intensively developed. In practical applications, the emerging data is changing rapidly. Hence, updating the knowledge bases (KBs) [Liu et al., 2006] in an efficient way is crucial for DLs in order to cope with real-life scenarios. Some effort was put to incorporate updates in DLs, e.g. in [Liu et al., 2006; De Giacomo et al., 2006; Drescher et al., 2009] or in [De Giacomo et al., 2017] for OBDA systems. Most of the cited works considered updates of the data layer (ABox) only, whereas we advocate that the logical rules used for reasoning may change too. Moreover, reasoning on updated ABoxes may require enriching the underlying DL language with new constructs, making unclear whether the existing DL reasoners can handle such new languages [De Giacomo et al., 2006]. Thus, there is still a need for novel DLs managing the updates on KBs.

In a broader perspective, the ability to specify in logical terms what are the effects of updating the models, is quite ubiquitous in computer science, with examples ranging from epistemic logics to specification languages for formal verification of programs. Prominent examples are logics of public announcements [Plaza, 1989] and separation logics [Reynolds, 2002]. The industrial success of separation logics, see e.g. [Distefano et al., 2019], is partly due to its ability to reason in a modular way on disjoint parts of the memory (by the means of the separating conjunction ∗ and the separating implication -∗). Roughly speaking, the operator ∗ decomposes the memory into two disjoint pieces and evaluates formulae on each piece separately. The operator -∗ asserts the behaviour of a heap after extending it with a new part satisfying certain properties. Though introduced in completely different contexts, some efforts on relating separation logics with DLs can be found in [Georgieva and Maier, 2005; Calvanese et al., 2014]. Many other logics concerning updates exist, e.g. sabotage and one-agent refinement modal logics [van Benthem, 2005; Bozzelli et al., 2013].

Motivations. Motivated by a lack of frameworks to specify evolution of interpretations in DLs, we would like to develop such formalisms by involving well-studied connectives from separation logics [Reynolds, 2002]. By contrast to the mentioned works on ABox updates, our framework aims at specifying how the satisfaction of GCIs or assertions evolves when the current interpretation is modified. Such an approach may benefit when ontologies are enriched by GCIs and assertions, either manually by the users or by automatic means. Herein, we plan to settle the foundations for such a framework.

Our contribution. We enrich KBs with dynamic axioms involving connectives from separation logics, that specify how the satisfaction of statements from the KBs evolves when the interpretation is decomposed or recomposed.

We introduce the notion of dynamic axioms (DAs) in KBs, endowing the set of interpretations with a binary composition operator ⊕, specifying that J = I1 ⊕ I2 holds when J can be decomposed into I1 and I2. In this work, the operator ⊕ affects roles only, namely it decomposes each role into two disjoint pieces while keeping domains and the interpretation of concept names within the obtained interpretations unchanged. Our DAs feature dynamic connectives ∗ and -⊛, respectively to decompose an interpretation and to augment it with a new disjoint interpretation. We distinguish the case of positive (i.e. negation-free) DAs. Throughout the paper, we study the KB consistency problem in the new setting.

For a logic L, we write LD (resp. LD+) to denote its extension with DAs (resp. positive DAs). We show that consistency for ALCD+ KBs remains EXPTIME-complete by a translation into a known extension of ALC. Moreover, the consistency for ALCD KBs is proved undecidable by a reduction from the concept satisfiability of ALC extended by rolevalue maps. Surprisingly we show that undecidability transfers to ELD. It is done by encoding concept negations within DAs. On the positive side, ELD+ is shown to be tractable, which makes it promising to implement.

2 A Framework with Dynamic Axioms

Basic DLs. We recall standard ingredients of the description logics (DLs) ALC and EL [Baader et al., 2017], and then we present our new framework for reasoning about dynamic axioms. We fix countably infinite mutually disjoint sets of individual names NI, concept names NC, and role names NR. The complex concepts of ALC are built from the grammar:

where A ∈ NC is a concept name and r ∈ NR is a role name. The semantics of ALC concepts is defined via interpretations I = (∆I , ·I ) composed of a non-empty set ∆I called the domain of I and a function ·I mapping individual names to elements of ∆I , concept names to subsets of ∆I , and role names to subsets of ∆I ×∆I . This mapping is extended to complex concepts, according to the clauses below:

We use ⊥ def= ¬⊤, ∀r.C def= ¬∃r.¬C, C ⊔ C ′ def= ¬(¬C ⊓ ¬C ′ ). An assertion is an expression of the form C(a), r(a, b) for a, b ∈ NI, C a complex concept and r ∈ NR. A general concept inclusion (GCI) has the form C1 ⊑ C2. A statement is either a GCI, a concept assertion C(a) or a role assertion r(a, b). The satisfaction of a statement is recalled below.

An ALC knowledge base K = (T ,A) consists of a finite set A (called ABox) of assertions and a finite set T (called TBox) of GCIs. An interpretation I satisfies the KB K=(T , A) (or I is a model of K, written: I |= K) if it satisfies all statements of A and T . A knowledge base K is called consistent if it has a model. EL is defined as the restriction of ALC to the concept constructor ⊓, to the existential restriction ∃, to ⊤ and to the concept names. Definitions of EL knowledge bases are lifted from ALC knowledge bases in an obvious way.

Reasoning with DBoxes. We introduce axioms specifying properties of updated interpretations. We enrich the set of interpretations I with a composition operator ⊕, i.e. a partial function ⊕ : I × I → I satisfying two natural properties:

(com) ⊕ is commutative, i.e. if I ⊕J is defined, then J ⊕I is defined and equal to I ⊕ J .

(assoc) ⊕ is associative, i.e. if I ⊕ (J ⊕ H) is defined, then (I ⊕ J ) ⊕ H is defined and equal to I ⊕ (J ⊕ H).

The function ⊕ is conceived as an operator to update dynamically the interpretations. For instance, when J = I1 ⊕ I2 holds, we say that adding I2 to the interpretation I1 leads to the new interpretation J , or alternatively, J can be decomposed into I1 and I2. In order to illustrate our approach, in this paper, only a specific composition operator is considered.

Whereas ALC KBs provide global constraints about the interpretations, we introduce dynamic boxes D (DBoxes) that specify how the satisfaction of statements evolve when the current interpretation is augmented or decomposed in the sense of the operator ⊕. For instance, I may not satisfy the GCI (∃r.⊤ ⊑ ∃s.⊤) but there is an additional interpretation J such that I ⊕ J is defined and satisfies ∃r.⊤ ⊑ ∃s.⊤. Typically, J contains new pairs of domain elements for the role s. Below, we define dynamic boxes as finite sets of dynamic axioms and the above situation can be specified by

The operator -⊛ in U1 -⊛ U2 states that there is an interpretation satisfying U1 and whose composition with the current interpretation is defined so that the resulting (augmented) interpretation satisfies U2. Similarly, we consider the operator ∗ so that U1 ∗U2 holds true when I can be decomposed into J1 and J2 (i.e. I = J1⊕J2), J1 satisfies U1 and J2 satisfies U2.

The set of positive dynamic axioms (PDAs) is defined by

Consequently, positive dynamic axioms are built from GCIs, assertions and are closed under ⊓, ⊔ and under the dynamic connectives ∗ and -⊛ (no negation). If the underlying DL is restricted to a subset of concept constructors (as for instance EL excludes ⊔), the set of positive dynamic axioms is restricted accordingly. In full generality, dynamic axioms (DAs) are defined as Boolean combinations of positive dynamic axioms:

A (resp. positive) dynamic box (DBox) D is defined as a finite set of (resp. positive) dynamic axioms. Note that negation ¬ does not occur in the scope of ∗ and -⊛ and can therefore occur only on the top of positive dynamic axioms.

We define the satisfaction relation |= between an interpretation and a dynamic axiom in the usual way for assertions, GCIs and for Boolean connectives. Here are the left clauses.

The dynamic connectives ∗ and -⊛ are exactly those used in separation logic [Reynolds, 2002; Vafeiadis and Parkinson, 2007] where ∗ is known as the separating conjunction and -⊛ is known as the septraction. A KB with dynamic axioms is a triple Kda = (T ,A,D) where (T ,A) forms a KB and D is a DBox. Similarly to the case of classical KBs, we write I |= Kda (and say that I is a model of Kda) if for all the statements α from (T ∪ A ∪ D), we have I |= α. A KB Kda is said to be consistent if it has a model. Thus, the consistency problem is defined also for the dynamic setting.

Below, we introduce the interpretation composition that is used throughout the paper. We write I = I1 + I2 whenever three interpretations I, I1 and I2 share the same domain, agree on the interpretation of the individual names and concept names, and for all r ∈ NR, we have rI = rI1 ⊎ rI2 , where ⊎ denotes disjoint union. Naturally, other operators could be investigated depending on the application domain.

Example 1. Let us consider a simple KB Kda = (T ,A,D) describing basketball teams and (possibly injured) basketball players. Let us assume that T contains the GCIs

∃has injury.Injury ⊑ Player, ∃is drafted.Team ⊑ Player,

∃has injury.Injury ⊓ ∃is drafted.Team ⊑ ⊥, essentially stating that no injured player can be drafted by a team. For the data layer, we suppose that the ABox contains has injury("Zion", "knee"). We can infer in a natural way that there is an evolution where the player "Zion" is drafted by the team "Pelicans" by asking for the consistency of Kda in the case where D contains the dynamic axiom

⊤ ∗ (⊤ -⊛ is drafted("Zion", "Pelicans") ⊓ dα∈T α). Notably, an interpretation I satisfying Kda can be decomposed into I ′ + J where I ′ |= has injury("Zion", "knee"). Then, J (the interpretation where "Zion" is not injured) is augmented so that is drafted("Zion", "Pelicans") holds, leading to the satisfaction of the dynamic axiom above. The PDA dα∈T α is added to guarantee that J satisfies the TBox.

Given a description logic L (in particular specifying a set of concepts and a set of roles), we write LD+ to denote its extension with positive dynamic axioms based on the concepts and roles from L, the concept constructors from L and based on (I, +). Similarly, we write LD to denote its extension with dynamic axioms and based on (I, +). We write CONS(L) to denote the knowledge base consistency problem for L. In the rest of the paper, we investigate the decidability status or the computational complexity of the knowledge base consistency problem for the logics ELD+, ELD, ALCD+ and ALCD.

3 A Toolkit for Positive Dynamic Axioms

In this section, we provide developments about the consistency of positive dynamic axioms U that are helpful to characterise the complexity of CONS(ALCD+) and CONS(ELD+). Below, L is either ALCD+ or ELD+. The culminating result is forthcoming Lemma 1 that states how the consistency of U can be expressed as the existence of a family of interpretations satisfying disjointness constraints.

Axioms as finite trees. Positive dynamic axioms can be represented as labelled finite binary trees using the standard tree encoding for terms. We recall that a binary tree Tree, which may contain nodes with (only) one child, is a nonempty subset of {1, 2}∗ such that, for all n ∈ {1, 2}∗ and i ∈ {1, 2}, n · i ∈ Tree implies n ∈ Tree and, n · 2 ∈ Tree implies n · 1 ∈ Tree. The elements of Tree are called nodes. The root of Tree is ε, i.e. the empty word. A (positive) dynamic axiom U can be represented by a labelled finite binary tree fU : TreeU → sub(U), where

• sub(U) is the set of subaxioms of U, defined as usually. For instance, for U = r(a, b)⊓(r(a, b)-⊛D(b)), we have sub(U) = {r(a, b), r(a, b) -⊛ D(b), D(b), U}.
• TreeU is the tree satisfying the following constraints:
• fU(ε) = U; if fU(n) is atomic, then n is a leaf,
• if fU(n) = U1⊗U2 for some binary ⊗, then n·1 and n·2 are in TreeU with fU(n·1)=U1 and fU(n·2)=U2.

Nodes associated with interpretations. Some nodes of TreeU will be associated with interpretations and constraints between those interpretations should be satisfied (see also the definition of DisjU below as well as Lemma 1). We write IntU to denote the smallest subset of TreeU such that ε ∈ IntU and n · 1, n · 2 ∈ IntU, for n having fU(n) of the form either U1 -⊛ U2 or U1 ∗ U2. For example, with U⋆ = (U1-⊛U2)⊓(U′1-⊛U′2 ), we have IntU⋆ ⊇ {ε, 1·1, 1·2, 2·1, 2·2}. Informally speaking, the nodes in IntU correspond to subaxioms of U that require the introduction of different interpretations. Thus, elements of IntU are implicitly associated with interpretations that relate them, as formally described below with the definition of DisjU. Given n ∈ TreeU, we write i(n) to denote the maximal prefix of n that is in IntU. With U⋆ above, we have i(1) = ε and i(2) = ε but i(1·1) = 1·1.

Disjointness axioms. We define the set of disjointness axioms DisjU using the nodes from IntU. As stated above, each element of IntU is associated with an interpretation. Because of this, these elements must satisfy expressions of the form n = n1 + n2, that reflect constraints between the corresponding interpretations. We overload the symbol '+' but we hope that this does not lead to any confusion. The set DisjU is the smallest set of disjointness axioms of the form n = n1+n2 with n, n1, n2 ∈ IntU such that

• if fU(n) = U1 ∗ U2 then i(n) = (n·1)+(n·2) ∈ DisjU,
• if fU(n) = U1 -⊛ U2 then (n·2) = (n·1)+i(n) ∈ DisjU,
• if n = n1 +n2 ∈ DisjU then n = n2 +n1 ∈ DisjU.

As the dynamic connectives ∗ and -⊛ have an existential flavour, satisfaction of U on an interpretation implies the existence of several interpretations constrained by compositions. The set of constraints between all these interpretations is represented by the set DisjU of disjointness axioms of the form n = n1 + n2. For instance, with U⋆ above, we have

More precisely, the sets DisjU and IntU are related as follows. A map g: IntU → I is said to be a complete witness for U iff for all n ∈ IntU, we have g(n) |= fU(n) and if n = n1 + n2 is in DisjU, then g(n) = g(n1) + g(n2). When g is a complete witness, g(ε) |= U. Not only g(ε) is a model for U but g determines completely how interpretations are decomposed or recomposed to guarantee the satisfaction of g(ε) |= U.

Lemma 1. Let U be a positive dynamic axiom in L. U is consistent iff there is a complete witness for U.

Note that the lemma can be applied to ELD+ and ALCD+. The "only if" part is obvious, since g(ε) |= U. For the "if" direction, the proof is by induction on the number of occurrences of either ∗ or -⊛ in U. Actually, we can show that if I |= U, then there is a complete witness for U with g(ε) = I. When U is ∗/-⊛-free, IntU = {ε} and DisjU is empty, which obviously leads to the conclusion. Otherwise, we perform a standard case analysis, the details are omitted.

4 Reasoning on ALC with Dynamic Axioms

We study the effect of adding dynamic boxes to ALC, resulting in description logics ALCD+ and ALCD.

4.1 Positive Dynamic Axioms for ALC

Below, we show that the consistency problem for ALCD+ is EXPTIME-complete, knowing that EXPTIME-hardness is inherited from ALC. The upper bound EXPTIME is obtained by internalising CONS(ALCD+) within the description logic ALCObself reg (a.k.a. ZO) for which knowledge base consistency is known to be in EXPTIME [Calvanese et al., 2009, Theorem 3.11]. The DL ZO extends ALC in many directions, but for our purposes, we recall the features that are essential for our reduction. ZO contains the universal role T (i.e. TI = ∆I ×∆I ), nominals {o} (i.e. {o}I is a singleton), and complex roles of the form r, ((r1 ∪r2) \ r), (r \ (r1 ∪r2)) and (r1 ∩ r2). For instance, expressing rI = rI 1 ⊎ rI 2 can be done with the following set of GCIs [r = r1 ⊎ r2] in ZO:

Let Kda = (T ,A,D) be an ALCD+ knowledge base with positive dynamic axioms. We write U⋆ to denote the positive dynamic axiom dα∈T ∪A∪D α and R to denote the set of role names occurring in U⋆ . Notice that Kda and the ALCD+ knowledge base (∅, ∅, {U⋆ }) are equiconsistent. It is time to take advantage of Section 3, and rely on the notions of IntU⋆ and DisjU⋆ therein introduced. The correctness of the construction is then guaranteed by Lemma 1. Given n ∈ IntU⋆, we write C n to denote the concept obtained from C but in which each role name r is substituted by a new role name rn (nothing is done on the concept names). Intuitively, given a complete witness g for U⋆ , the ZO interpretation of rn corresponds to the interpretation of r in g(n), consistently with the translation τ defined below. Assertions and GCIs are translated as usually in the presence of the universal role and nominals, whereas, as a peculiarity, the constraints about disjointness are stated in the target ZO TBox (see the last clause).

• τ(C(a), n) def= ∀T.(¬{oa} ⊔C i(n) ),
• τ(r(a, b), n) def= ∀T.(¬{oa} ⊔ ∃ri(n) .{ob}),
• τ(C ⊑ D, n) def= ∀T.(¬C i(n) ⊔Di(n) ),
• τ(U⊗V, n) def= τ(U, n· 1)⊗τ(V, n· 2) with ⊗ ∈ {⊔, ⊓}.
• τ(U⊗V, n) def= τ(U, n· 1)⊓τ(V, n· 2) with ⊗ ∈ {∗,-⊛}.

In the first three cases above, we rely on the fact that for every I = (∆I , ·I ), if C I ⊆ DI then (∀T.¬C ⊔D)I = ∆I , else (∀T.¬C ⊔D)I = ∅. The correctness of τ is stated below.

Lemma 2. Kda is consistent iff (T , A) is consistent with T = ⋃{[rn = rn1 ⊎rn2 ] | n = n1+n2 ∈ DisjU⋆ , r ∈ R} and A = {τ(U⋆ , ε)(a)}, where a is an arbitrary individual name.

In the proof, an interpretation satisfying (T , A) can be read as a complete witness for U and by Lemma 1 this entails the consistency of Kda. The converse direction is proved analogously. As the knowledge base in ZO is of polynomial-size in the size of Kda, we get the EXPTIME upper bound.

Theorem 1. CONS(ALCD+) is EXPTIME-complete.

4.2 Undecidability of CONS(ALCD)

We have seen that CONS(ALCD+) is EXPTIME-complete. By contrast, we show that adding negation at the top-level of PDAs leads to the undecidability of CONS(ALCD).

To start with, we consider the well-known extension of ALC with complex role inclusion axioms (CRIAs) of the form r1 ◦ · · · ◦ rn ⊑ s, where I |= r1 ◦ · · · ◦ rn ⊑ s iff rI 1 ◦ · · · ◦ rIn ⊆ sI . An RBox R is a finite collection of CRIAs. A concept C in ALC is satisfiable with respect to the RBox R iff there is I such that C I ̸= ∅ and for all α ∈ R, we have I |= α. Without regularity conditions on the RBox R, as considered in [Demri, 2001; Horrocks and Sattler, 2004], satisfiability of ALC concepts with respect to RBoxes made of arbitrary CRIAs is undecidable, see e.g. [Baldoni et al., 1998]. This is precisely the problem reduced to CONS(ALCD).

In order to encode a CRIA of the form r1 ◦ · · · ◦ rn ⊑ s into a dynamic axiom, we take advantage of auxiliary and fresh role names t, t1, t2 interpreted by the empty relation. Note that GCIs are atomic positive dynamic axioms and the GCI ∃t.⊤ ⊑⊥ holds only in interpretations I such that tI = ∅. To better reflect this, we use t ≡ ∅ to denote ∃t.⊤ ⊑⊥.

Let C be a concept in ALC written with role names occurring in {s1, . . . , sm}. As a first step for the translation, we introduce a negation-free dynamic axiom that is roughly equivalent to ¬(C ⊑⊥), i.e. it is satisfied only by interpretations I such that C I ̸= ∅. As it is negation-free, this dynamic axiom can be then used under the scope of -⊛ and ∗. In order to define such a dynamic axiom, we rely on an auxiliary role name t (not occurring in C). Then, we write 〈C ̸≡t⊥〉 to denote the (positive) dynamic axiom below:

Informally, under the assumption that t is interpreted vacuously, this formula ensures that at least one domain element satisfies C (because the disjoint new interpretation added through -⊛ can be defined so that every domain element points to some element satisfying C, via t).

Lemma 3. Let I be an interpretation such that tI = ∅ holds. Then C I is non-empty iff I |= 〈C ̸≡t⊥〉 holds.

Let us explain now how to encode a CRIA ⃗r ⊑ s, where ⃗r = r1 ◦ · · · ◦ rn, starting with its negation. We write V (⃗r, s, t1, t2) to denote the dynamic axiom below:

Let us consider an interpretation I such that tI1 = tI2 = ∅. Informally, this dynamic axiom simply states that when (d, e) ∈ (r1 ◦ · · · ◦ rn)I but (d, e) ̸∈ sI for some d, e, it is possible to augment tI1 with the interpretation J such that (d, f) ∈ (r1 ◦ · · · ◦ rn ◦ t1)I+J for some f but (d, f ′ ) ̸∈ (s ◦ t1)I+J for all f ′ . Also, observe that V (⃗r, s, t1, t2) uses negation only in ALC subconcepts (see ¬∃s.∃t1.⊤). The negation of V (⃗r, s, t1, t2) captures the concept of CRIAs as follows.

Consequently, given an ALC concept C, an RBox R and an individual name a, C is satisfiable with respect to R iff the following dynamic axiom in ALCD is consistent:

Theorem 2. CONS(ALCD) is undecidable.

5 Reasoning on EL with Dynamic Axioms

Below we investigate the effects of adding DAs to EL [Baader et al., 2005], ranging from tractability to undecidability.

5.1 Positivity for EL Leads to Tractability

Since assertions and GCIs are atomic PDAs, we can restrict ourselves to checking the consistency of a DBox. Negation is not allowed in EL, hence any EL KB is trivially consistent. However, the consistency problem of EL with positive DAs is no longer trivial. The following example demonstrates a way to obtain an inconsistent ELD+ knowledge base: U† = r(a, b)⊓(r(a, b)-⊛(⊤ ⊑ ⊤)). Inconsistency happens because, if I |= U†, then there are I ′ and I ′′ such that I ′ = I+I ′′ and I ′′ |= r(a, b). Moreover, as I |= U†, we have I |= r(a, b), which leads to a contradiction because I and I ′′ have disjoint role interpretations. Below, we show that the inconsistency of PDAs can only be due to a generalisation of such a disjointness constraint. We provide an algorithm to decide CONS(ELD+) in polynomial time and we give technical developments for proving the correctness of our complexity characterisation. The proof for the adequateness of our algorithm reveals to be the difficult part. Let U be a PDA. In Figure 1, we define a simple proof system (parameterised by U) that is essential to characterise the consistency status of U. It takes care of the disjointness axioms in order to conclude whether r(a, b) holds in the interpretation g(n). The calculus can derive either inconsistency ⊥ or expressions of the form either n: r(a, b) or n: ¬r(a, b) where n ∈ IntU (such expressions are also called statements below). The expression n: r(a, b) is intended to state that the interpretation associated with n satisfies r(a, b). We write U ⊢ n : r(a, b) when r(a, b) can be derived from the calculus with i(·) and DisjU computed from U (similarly for n: ¬r(a, b) and ⊥).

Before presenting the first property of the proof system, given a positive dynamic axiom U, we write RA(U) to denote the set of role assertions r(a, b) occurring in U. A complete snapshot with respect to U is a map f : IntU × RA(U) → {0, 1} such that for all r(a, b) ∈ RA(U),

• for all n ∈ IntU, U ⊢ n: r(a, b) implies f(n, r(a, b))=1, and U ⊢ n : ¬r(a, b) implies f(n, r(a, b)) = 0,
• f(n, r(a, b)) = f(n1, r(a, b)) + f(n2, r(a, b)) ≤ 1, whenever n = n1 + n2 ∈ DisjU.

Roughly speaking, a complete snapshot determines which pairs of domain elements are related by the interpretation of role names occurring in U (assuming the unique name assumption can be enforced, which will be the case). Obviously, f(n, r(a, b)) = 1 stands for g(n) |= r(a, b) where g is a complete witness. However, if r, a, and b occur in U but not the role assertion r(a, b), then there is no need to determine whether the interpretation associated with n satisfies r(a, b).

Lemma 5. Let U be a positive dynamic update s.t. U ̸⊢⊥. Then, there is a complete snapshot with respect to U.

The constructive proof of Lemma 5 consists in building the complete snapshot by first using the statements α such that U ⊢ α, then to set f(ni, r(a, b)) to 1 when n = n1 + n2 ∈ DisjU, f(n, r(a, b)) = 1, neither f(n1, r(a, b)) nor f(n2, r(a, b)) is defined, and ni ⪯ n3-i. After removing these ambiguities,

Figure 1: A simple proof system (i ∈ {1, 2}).

f is completed so that all the remaining values are 0. One can check that f is well-defined (in particular, it never happens that f(n, r(a, b)) = b with b ∈ {0, 1} and then set to f(n, r(a, b)) = (1 - b)) and f is a complete snapshot.

Lemma 6 (Correctness). Let U be a PDA s.t. U ⊢ n: r(a, b) (resp. U ⊢ n: ¬r(a, b)). For all complete witnesses g for U, we have g(n) |= r(a, b) (resp. g(n) ̸|= r(a, b)).

As expected, the proof is by induction on the length of the derivation of U ⊢ α and by taking advantage of Lemma 1. Consequently, if U ⊢⊥, then any knowledge base Kda = (T , A, D) such that U ∈ D is inconsistent. The proof system in Figure 1 is also complete, as stated below.

Lemma 7 (Characterisation). Let Kda = (T ,A,D) be a knowledge base with positive dynamic axioms. Kda is consistent iff ⊥ cannot be derived from U = dα∈T ∪A∪D α.

The assertions C(a) play no role in the proof system and therefore such assertions have no influence on the derivability of ⊥. This can be explained by the fact that any EL knowledge base (without dynamic axioms) is consistent. Our characterisation is simple as it is sufficient to check the derivability of ⊥. Though one direction of the proof is immediate from Lemma 6, the other direction requires to build safely an interpretation satisfying Kda. To do so, we collect all the assertions and GCIs occurring in U and we know that their conjunction is consistent, say in some I satisfying the unique name assumption for all the individual names occurring in U. From each domain element interpreting one such individual name, I is unravelled from it (using standard unravelling, see e.g. [Baader et al., 2017]) and copy a number of times polynomial in the size of U. Unravellings and copies are performed to preserve the initial satisfaction on I whereas the different copies are designed so that we have enough edges between the domain elements to apply the dynamic connectives ∗ and -⊛. The last step consists in deciding how to make true the assertions from RA(U). Lemma 5 is essential to make it in a consistent way. Indeed, the domain elements interpreting individual names occurring in U cannot be copied.

Theorem 3. CONS(ELD+) is in PTIME.

Given Kda = (T ,A,D), we build the equiconsistent PDA U = dα∈T ∪A∪D α. The computations of TreeU, IntU

and DisjU can be done in PTIME. Determining which statements are derivable from U can be also done in PTIME, by using a saturation algorithm and observing that the number of potential derivable statements is polynomial too.

5.2 Why Being Positive is Always Better

In this section, we show that CONS(ELD) is undecidable, by refining the arguments for the undecidability of CONS(ALCD). The main difficulty is to encode concept negation with the help of dynamic axioms (not necessarily positive) but when the concepts are restricted to those from EL. Technical developments are mainly based on those from Section 4.2. Below, we pinpoint the main differences.

We use an auxiliary vocabulary including the concept name Emp and the role names t, t1, t2, t3 that are reserved to define auxiliary concepts and dynamic axioms. W.l.o.g., we assume that these names do not occur in our instances of ALC augmented with CRIAs. Roughly speaking, in the translation, we force Emp to behave as ⊥ from ALC. Recall that ⊥ is not an EL concept, and it is heavily used in the undecidability proof from Section 4.2. To provide the right semantics of Emp, we introduce the dynamic axiom [Emp ≡t⊥] defined as [Emp ≡t⊥] def= ¬(⊤ -⊛ (⊤ ⊑ ∃t.Emp)).

Lemma 8. For every I, EmpI = ∅ iff I |= [Emp ≡t⊥].

So, for any arbitrary EL concept C, assuming that I |= [Emp ≡t⊥], we have I |= C ⊑ Emp iff C I = ∅. Moreover, Emp allows us to redefine in ELD 〈C ̸≡t⊥〉 introduced for ALCD : it is sufficient to substitute ⊥ with Emp. Indeed, assuming that the role names occurring in C are from R, and t ̸∈ R, then the ELD PDA below

satisfies the following lemma (analogous to Lemma 3).

Lemma 9. Let I be an interpretation such that EmpI = ∅ and tI = ∅. We have I |= 〈C ̸≡t⊥〉 iff C I ̸= ∅.

The dynamic axiom V (⃗r, s, t1, t2) introduced in Section 4.2 to express a CRIA ⃗r ⊑ s can be translated into ELD. Again, every occurrence of ⊥ is substituted with Emp. However, this is not enough as we need to deal with the negated concept ¬∃s.∃t1.⊤from V (⃗r, s, t1, t2) in Section 4.2. To do so, we introduce an auxiliary role name t3 and simply state that the first projections of (s ◦ t1)I and rI 3 are disjoint, but this is not the case for (r1◦· · ·◦rn◦t1)I and rI 3 . The resulting formula V (⃗r, s, t1, t2, t3) is defined as follows:

Lemma 10 (closely related to Lemma 4) states that this formula behaves as its homonymous formula in ALCD.

Lemma 10. Let I be an interpretation s.t. EmpI = ∅ and for every i ∈ {1, 2, 3} tIi = ∅. Let ⃗r ⊑ s be a CRIA, where ⃗r = r1 ◦ · · · ◦rn. Then, I |= ¬V (⃗r, s, t1, t2, t3) iff I |= ⃗r ⊑ s.

Now, let C be an ALC concept, R be an RBox and a be an arbitrary individual name. Let us assume for the moment that the assertion C(a) can be translated into an equivalent DA τ(C(a)) of ELD (shown below). Then, by relying on the formulae defined previously, we conclude that C is satisfiable with respect to R iff the DA in ELD below is consistent:

It remains to explain how to replace C(a) by a DA τ (C(a)) in ELD, while preserving the equivalence. We use the renaming technique [Scott, 1962] and rely on the presence of GCIs in DAs. Let D1, . . . , Dα be the subconcepts of C, say D1 = C. We use new concept names B1, . . . , Bα not appearing in C. The idea is to enforce a dynamic axiom Ui, for all i ∈ [1, α], that glues the new concept names in a way that Bi is shown equivalent to Di. Formally, these DAs are computed as follows (C1 ≡ C ′1 denotes (C1 ⊑ C ′1 ) ⊓ (C ′1 ⊑ C1)).

• If Di is a concept name or ⊤, then Ui def= (Bi ≡ Di),
• If Di =Dj ⊓Dk then Ui def=(Bi ≡ (Bj ⊓Bk)),
• If Di = ∃rk.Dj then Ui def=(Bi ≡ ∃rk.Bj),
• Ui def= [⊤ ⊑ Bi ⊔ Bj ]t1 ⊓ ¬(⊤ -⊛ (⊤ ⊑ ∃t1.(Bi ⊓ Bj ))) whenever Di = ¬Dj , where [⊤ ⊑ Bi ⊔ Bj ]t1 denotes ¬(∃t1.⊤ ⊑ Emp -⊛ (〈∃t2.⊤ ̸≡t1 ⊥〉⊓ (Bi ⊓ ∃t2.⊤ ⊑ Emp) ⊓ (Bj ⊓ ∃t2.⊤ ⊑ Emp))).

We define τ(C(a)) as B1(a) ⊓ (di∈[1,α] Ui), completing the definition of the equiconsistent ∗-free dynamic axiom. We are now in position to state a striking undecidability result.

Theorem 4. CONS(ELD) is undecidable (even without ∗).

6 Concluding Remarks

We introduced a framework for enriching knowledge bases with a dynamic box (DBox) that specifies how the satisfaction of GCIs and assertions evolves when the interpretation is modified. Its dynamic connectives ∗ and -⊛ are imported from separation logics. Such an incursion of separation logics in DLs is completely new. The framework can be developed in many directions but we focused on a few landmark problems. Whereas we have shown that CONS(ALCD+) is EXPTIME-complete and CONS(ELD+) is in PTIME, the extensions with dynamic axioms admitting negation at the top level lead to undecidable problems. The PTIME upper bound for CONS(ELD+) is obtained using a simple algorithm thanks to a characterisation whose proof requires a fine-tuned model-theoretical construction. Besides, we showed that the satisfiability problem for ALC with respect to complex role inclusion axioms can be reduced to CONS(ALCD), leading to undecidability. More surprisingly, CONS(ELD) is undecidable too (which amounts to encode concept negation).

Though updates for ABoxes have been already investigated, see e.g. [Liu et al., 2006; De Giacomo et al., 2006], our framework is original as it concerns updates in interpretations. In the paper, we only considered (de)composition of roles and the only reasoning task was about knowledge base consistency. Other variants are possible (domain (de)composition, subsumption problems, etc.) in particular related to alternative interpretations for the composition operator.

Acknowledgements

B. Bednarczyk is supported by ERC Consolidator Grant 771779 (DeciGUT). S. Demri and A. Mansutti are supported by the Centre National de la Recherche Scientifique (CNRS).