Dynamic Description Logic based on DL-Lite

Na Zhang, Liang Chang, Zhoubo Xu, Tianlong Gu

Guangxi Key Laboratory of Trusted Software, Guilin University of Electronic Technology,
Guilin 541004, China

zhnamengluo@163.com, {chang1, xzbli_11, cctlgu}@guet.edu.cn

**Abstract.** Description logics offer considerable expressive power for describing knowledge about static application domains while reasoning is still decidable. The dynamic description logic DDL is a family of dynamic extensions of description logics for representing and reasoning about knowledge of dynamic application domains. In order to provide effective reasoning mechanisms, systems of DDL investigated in the literatures assume that there is no general concept inclusion(GCI) contained in the knowledge base. In this paper, we build a system of dynamic description logic based on the tractable description logic $DDL-Lite_R^{pr}$, in such a way that all the knowledge described by $DDL-Lite_R^{pr}$ is supported by our system. A decision algorithm is provided for our system $DDL-Lite_R^{pr}$. Termination and correctness of the algorithm are proved.

**Keywords:** description logic, dynamic description logic, action theory, satisfiability, tableau algorithm

# 1 Introduction

With the rapid development of the Semantic Web, description logics [1] are playing an important role in it, which are recommended by W3C as the basis of Web Ontology Language OWL [2]. About static application domains, they provide considerable expressive power and decidable reasoning mechanisms [3]. But they can't directly deal with knowledge of dynamic application domains which are characterized by actions.

For this limitation, Shi et al. [4] put forward a dynamic description logic DDL based on a combination of description logic ALC, dynamic logic and action theory. Based on DDL, a family of dynamic description logics named DDL(X®)[5] was proposed for representing and reasoning about actions, where the minimal change semantics[6] were used to define the semantics of atomic action definitions. But all the current decision algorithms for dynamic description logics are all restricted to requiring that TBoxes of description logics don't include GCIs any more. The DL-Lite family [7] is a family of DLs tailored to capture conceptual modeling constructs while keeping reasoning.

Based on [5], in this paper, we first of all propose a dynamic description logic $DDL-Lite_R^{pr}$ and give its syntax and semantics. And we adopt model-based semantics $\mathcal{L}^a \subseteq [8]$ of ABox update to define the semantics of atomic action definitions. Then a
tableau decision algorithm which supports GCIs for DDL-Lite<sub>R</sub><sup>pr</sup> is given. Finally, the termination and correctness of the algorithm are proved.

## 2 Dynamic Description Logic DDL-Lite<sub>R</sub><sup>pr</sup>

DDL-Lite<sub>R</sub><sup>pr</sup> primitive symbols include a set $N_C$ of concept names, a set $N_R$ of role names, a set $N_I$ of individual names and a set $N_A$ of action names. With the help of a set of constructors, starting from these symbols, roles, concepts, formulas and actions can be inductively constructed respectively.

**Definition 1.** Roles of DDL-Lite<sub>R</sub><sup>pr</sup> are formed according to the following syntax rule:

$$R ::= P \mid P^{-} \text{ where } P \in N_R.$$

**Definition 2.** Concepts of DDL-Lite<sub>R</sub><sup>pr</sup> are formed according to the following syntax rule:

$$C, C' ::= A_i \mid \neg C \mid \exists R \text{ where } A_i \in N_C, R \text{ is a role.}$$

The form of $C_1 \sqsubseteq C_2$ is called a GCI short for a general concept inclusion assertion, where $C_1$ and $C_2$ are any concept. The form of $R_1 \sqsubseteq R_2$ is called a role inclusion assertion where $R_1$ and $R_2$ are any role. Each finite set $\mathcal{T}$ of GCIs and role inclusion assertions is called a TBox of DDL-Lite<sub>R</sub><sup>pr</sup>, where disjointness that involves roles is forbidden.

**Definition 3.** Formulas of DDL-Lite<sub>R</sub><sup>pr</sup> are formed according to the following syntax rule:

$$\varphi, \varphi' ::= C(p) | R(p, q) | <\pi> \varphi | \neg \varphi \text{ where } p, q \in N_I, R \in N_R, C \text{ is a concept, } \pi \text{ is an action.}$$

Formulas of the form $C(p), R(p, q), <\pi>\varphi$ and $\neg\varphi$ are respectively called concept assertion, role assertion, diamond assertion and negation formula. Concept assertions, role assertions, negations of concept assertions, and negations of role assertions are all called ABox assertions. A finite set of ABox assertions is called an ABox of DDL-Lite<sub>R</sub><sup>pr</sup>. For any ABox $\mathcal{A}$, we use $\mathcal{A}^- \text{ to denote the set } \{\neg\varphi \mid \varphi \in \mathcal{A}\}$.

**Definition 4.** With respect to a TBox $\mathcal{T}$, an atomic action definition of DDL-Lite<sub>R</sub><sup>pr</sup> is of the form $\alpha \equiv (P, E)$, where,

(1) $\alpha \in N_A$ is an atomic action name;

(2) $P$ is a finite set of ABox assertions for describing the pre-conditions of the action;

(3) $E$ is a finite set of ABox assertions for describing the post-conditions.

For each finite set $\mathcal{A}_c$ of atomic action definitions, if no action name occurs on the left-hand sides for more than once, then we call $\mathcal{A}_c$ an ActBox of DDL-Lite<sub>R</sub><sup>pr</sup>.

**Definition 5.** With respect to a TBox $\mathcal{T}$, an ActBox $\mathcal{A}_c$, actions of DDL-Lite<sub>R</sub><sup>pr</sup> are formed according to the following syntax rule:

$$\pi, \pi' ::= \alpha \mid \varphi? \mid \pi \cup \pi' \mid \pi; \pi' \mid \pi^* \text{ where } \alpha \text{ is an atomic action, } \varphi \text{ is a formula.}$$

Actions of the form $\alpha, \varphi?, \pi \cup \pi', \pi; \pi'$ and $\pi^*$ are respectively called atomic action, test action, choice action, sequential action and iterated action.

**Definition 6.** A DDL-Lite<sub>R</sub><sup>pr</sup>-model is of the form $M = (W, T, \Delta, I)$, where,

1) $W$ is a non-empty finite set composed of states;

2) $T$ is a function that maps every action name $\alpha \in N_A$ to a binary relation $T(\alpha) \subseteq W \times W$;

3) $\Delta$ is a non-empty set made up of individuals;

4) $I$ is a function which associates every state $w \in W$ a DL-interpretation $I(w)=(\Delta, I^{(w)})$, where the function $I^{(w)}$
- maps each concept name $C_i \in N_C$ to a set $C_i^{(w)} \subseteq \Delta$,

- maps each role name $R_i \in N_R$ to a binary relation $R_i^{(w)} \subseteq \Delta \times \Delta$, and

- maps each individual name $p_i \in N_I$ to an individual $p_i^{(w)} \in \Delta$, with the constraints that $p_i^{(w)} = p_i^{(w')}^*$ for any state $w' \in W$.

**Definition 7.** Let $\mathcal{T}$, $\mathcal{Ac}$ be a TBox, an ActBox respectively. $M = (W, T, \Delta, I)$ is a model of DDL-Lite$_R^{\mathrm{pr}}$. The semantics of roles, concepts, formulas and actions of DDL-Lite$_R^{\mathrm{pr}}$ are defined inductively as follows.

Firstly, for any state $w \in W$, each role $R$ is interpreted as a binary relation $R^{(w)} \subseteq \Delta \times \Delta$ and each concept $C$ is interpreted as a set $C^{(w)} \subseteq \Delta$. The semantics of roles and concepts of DDL-Lite$_R^{\mathrm{pr}}$ are defined inductively as follows:

1. $(R^{(w)}) = \{(y, x) | x \in \Delta, y \in \Delta \text{ and } (x, y) \in R^{(w)}\}$;

2. $(\neg C)^{(w)} = \Delta \setminus C^{(w)}$, where “$\neg$” is the set difference operator;

3. $(\exists R)^{(w)} = \{ x \in \Delta | \text{ there is some } y \in \Delta \text{ such that } (x, y) \in R^{(w)} \}$.

Secondly, for any state $w \in W$, the satisfaction-relation $(M, w) \models \varphi$ for any formula $\varphi$ is defined inductively as follows:

4. $(M, w) \models C(p)$ iff $p^I \in C^{(w)}$;

5. $(M, w) \models R(p, q)$ iff $(p^I, q^I) \in R^{(w)}$;

6. $(M, w) \models \neg \varphi$ iff it is not the case that $(M, w) \models \varphi$;

7. $(M, w) \models \langle \pi \rangle \models \varphi$ iff some state $w' \in W$ exists with $(w, w') \in T(\pi)$ and $(M, w') \models \varphi$;

8. $(M, w) \models [\pi] \varphi$ iff for every state $w' \in W$: if $(w, w') \in T(\pi)$ then $(M, w') \models \varphi$.

Finally, each action $\pi$ is interpreted as a binary relation $T(\pi) \subseteq W \times W$ according to the following definitions:

9. $T(\varphi) = \{(w, w) | (M, w) \models \varphi\}$;

10. $T(\pi \cup \pi') = T(\pi) \cup T(\pi')$;

11. $T(\pi; \pi') = \{(w, w') | \text{ there is some state } w'' \in W \text{ such that } (w, w'') \in T(\pi) \text{ and } (w'', w') \in T(\pi')\}$;

12. $T(\pi^*)$ = reflexive transitive closure of $T(\pi)$.

A model $M$ satisfies a TBox $\mathcal{T}$, denoted by $M \models \mathcal{T}$, if and only if for every state $w \in W$, $C_1^{(w)} \subseteq C_2^{(w)}$ for every concept inclusion assertion $C_1 \subseteq C_2 \in \mathcal{T}$ and $R_1^{(w)} \subseteq R_2^{(w)}$ for every role inclusion assertion $R_1 \subseteq R_2 \in \mathcal{T}$. A state $w$ of a model $M$ satisfies an ABox $\mathcal{A}$, denoted by $(M, w) \models \mathcal{A}$, if and only if $(M, w) \models \varphi$ for every ABox assertion $\varphi \in \mathcal{A}$.

According to $\mathcal{Ac}$, any atomic action $\alpha$ is specified by some atomic action definition $\alpha \equiv (P, E)$. Then w.r.t. a TBox $\mathcal{T}$, a model $M$ satisfies an atomic action definition $\alpha \equiv (P, E)$, in symbols $M \models_T \alpha \equiv (P, E)$, if and only if $M \models_T$ and $T(\alpha) = \{(w, w') | \begin{array}{l} \textcircled{1}(M, w) \models P, \\ \textcircled{2}(M, w') \models E, \\ \textcircled{3} \text{ for every state } w'' \in W, \text{ if } (M, w'') \models E, \text{ then } \mathrm{dist}_{\mathcal{A}}^a (I(w), I(w')) \subseteq \mathrm{dist}_{\mathcal{A}}^b (I(w), I(w'')) \end{array}$}.

The distance function between interpretations is specified in details as follows.

Firstly, given two interpretations $I(w) = (\Delta, \cdot^{(w)})$ and $I(w') = (\Delta, \cdot^{(w')})$, the distance between them is denoted by $\mathrm{dist}_{\mathcal{A}}^b(I(w), I(w'))$. Then $\mathrm{dist}_{\mathcal{A}}^b(I(w), I(w')) = I(w) \ominus I(w') = \bigcup_{C \in N_C} ((C^{(w)} - C^{(w')}) \cup (C^{(w')} - C^{(w)}) \cup ((R^{(w)} - R^{(w')}) \cup (R^{(w')} - R^{(w)}))$

where $\ominus$ is the set symmetric difference operator. Distances under $\mathrm{dist}_{\mathcal{A}}^b$ are compared by set inclusion.

**Definition 8.** A model $M$ satisfies an ActBox $\mathcal{Ac}$ w.r.t. a TBox $\mathcal{T}$, in symbols $M \models_T \mathcal{Ac}$, if and only if $M \models_T \alpha \equiv (P, E)$ for every atomic action definition $\alpha \equiv (P, E) \in \mathcal{Ac}$.
**Definition 9.** A formula $\varphi$ is satisfiable w.r.t. a TBox $\mathcal{T}$ and an ActBox $\mathcal{A}_c$ if and only if there is a model $M = (W, T, \Delta, I)$ and a state $w \in W$ such that $M \models \mathcal{T}$, $M \models_{\mathcal{T}} \mathcal{A}_c$ and $(M, w) \models \varphi$.

### 3 Tableau Decision Algorithm for DDL-Lite<sub>R</sub><sup>pr</sup>

Let $\mathcal{T}, \mathcal{A}_c$ be a TBox and an ActBox respectively. Let $\varphi$ be a DDL-Lite<sub>R</sub><sup>pr</sup>-formula which is defined w.r.t. $\mathcal{A}_c$. For the convenience of presentation, we firstly transform the formula $\varphi$ into a normal form $nf(\varphi)$ according to the following steps.

(1) Replace every occurrence of atomic actions with their atomic action definitions. Let $\varphi'$ be the resulted formula.

(2) Transform $\varphi'$ into an equivalent one in negation normal form by pushing negations inwards according to the following equivalences:

$$ \neg (<\pi>\psi) = [\pi] \neg\psi \quad \neg ([\pi] \psi) = <\pi>\neg\psi \quad \neg\neg\psi = \psi $$

A full closure of an ABox $\mathcal{A}$ w.r.t. TBox $\mathcal{T}$, denoted by $fcl_{\mathcal{T}}(\mathcal{A})$, is the set of all ABox assertions $f$ such that $\mathcal{A} \models \tau_f$.

Next, we introduce some definitions involved in the algorithm as follows.

Given a TBox $\mathcal{T}$, a prefix $\sigma.\mu$ with a sequential action $\sigma$ and a set $\mu$ of ABox assertions is constructed according to the following syntax rule:

$$ \sigma.\mu ::= (\emptyset, \emptyset).\emptyset \mid \sigma; (P, E). (\mu \setminus (fcl_{\mathcal{T}}(E))^{\top}) \cup E $$

where $(\emptyset, \emptyset)$ and $(P, E)$ are atomic actions, $\sigma; (P, E)$ is a sequential action.

We also use $\sigma_0.\mu_0$ to denote the prefix $(\emptyset, \emptyset)$. $\emptyset$ and call it the initial prefix. A prefixed formula is a pair $\sigma.\mu:\varphi$, where $\sigma.\mu$ is a prefix and $\varphi$ is a formula.

A branch $\mathcal{B}$ is a union of a set $\mathcal{B}_{PF}$ of prefixed formulas and a set $\mathcal{B}_E$ of eventuality records which is of the form $X \equiv <\pi^*>\varphi$.

A branch $\mathcal{B}$ is completed if and only if it can't be expanded by any tableau expansion rule.

An eventuality record $X \equiv <\pi^*>\varphi$ is fulfilled in a branch $\mathcal{B}$ if and only if there is a prefix $\sigma.\mu$ such that both $\sigma.\mu: X \in \mathcal{B}$, and $\sigma.\mu:\varphi \in \mathcal{B}$.

A branch $\mathcal{B}$ is ignorable if and only if it is completed but contains some eventuality record $X \equiv <\pi^*>\varphi$ which is not fulfilled.

A branch $\mathcal{B}$ is contradictory if and only if there is some prefix $\sigma.\mu$ and some formula $\varphi$ such that both $\sigma.\mu:\varphi \in \mathcal{B}$ and $\sigma.\mu:\neg\varphi \in \mathcal{B}$.

For any branch $\mathcal{B}$, $\{\psi|\sigma_0.\mu_0: \psi \in \mathcal{B}\}$ and $\psi$ is an ABox assertion} is denoted by $IV_{\mathcal{B}}$.

Tableau expansion rules on inverse roles, non-atomic actions are the same with [5].

<table><caption>**Fig.1.** Tableau expansion rules on atomic actions</caption><tr><td>neg-atom<sup>-></sup>rule</td><td>If σ.μ:¬(<P, E>)>φ ∈ B, {σ.μ:ψ<sup>¬</sup> | ψ ∈ P}∩B=Ø, and there is a prefix σ'.μ' with both μ' = (μ\(fcl<sub>T</sub>(E))<sup>¬</sup>)∪E and σ'.μ':¬φ ∉ B, then set either B := B ∪ {σ'.μ':¬φ} or B := B ∪ {σ.μ:¬ψ} for some ψ ∈ P.</td></tr><tr><td>atom<sup>-></sup>rule</td><td>If σ.μ:<(P, E)>φ ∈ B, and if {σ.μ: ψ | ψ ∈ P} ⊊ B, or no prefix σ'.μ' exists with both μ' = (μ\(fcl<sub>T</sub>(E))<sup>¬</sup>)∪E and σ'.μ':φ ∈ B, then: if there is no prefix σ'.μ' with μ' = (μ\(fcl<sub>T</sub>(E))<sup>¬</sup>)∪E, then introduce a prefix σ''.μ'' := σ; (P, E). (μ\(fcl<sub>T</sub>(E))<sup>¬</sup>)∪E and set B := B ∪ {σ.μ: ψ | ψ ∈ P}∪{σ''.μ'' : φ | φ ∈ μ''}, else find a prefix σ'.μ' with μ' = (μ\(fcl<sub>T</sub>(E))<sup>¬</sup>)∪E, and set B := B ∪ {σ.μ: ψ | ψ ∈ P}∪{σ'.μ' : φ} ∪ {σ'.μ' : φ | φ ∈ μ'}</td></tr></table>
<table><caption>**Fig.2.** Tableau expansion rules on ABox assertions</caption><tr><td>B-rule</td><td>If σ.μ:φ∈B, and φ is an ABox assertion, then : 1. A={φ}; 2. if {σ₀.μ₀: φ | φ ∈ A<sup>Regress(σ.μ)</sup>} ⊊ B, then any ψ ∈ A<sup>Regress(σ.μ)</sup> and σ₀.μ₀:ψ ∈ B set B := B ∪ {σ₀.μ₀: ψ}.</td></tr></table>

For B-rule, ABox $\mathcal{A}^{\text{Regress}(\sigma,\mu)}$ is constructed according to the following Algorithm 1.
**Algorithm 1** Given a regress setting $K=(\mathcal{T}, \mathcal{A})$ and $\mu^-$, given that $\mathcal{A}$ and $\mu^-$ w.r.t. $\mathcal{T}$ are satisfiable respectively, construct an ABox $\mathcal{A}'$ by the following steps.

**Step 1.** Let $\mathcal{A}'$ is an empty set and S is equivalent to $fcl_{\mathcal{T}}(\mathcal{A})$.

**Step 2.** If S is not an empty set, do the following operations:

1. Choose some $\psi$ of S and at the same time remove $\psi$ from S.

2. If a union of the two sets $\{\psi\}$, $fcl_{\mathcal{T}}(\mu^-)$ is satisfiable, then add $\psi$ to $\mathcal{A}'$.

3. Repeat Step 2 until the condition is unallowed.

The construction process ensures the following Lemma 3 and $\mathcal{A}^{\text{Regress}(\sigma,\mu)}$ is a union of $\mathcal{A}$, $\mu^-$.

Finally, the tableau decision algorithm is described as follows.

**Algorithm 2** The satisfiability of a formula $\varphi$ w.r.t. a TBox $\mathcal{T}$ and an ActBox $\mathcal{A}_c$ is decided according to the following steps:

**Step1.** Construct a branch $B := \{\sigma_0, \mu_0: \text{nfl}(\varphi)\}$.

**Step2.** If all the tableau expansion rules are applied to $B$ in random order so that they yield a completed branch $B'$, and $B'$ is neither contradictory nor ignorable, and $IV_B$ of $B'$ is consistent w.r.t. $\mathcal{T}$, then the algorithm returns "TRUE", else returns "FALSE".

**Theorem 1.** Algorithm 2 terminates.

Firstly, the number of branches which will be investigated by Algorithm 2 is finite. Then, for each branch $B$ investigated by Algorithm 2, the number of ABox assertions contained in the initial view $IV_B$ is also finite. Finally, the consistency of $IV_B$ w.r.t. $\mathcal{T}$ can be decided with terminable procedures.

To demonstrate the correctness of Algorithm 2, some notations are introduced as follows.

Firstly, with reference to Algorithm AlignAlg((T, A), N)[8], Algorithm 1 has the following properties.

**Lemma 1.** Let $\mathcal{T}, \mathcal{A}, \mathcal{N}$ be a TBox, an ABox and an ABox, respectively. $\mathcal{A}, \mathcal{N}$ w.r.t. $\mathcal{T}$ are consistent, if $\mathcal{A}^N$ is an ABox which is constructed according to Algorithm 1 under $\mathcal{A}$ and the update information $\mathcal{N}$, then we have $\mathcal{A}^N = fcl_{\mathcal{T}}(\mathcal{A}) - (fcl_{\mathcal{T}}(\mathcal{N}))^- \cup \mathcal{N}$.

**Lemma 2.** Let $\mathcal{T}$ be a TBox, $\sigma.\mu$ is a prefix w.r.t. $\mathcal{T}$, where $\sigma = (\emptyset, \emptyset)$; $(P_1, E_1)$; $(P_2, E_2)$; ...; $(P_n, E_n)$. For any ABox $\mathcal{A}$, if $\mathcal{A}$ w.r.t. $\mathcal{T}$ is consistent, then there must be $((\mathcal{A}^{E_1})^{E_2} \cdots)^{E_n} = \mathcal{A}^\mu$.

Secondly, we introduce branch-model mappings to act as bridges between branches and models.

Let $\mathcal{T}, \mathcal{A}_c, B$ and $M = (W, T, \Delta, I)$ be a TBox, an ActBox, a branch and a model respectively. A branch-model mapping $\delta$ w.r.t. $\mathcal{T}, B$ and $M$ is a function from $\Sigma$ of prefixes occurring in $B$ to states of $M$, satisfying that for each pair of prefixes $\sigma.\mu$ and $\sigma'.\mu'$ occurring in $B$: if there is an atomic action $(P, E)$, $\sigma'=\sigma; (P, E)$ and $\mu' = (\mu \setminus fcl_{\mathcal{T}}(E))^- \cup E$, then:

(1) $M \models \mathcal{T}$; (2) $(M, \delta(\sigma.\mu)) \models P$; (3) $(M, \delta(\sigma'.\mu')) \models E$; (4) for any $\sigma''$. $\mu'' \in \Sigma$, if $(M, \delta(\sigma''$. $\mu'')) \models E$, then $\text{dist}_{\subseteq}^a(I(\delta(\sigma.\mu)), I(\delta(\sigma'.\mu'))) \subseteq \text{dist}_{\subseteq}^a(I(\delta(\sigma.\mu)), I(\delta(\sigma''$. $\mu'')))$.
By means of a branch-model mapping, we can get the following property.

**Lemma 3.** Let $\mathcal{A}^{\text{Regress}(\sigma, \mu)}$ be a ABox constructed by the regression operator in the B-rule. Let $M = (W, I, \Delta, I)$ be a model with $M \models \mathcal{T}$. Then, for any branch-model mapping $\delta$ w.r.t. $\mathcal{T}$, $\mathcal{B}$ and $M$, we have $(M, \delta(\sigma, \mu)) \models \mathcal{A}$, iff $(M, \delta(\sigma_0, \mu_0)) \models \mathcal{A}^{\text{Regress}(\sigma, \mu)}$.

Finally, it is easy to prove the correctness of Algorithm 2.

**Theorem 2.** Algorithm 2 returns “$\varphi$ is satisfiable w.r.t. $\mathcal{T}$ and $\mathcal{A}_c$” if and only if $\varphi$ w.r.t. $\mathcal{T}$ and $\mathcal{A}_c$ is satisfiable.

# 4 Conclusion

Dynamic description logic DDL-Lite<sub>R</sub><sup>pr</sup> not only inherits the feature of representing and reasoning about knowledge of dynamic application domains as the same with the existing dynamic description logics, but also at the same time its TBoxes are composed of GCIs. We broaden knowledge offered by TBoxes of dynamic description logics and provide a reliable algorithm foundation for the practical application of a dynamic description logic with GCIs. Further work is to optimize the algorithm and develop a corresponding dynamic description logic reasoning machine.

**Acknowledgements.** This work is supported by the National Natural Science Foundation of China (Nos. 61363030, 61100025, 61262030), the Natural Science Foundation of Guangxi Province (No.2012GXNSFBA053169) and the Science Foundation of Guangxi Key Laboratory of Trusted Software.

# References

1. Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P.F.: The Description Logic Handbook: Theory, Implementation and Applications. Cambridge University Press, Cambridge (2003)

2. Horrocks, I., Patel-Schneider, P.F., Harmelen, F.V.: From SHIQ and RDF to OWL: the making of a web ontology language. J. Web Semant. 1(1), 7–26 (2003)

3. Baader, F., Sattler, U.: An Overview of Tableau Algorithms for Description Logics. Studia Logica 69, 5–40(2001)

4. Shi, Z.Z., Dong, M.K., Jiang, Y.C., Zhang, H.J.: A logical foundation for the semantic Web. Science in China, Ser. F: Information Sciences 48(2), 161–178 (2005)

5. Chang, L., Shi, Z.Z., Gu, T.L., Zhao, L.Z.: A family of dynamic description logics for representing and reasoning about actions. Journal of Automated Reasoning 49(1), 19–70 (2012)

6. Baader, F., Lutz, C., Miličić, M., Sattler, U., Wolter, F.: Integrating description logics and action formalisms: first results. In: Proc. of the 12th Nat. Conf. on Artificial Intelligence (AAAI’05), pp. 572–577. AAAI Press / MIT Press (2005)

7. Artale, A., Calvanese, D., Kontchakov, R., Zakharyaschev, M.: The DL-Lite family and relations. J. of Artificial Intelligence Research 36, 1–69 (2009)

8. Kharlamov, E., Zheleznyakov, D.: Capturing instance level ontology evolution for DL-Lite. In: Proc. of the 10th Int. Conf. on Semantic Web(ISWC’11), pp. 321–337. Springer (2011)