Bisimilarity for paraconsistent description logics

Abstract

We introduce comparisons w.r.t. information between interpretations in paraconsistent description logics and use them to define bisimilarity for such logics. This notion is useful for concept learning in description logics when inconsistencies occur. We give preservation results and the Hennessy-Milner property for comparisons w.r.t. information in paraconsistent description logics. As consequences, we obtain also invariance results and the Hennessy-Milner property for bisimilarity in paraconsistent description logics.

Keywords

Description logics paraconsistent logics bisimulation bisimilarity

1 Introduction

Description logics (DLs) are a family of knowledge representation formalisms, which are suitable for reasoning about terminological knowledge. The basic elements of DLs are concepts, roles and individuals. A concept is interpreted as a set of individuals, while a role is interpreted as a binary relation between individuals. Concepts and roles are constructed from concept names, role names and individual names using constructors. A knowledge base in a DL contains a TBox with concept definitions and terminological axioms, and an ABox with assertions about individuals. It may also contain an RBox with axioms about roles. DLs are variants of modal logics, they are usually designed to be tractable fragments of first-order logic.

Two individuals in an interpretation are indiscernible w.r.t. a description language if they are bisimilar w.r.t. that language. In modal and description logics, bisimilarity is defined using bisimulation, which is a useful notion for both mathematical and computational investigations. There are many works on bisimulation in modal logics and for labeled transition systems [1], but bisimulation in DLs received considerable attention from researchers only recently [2 , 9]. Apart from analyzing expressiveness [5, 8], bisimulation is also useful for concept learning in DLs [6 , 21].

Using the traditional semantics, any conclusion can be drawn from an inconsistent knowledge base. In order to avoid that trivialization, paraconsistent semantics/reasoning can be used. Extensions of DLs with paraconsistent semantics and reasoning methods for them have been studied by a considerable number of researchers [10–13 , 23]. In [17] Nguyen and Szałas discussed earlier work on paraconsistent DLs and studied a large family of paraconsistent semantics for the expressive DL $SROIQ$ . They compared the strength of those paraconsistent semantics. Given two paraconsistent semantics $s$ and $s^{'}$ , if $s^{'}$ is stronger than $s$ and a knowledge base KB is consistent in $s^{'}$ , then it is better to use KB with $s^{'}$ than $s$ .

In this work, we study bisimilarity for paraconsistent DLs. The notion is useful for concept learning in DLs for the case when a given interpretation, treated as a training information system, contains inconsistent information. Dealing with noise or inconsistent information has been investigated in traditional machine learning. However, as far as we know, it was not studied before for concept learning in DLs. As bisimilarity is the notion for characterizing indiscernibility in DLs, bisimilarity for paraconsistent DLs is worth studying.

Due to the nature of the considered paraconsistent semantics, we define bisimilarity for paraconsistent DLs by introducing and using comparisons w.r.t. information between interpretations in paraconsistent DLs. Comparisons w.r.t. information differ from bisimulation-based comparisons studied in [2, 3] (also called directed simulations in [7]) in that the former use the information ordering and preserve information (about truth and falsity) in paraconsistent DLs, while the latter use the truth ordering and preserve semi-positive concepts in traditionalDLs.

The DLs considered in this work extend the basic DL $ALC$ with features among inverse roles, nominals, qualified number restrictions, the universal role and local reflexivity of a role. The paraconsistent semantics we use for them are the ones from [17], but with a slight modification. We give results on preservation of concepts, TBoxes and ABoxes as well as the Hennessy-Milner property for comparisons w.r.t. information in paraconsistent DLs. As consequences, we obtain also invariance results and the Hennessy-Milner property for bisimilarity in paraconsistent DLs.

This work is an extension of the conference paper [14]. In comparison with [14], it additionally provides full proofs for all of the results, a discussion on applications, and more explanations.

The rest of this structure is as follows. In Section 2, we specify the paraconsistent DLs studied in this work. In Section 3, we define comparisons w.r.t. information and then bisimilarity for the considered paraconsistent DLs. We provide results about preservation and invariance in Section 4 and results on the Hennessy-Milner property in Section 5. In Section 6, we discuss applications of bisimilarity to concept learning in paraconsistent DLs. We conclude this work in Section 7.

2 Preliminaries

2.1 Syntax of the description logics ${ALC}_{Φ}$

Let Φ be a set of features among I (inverse roles), O (nominals), Q (qualified number restrictions), U (the universal role) and Self (local reflexivity of a role). In this section we recall notations and semantics of the DL ${ALC}_{Φ}$ that extends $ALC$ with the features from Φ.

Assume that our language uses a countable set C of concept names, a countable set R of role names (not containing U), and a countable set I of individual names. We use letters like A, B to denote concept names, letters like r, s to denote role names, and letters like a, b to denote individual names.

Roles (of ${ALC}_{Φ}$ ) are defined as follows:

if r ∈ R then r is a role,

if I ∈ Φ and r ∈ R then r^- is a role,

if U ∈ Φ then U is a role (the universal role).

Concepts (of ${ALC}_{Φ}$ ) are defined as follows:

⊤ and ⊥ are concepts,

if A∈ C then A is a concept,

if C, D are concepts and R is a role then:

¬C, C ⊓ D, C ⊔ D, ∀R . C, ∃R . C are concepts,

if O ∈ Φ and a ∈ I then {a} is a concept,

if Q ∈ Φ, R ≠ U and n is a natural number, then ≥ n R . C and ≤ n R . C are concepts,

if Self ∈ Φ and r ∈ R then ∃r . Self is a concept.

We use letters like C, D to denote concepts, and letters like R, S to denote roles. Given a finite set Γ = {C₁, …, C_n} of concepts, by ⊓Γ we denote C₁ ⊓ … ⊓ C_n, and by ⨆Γ we denote C₁ ⊔ … ⊔ C_n. If Γ =∅, then ⊓Γ =⊤ and ⨆Γ =⊥.

A terminological axiom, also called a general concept inclusion (GCI), is an expression of the form C ⊑ D. A TBox is a finite set of terminological axioms. An individual assertion is an expression of the form C (a), R (a, b), ¬R (a, b), a ≐ b or a ≠ b, where R ≠ U. An ABox is a finite set of individual assertions. A knowledge base is a pair $〈 T, A 〉$ consisting of a TBox $T$ and an ABox $A$ .

2.2 Paraconsistent semantics for description logics

In this subsection, we specify a family of paraconsistent semantics for DLs, which is based on [13, 17], but has a slight modification for semantics of number restrictions. Each paraconsistent semantics from the defined family, let’s say $s$ , is characterized by four parameters, denoted by $s_{C}$ , $s_{R}$ , $s_{\forall \exists Q}$ , $s_{GCI}$ , with the following intuitive meanings:

$s_{C} \in {2, 3, 4}$ specifies the number of possible truth values of assertions of the form A (x), where A∈ C.

$s_{R} \in {2, 3, 4}$ specifies the number of possible truth values of assertions of the form r (x, y), where r ∈ R.

$s_{\forall \exists Q} \in {+, \pm}$ specifies which from two considered semantics is used for concepts of the form ∀R . C, ∃R . C, ≤ n R.C or ≥ n R.C.

$s_{GCI} \in {w, m, s}$ specifies one of the three semantics for general concept inclusions: weak (w), moderate (m), strong (s).

In the case $s_{C} = 2$ , the truth values of assertions of the form A (x) are (true) and (false). In the case $s_{C} = 3$ , the third truth value is (inconsistent). In the case $s_{C} = 4$ , the additional truth value is (unknown). When $s_{C} = 3$ , one can identify inconsistency with the lack of knowledge, and the third value can be read either as inconsistent or as unknown. Similar explanations can be stated for $s_{R}$ .

We identify $s$ with the tuple $〈 s_{C}, s_{R}, s_{\forall \exists Q}, s_{GCI} 〉$ . The set of considered paraconsistent semantics is thus $S = {2, 3, 4} \times {2, 3, 4} \times {+, \pm} \times {w, m, s} .$

For $s \in S$ , an $s$ -interpretation is a pair $I = 〈 Δ^{I}, \cdot^{I} 〉$ , where $Δ^{I}$ is a non-empty set, called the domain, $\cdot^{I}$ is the interpretation function, which maps every individual name a to an element $a^{I} \in Δ^{I}$ , every concept name A to a pair $A^{I} = 〈 A_{+}^{I}, A_{-}^{I} 〉$ of subsets of $Δ^{I}$ , and every role name r to a pair $r^{I} = 〈 r_{+}^{I}, r_{-}^{I} 〉$ of binary relations on $Δ^{I}$ such that:

if $s_{C} = 2$ then $A_{+}^{I} = Δ^{I} \ A_{-}^{I}$

if $s_{C} = 3$ then $A_{+}^{I} \cup A_{-}^{I} = Δ^{I}$

if $s_{R} = 2$ then $r_{+}^{I} = (Δ^{I} \times Δ^{I}) \ r_{-}^{I}$

if $s_{R} = 3$ then $r_{+}^{I} \cup r_{-}^{I} = Δ^{I} \times Δ^{I}$ .

Remark 1. (from [17]) The intuition behind $A^{I} = 〈 A_{+}^{I}, A_{-}^{I} 〉$ is that $A_{+}^{I}$ gathers positive evidence about A, while $A_{-}^{I}$ gathers negative evidence about A. Thus, $A^{I}$ can be treated as the function from $Δ^{I}$ to {, , , } defined below:

Informally, $A^{I} (x)$ can be thought of as the truth value of $x \in A^{I}$ . Note that $A^{I} (x) \in$ {, } if $s_{C} = 2$ , and $A^{I} (x) \in$ {, , } if $s_{C} = 3$ . The intuition behind $r^{I} = 〈 r_{+}^{I}, r_{-}^{I} 〉$ is similar, and under which $r^{I} (x, y) \in$ {, } if $s_{R} = 2$ , and $r^{I} (x, y) \in$ {, , } if $s_{R} = 3$ . ■

The interpretation function $\cdot^{I}$ maps a role R to a pair $R^{I} = 〈 R_{+}^{I}, R_{-}^{I} 〉$ , defined for the case R ∉ R as follows: $\begin{matrix} (r^{-})^{I} & = & 〈 (r_{+}^{I})^{- 1}, (r_{-}^{I})^{- 1} 〉 \\ U^{I} & = & 〈 Δ^{I} \times Δ^{I}, \emptyset 〉 . \end{matrix}$ It maps a complex concept C to a pair $C^{I} = 〈 C_{+}^{I}, C_{-}^{I} 〉$ of subsets of $Δ^{I}$ defined as follows: $\begin{matrix} ⊤^{I} & = & 〈 Δ^{I}, \emptyset 〉 \\ ⊥^{I} & = & 〈 \emptyset, Δ^{I} 〉 \\ ({a})^{I} & = & 〈 {a^{I}}, Δ^{I} \ {a^{I}} 〉 \\ (\neg C)^{I} & = & 〈 C_{-}^{I}, C_{+}^{I} 〉 \\ (C ⊓ D)^{I} & = & 〈 C_{+}^{I} \cap D_{+}^{I}, C_{-}^{I} \cup D_{-}^{I} 〉 \\ (C ⊔ D)^{I} & = & 〈 C_{+}^{I} \cup D_{+}^{I}, C_{-}^{I} \cap D_{-}^{I} 〉 \\ (\exists R . Self)^{I} & = & 〈 {x \in Δ^{I} ∣ 〈 x, x 〉 \in R_{+}^{I}}, \\ {x \in Δ^{I} ∣ 〈 x, x 〉 \in R_{-}^{I}} 〉; \end{matrix}$ if $s_{\forall \exists Q} = +$ then $\begin{matrix} (\exists R . C)^{I} \\ = 〈 {x \in Δ^{I} ∣ \exists y (〈 x, y 〉 \in R_{+}^{I} \land y \in C_{+}^{I})}, \\ {x \in Δ^{I} ∣ \forall y (〈 x, y 〉 \in R_{+}^{I} \to y \in C_{-}^{I})} 〉 \\ (\forall R . C)^{I} \\ = 〈 {x \in Δ^{I} ∣ \forall y (〈 x, y 〉 \in R_{+}^{I} \to y \in C_{+}^{I})}, \\ {x \in Δ^{I} ∣ \exists y (〈 x, y 〉 \in R_{+}^{I} \land y \in C_{-}^{I})} 〉; \end{matrix}$

$\begin{matrix} (\geq n R . C)^{I} \\ = 〈 {x \in Δ^{I} ∣ # {y ∣ 〈 x, y 〉 \in R_{+}^{I} \land y \in C_{+}^{I}} \geq n}, \\ {x \in Δ^{I} ∣ # {y ∣ 〈 x, y 〉 \in R_{+}^{I} \land y \notin C_{-}^{I}} < n} 〉 \\ (\leq n R . C)^{I} \\ = 〈 {x \in Δ^{I} ∣ # {y ∣ 〈 x, y 〉 \in R_{+}^{I} \land y \notin C_{-}^{I}} \leq n}, \\ {x \in Δ^{I} ∣ # {y ∣ 〈 x, y 〉 \in R_{+}^{I} \land y \in C_{+}^{I}} > n} 〉; \end{matrix}$ if $s_{\forall \exists Q} = \pm$ then $\begin{matrix} (\exists R . C)^{I} \\ = 〈 {x \in Δ^{I} ∣ \exists y (〈 x, y 〉 \in R_{+}^{I} \land y \in C_{+}^{I})}, \\ {x \in Δ^{I} ∣ \forall y (〈 x, y 〉 \notin R_{-}^{I} \to y \in C_{-}^{I})} 〉 \\ (\forall R . C)^{I} \\ = 〈 {x \in Δ^{I} ∣ \forall y (〈 x, y 〉 \notin R_{-}^{I} \to y \in C_{+}^{I})}, \\ {x \in Δ^{I} ∣ \exists y (〈 x, y 〉 \in R_{+}^{I} \land y \in C_{-}^{I})} 〉; \end{matrix}$ $\begin{matrix} (\geq n R . C)^{I} \\ = 〈 {x \in Δ^{I} ∣ # {y ∣ 〈 x, y 〉 \in R_{+}^{I} \land y \in C_{+}^{I}} \geq n}, \\ {x \in Δ^{I} ∣ # {y ∣ 〈 x, y 〉 \notin R_{-}^{I} \land y \notin C_{-}^{I}} < n} 〉 \\ (\leq n R . C)^{I} \\ = 〈 {x \in Δ^{I} ∣ # {y ∣ 〈 x, y 〉 \notin R_{-}^{I} \land y \notin C_{-}^{I}} \leq n}, \\ {x \in Δ^{I} ∣ # {y ∣ 〈 x, y 〉 \in R_{+}^{I} \land y \in C_{+}^{I}} > n} 〉 . \end{matrix}$

For a set Γ of concepts, we denote $Γ_{+}^{I} = ⋂ {C_{+}^{I} ∣ C \in Γ}$ , $Γ_{-}^{I} = ⋃ {C_{-}^{I} ∣ C \in Γ}$ and $Γ^{I} = 〈 Γ_{+}^{I}, Γ_{-}^{I} 〉$ . Observe that, if Γ is finite, then $Γ^{I} = (⊓ Γ)^{I}$ .

Remark 1 applies also to complex concepts. For example, we say that $C^{I} (x) =$ if $x \in C_{+}^{I}$ and $x \in C_{-}^{I}$ . Note that $C^{I}$ is defined in the standard way [10 , 23] for the case C is of the form ⊤, ⊥, ¬D, D ⊓ D′ or D ⊔ D′. When $s_{\forall \exists Q} = +$ , $(\forall R . C)^{I}$ and $(\exists R . C)^{I}$ are defined as in [10 , 23], as in [13 , 17] when $s_{\forall \exists} = +$ , and as using semantics A of [19]. When $s_{\forall \exists Q} = \pm$ , $(\forall R . C)^{I}$ and $(\exists R . C)^{I}$ are defined as in [13 , 17] when $s_{\forall \exists} = \pm$ and as using semantics B of [19]. The parameter $s_{\forall \exists Q}$ also denotes the way of defining $(\geq n R . D)^{I}$ and $(\leq n R . D)^{I}$ . In the case $s_{\forall \exists Q} = +$ , $(\geq n R . D)^{I}$ and $(\leq n R . D)^{I}$ are defined as in [10 , 23], but for the case $s_{\forall \exists Q} = \pm$ , they are defined differently in order to guarantee the following properties: $\begin{matrix} (\exists R . C)^{I} & = & (\geq 1 R . C)^{I} \\ (\forall R . C)^{I} & = & (\leq 0 R . \neg C)^{I} . \end{matrix}$

Example 1. Let C = {A}, R = {r} and I = {a}. Consider a paraconsistent semantics $s$ with $s_{C} = s_{R} = 3$ and the $s$ -interpretations $I$ , $I^{'}$ and $I^{″}$ specified and illustrated below:

$Δ^{I} = {u, v, w}$ , $a^{I} = u$ , $A^{I} = 〈 {v, w}, {u, v} 〉$ , $r^{I} = 〈 {〈 u, v 〉, 〈 u, w 〉, 〈 v, w 〉, 〈 w, v 〉}, {〈 u, u 〉, 〈 v, u 〉, 〈 w, u 〉, 〈 v, v 〉, 〈 w, w 〉, 〈 w, v 〉} 〉$ ,

$Δ^{I^{'}} = {u^{'}, v^{'}}$ , $a^{I^{'}} = u^{'}$ , $A^{I^{'}} = 〈 {v^{'}}, {u^{'}, v^{'}} 〉$ , $r^{I^{'}} = 〈 {〈 u^{'}, v^{'} 〉, 〈 v^{'}, v^{'} 〉}, {〈 u^{'}, u^{'} 〉, 〈 v^{'}, v^{'} 〉, 〈 v^{'}, u^{'} 〉} 〉$ ,

$Δ^{I^{″}} = {u^{″}, v^{″}}$ , $a^{I^{″}} = u^{″}$ , $A^{I^{″}} = 〈 {v^{″}}, {u^{″}} 〉$ , $r^{I^{″}} = 〈 {〈 u^{″}, v^{″} 〉, 〈 v^{″}, v^{″} 〉}, {〈 u^{″}, u^{″} 〉, 〈 v^{″}, v^{″} 〉, 〈 v^{″}, u^{″} 〉} 〉$ .

In this figure, a notation x : A_f (resp. x : A_t, x:A_i) means A (x) is false (resp. true, inconsistent), and a normal (resp. dashed) edge from a node x to a node y means r (x, y) is true (resp. inconsistent). Inside an $s$ -interpretation, if there is no edge from x to y, then r (x, y) is false.

Regardless of $s_{\forall \exists Q}$ , we have that:

$(\exists r . A)^{I} = 〈 {u, v, w}, {w} 〉$ ,

$(\forall r . A)^{I} = 〈 {u, v, w}, {u, w} 〉$ ,

$(\geq 2 r . A)^{I} = 〈 {u}, {u, v, w} 〉$ ,

$(\leq 1 r . \neg A)^{I} = 〈 {u, v, w}, \emptyset 〉$ ,

$(\exists r . Self)^{I} = 〈 \emptyset, {u, v, w} 〉$ ,

$(\exists r . A)^{I^{'}} = 〈 {u^{'}, v^{'}}, {u^{'}, v^{'}} 〉$ ,

$(\forall r . A)^{I^{'}} = 〈 {u^{'}, v^{'}}, {u^{'}, v^{'}} 〉$ ,

$(\exists r . Self)^{I^{'}} = 〈 {v^{'}}, {u^{'}, v^{'}} 〉$ .

However,

$(\exists r . A)^{I^{″}} = 〈 {u^{″}, v^{″}}, \emptyset 〉$ if $s_{\forall \exists Q} = +$ , and

$(\exists r . A)^{I^{″}} = 〈 {u^{″}, v^{″}}, {v^{″}} 〉$ if $s_{\forall \exists Q} = \pm$ . ■

Observe that if $s_{R} = 2$ then $s_{\forall \exists Q}$ is not essential. Also, De Morgan laws hold for our constructors w.r.t. any semantics from $S$ . The following proposition of [17] means that: if $s_{C} \in {2, 3}$ and $s_{R} \in {2, 3}$ then $s$ is a three-valued semantics; if $s_{C} = s_{R} = 2$ then $s$ is a two-valued semantics.

Proposition 1. Let $s \in S$ be a semantics such that $s_{C} \in {2, 3}$ and $s_{R} \in {2, 3}$ . Let $I$ be an $s$ -interpretation, C be a concept, and R be a role. Then $C_{+}^{I} \cup C_{-}^{I} = Δ^{I}$ and $R_{+}^{I} \cup R_{-}^{I} = Δ^{I} \times Δ^{I}$ . Furthermore, if $s_{R} = 2$ , then $R_{+}^{I} = (Δ^{I} \times Δ^{I}) \ R_{-}^{I}$ ; if $s_{C} = s_{R} = 2$ , then $C_{+}^{I} = Δ^{I} \ C_{-}^{I}$ .

Let $s \in S$ and let $I$ be an $s$ -interpretation. We say that:

$I$ $s$ -validatesC ⊑ D, denoted by $I ⊨_{s} C ⊑ D$ , if:

case $s_{GCI} = w$ : $C_{-}^{I} \cup D_{+}^{I} = Δ^{I}$

case $s_{GCI} = m$ : $C_{+}^{I} \subseteq D_{+}^{I}$

case $s_{GCI} = s$ : $C_{+}^{I} \subseteq D_{+}^{I}$ and $D_{-}^{I} \subseteq C_{-}^{I}$

$I$ is an $s$ -model of a TBox $T$ , denoted by $I ⊨_{s} T$ , if it $s$ -validates all axioms of $T$ ;

$I$ $s$ -satisfies an individual assertion φ if $I ⊨_{s} φ$ , where $\begin{matrix} I ⊨_{s} C (a) & if & a^{I} \in C_{+}^{I} \\ I ⊨_{s} R (a, b) & if & 〈 a^{I}, b^{I} 〉 \in R_{+}^{I} \\ I ⊨_{s} \neg R (a, b) & if & 〈 a^{I}, b^{I} 〉 \in R_{-}^{I} \\ I ⊨_{s} a ≐ b & if & a^{I} = b^{I} \\ I ⊨_{s} a \neq b & if & a^{I} \neq b^{I} \end{matrix}$

$I$ is an $s$ -model of an ABox $A$ , denoted by $I$ $⊨_{s}$ $A$ , if it $s$ -satisfies all assertions of $A$ ;

$I$ is an $s$ -model of a knowledge base $〈 T, A 〉$ if it is an $s$ -model of both $T$ and $A$ ;

a knowledge base $〈 T, A 〉$ is $s$ -satisfiable if it has an $s$ -model.

Theorem 4.3 of [17] is a result about comparing the strength of semantics $s$ and $s^{'}$ from $S$ for the case $s_{\forall \exists Q} = s_{\forall \exists Q}^{'} = +$ . Analogously, it also holds for the case $s_{\forall \exists Q} = s_{\forall \exists Q}^{'} = \pm$ .

3 Comparison with respect to information and bisimilarity for paraconsistent DLs

Let Φ ⊆ {I, O, Q, U, Self} be a set of features, $s \in S$ a paraconsistent semantics, and $I$ , $I^{'}$ $s$ -interpretations. A non-empty binary relation $Z \subseteq Δ^{I} \times Δ^{I^{'}}$ is called a $(Φ, s)$ -comparison w.r.t. information between $I$ and $I^{'}$ if the following conditions hold for every a ∈ I, $x, y \in Δ^{I}$ , $x^{'}, y^{'} \in Δ^{I^{'}}$ , A ∈ C, r ∈ R and every role R of ${ALC}_{Φ}$ different from U: $Z (a^{I}, a^{I^{'}})$ (2) $Z (x, x^{'}) \Rightarrow [A_{+}^{I} (x) \Rightarrow A_{+}^{I^{'}} (x^{'})]$ (3) $Z (x, x^{'}) \Rightarrow [A_{-}^{I} (x) \Rightarrow A_{-}^{I^{'}} (x^{'})]$ (4) $\begin{matrix} [Z (x, x^{'}) \land R_{+}^{I} (x, y)] \\ \Rightarrow \exists y^{'} \in Δ^{I^{'}} [Z (y, y^{'}) \land R_{+}^{I^{'}} (x^{'}, y^{'})], \end{matrix}$ (5) if $s_{\forall \exists Q} = +$ then

$\begin{matrix} [Z (x, x^{'}) \land R_{+}^{I^{'}} (x^{'}, y^{'})] \\ \Rightarrow \exists y \in Δ^{I} [Z (y, y^{'}) \land R_{+}^{I} (x, y)], \end{matrix}$ (6) if $s_{\forall \exists Q} = \pm$ then

$\begin{matrix} [Z (x, x^{'}) \land \neg R_{-}^{I^{'}} (x^{'}, y^{'})] \\ \Rightarrow \exists y \in Δ^{I} [Z (y, y^{'}) \land \neg R_{-}^{I} (x, y)], \end{matrix}$ (7) if O ∈ Φ then

$Z (x, x^{'}) \Rightarrow (x = a^{I} \Leftrightarrow x^{'} = a^{I^{'}}),$ (8) if Q ∈ Φ then

$if Z(x,x′) holds and y1,…,yn (n ≥ 1) are pairwise different elements of Δ I such that R+ I(x,yi) holds for every 1 ≤ i ≤ n, then there exist pairwise different elements y1′,…,yn′ of Δ I′ such that R+ I′ (x′,yi′) and Z(yi,yi′) hold for every 1 ≤ i ≤ n,$ (9) if Q ∈ Φ and $s_{\forall \exists Q} = +$ then

$if Z(x,x′) holds and y1′,…,yn′ (n ≥ 1) are pairwise different elements of Δ I′ such that R+ I′ (x′,yi′) holds for every 1 ≤ i ≤ n, then there exist pairwise differen telements y1,…,yn of Δ I such that R+ I(x,yi) and Z(yi,yi′) hold for every 1 ≤ i ≤ n,$ (10) if Q ∈ Φ and $s_{\forall \exists Q} = \pm$ then

$if Z(x,x′) holds and y1′,…,yn′ (n ≥ 1) are pairwise different elements of Δ I′ such that ¬ R- I′ (x′,yi′) holds for every 1 ≤ i ≤ n, then there exist pairwise different elements y1,…,yn of Δ I such that ¬ R- I(x,yi) and Z(yi,yi′) hold for every 1 ≤ i ≤ n,$ (11) if U ∈ Φ then $\forall x \in Δ^{I} \exists x^{'} \in Δ^{I^{'}} Z (x, x^{'})$ (12) $\forall x^{'} \in Δ^{I^{'}} \exists x \in Δ^{I} Z (x, x^{'}),$ (13) if Self ∈ Φ then $Z (x, x^{'}) \Rightarrow [r_{+}^{I} (x, x) \Rightarrow r_{+}^{I^{'}} (x^{'}, x^{'})]$ (14) $Z (x, x^{'}) \Rightarrow [r_{-}^{I} (x, x) \Rightarrow r_{-}^{I^{'}} (x^{'}, x^{'})] .$ (15)

For example, if Φ = {I, Q} and $s_{\forall \exists Q} = +$ , then only the conditions (2)-(6), (9) and (10) are essential.

We write $I ≲_{Φ, s}^{\inf} I^{'}$ to denote that there exists a $(Φ, s)$ -comparison w.r.t. information between $I$ and $I^{'}$ . For $x \in Δ^{I}$ and $x^{'} \in Δ^{I^{'}}$ , we write $x ≲_{Φ, s}^{\inf} x^{'}$ to denote that there exists a $(Φ, s)$ -comparison w.r.t. information Z between $I$ and $I^{'}$ such that Z (x, x′) holds.

Remark 2. Given Φ, $s$ and two finite $s$ -interpretations $I$ and $I^{'}$ , we can try to construct a $(Φ, s)$ -comparison Z w.r.t. information between $I$ and $I^{'}$ as follows. At the beginning, we initialize $Z : = Δ^{I} \times Δ^{I^{'}}$ . Then, while there exists a pair 〈x, x′〉 ∈ Z that does not satisfy some conditions among (3)-(11), (14) and (15), delete that pair from Z. After that, if Z satisfies the conditions (2), (12) and (13), then it is the largest (w.r.t. ⊆) $(Φ, s)$ -comparison w.r.t. information between $I$ and $I^{'}$ . Otherwise, $I ≴_{Φ, s}^{\inf} I^{'}$ . ■

Example 2. Let us continue Example 1. Let C, R, I, $s$ , $I$ , $I^{'}$ and $I^{″}$ be as in Example 1. It can be checked that:

If Z is a $(Φ, s)$ -comparison w.r.t. information between $I$ and $I^{'}$ , then {〈u, u′〉, 〈v, v′〉, 〈w, v′〉} ⊆ Z and Q ∉ Φ. The pair 〈u, u′〉 must belong to Z due to the condition (2) and the facts that $a^{I} = u$ and $a^{I^{'}} = u^{'}$ . Consequently, the pairs 〈v, v′〉 and 〈w, v′〉 must belong to Z due to the condition (5). Conversely, if Q ∉ Φ, then {〈u, u′〉, 〈v, v′〉, 〈w, v′〉} is a $(Φ, s)$ -comparison w.r.t. information between $I$ and $I^{'}$ . If Q ∉ Φ and {I, O}∩ Φ ≠ ∅, then there are no more $(Φ, s)$ -comparisons w.r.t. information between $I$ and $I^{'}$ . If {Q, I, O}∩ Φ = ∅, then {〈u, u′〉, 〈u, v′〉, 〈v, v′〉, 〈w, v′〉} is another $(Φ, s)$ -comparison w.r.t. information between $I$ and $I^{'}$ . If Q ∈ Φ, then $u ≴_{Φ, s}^{\inf} u^{'}$ due to the condition (9), and hence the condition (2) does not hold and $I ≴_{Φ, s}^{\inf} I^{'}$ .

Z = {〈u″, u〉, 〈v″, v〉, 〈v″, w〉} is a $(Φ, s)$ -comparison w.r.t. information between $I^{″}$ and $I$ if {Q, Self}∩ Φ = ∅ and $s_{\forall \exists Q} = +$ . If, additionally, {I, O}∩ Φ ≠ ∅, then that Z is the unique $(Φ, s)$ -comparison w.r.t. information between $I^{″}$ and $I$ , otherwise there are three more, which extend that Z with 〈u″, v〉 and/or 〈u″, w〉. If Self ∈ Φ, then $v^{″} ≴_{Φ, s}^{\inf} v$ due to the conditions (14) and (15), and consequently, $u^{″} ≴_{Φ, s}^{\inf} u$ due to the condition (5), which in turn falsifies the condition (2) and causes $I ≴_{Φ, s}^{\inf} I^{'}$ . If $s_{\forall \exists Q} = \pm$ , then $v^{″} ≴_{Φ, s}^{\inf} v$ due to the condition (7), and as for the case considered in the previous sentence, $I ≴_{Φ, s}^{\inf} I^{'}$ .

$I^{'} ≴_{Φ, s}^{\inf} I$ and $I ≴_{Φ, s}^{\inf} I^{″}$ , regardless of Φ, $s_{\forall \exists Q}$ and $s_{GCI}$ .

Z = {〈u″, u′〉, 〈v″, v′〉} is a $(Φ, s)$ -comparison w.r.t. information between $I^{″}$ and $I^{'}$ , regardless of Φ, $s_{\forall \exists Q}$ and $s_{GCI}$ . ■

If $I ≲_{Φ, s}^{\inf} I^{'}$ and $I^{'} ≲_{Φ, s}^{\inf} I$ , then we say that $I$ and $I^{'}$ are $(Φ, s)$ -bisimilar to each other and denote this by $I \sim_{Φ, s} I^{'}$ . For $x \in Δ^{I}$ and $x^{'} \in Δ^{I^{'}}$ , if $x ≲_{Φ, s}^{\inf} x^{'}$ and $x^{'} ≲_{Φ, s}^{\inf} x$ , then we say that x and x′ are $(Φ, s)$ -bisimilar to each other and denote this by $x \sim_{Φ, s} x^{'}$ .

Observe that the union of a non-empty set of $(Φ, s)$ -comparisons w.r.t. information between $I$ and $I^{'}$ is also a $(Φ, s)$ -comparison w.r.t. information between $I$ and $I^{'}$ . Thus, if there exist $(Φ, s)$ -comparisons w.r.t. information between $I$ and $I^{'}$ , then the relation ${〈 x, x^{'} 〉 \in Δ^{I} \times Δ^{I^{'}} ∣ x ≲_{Φ, s}^{\inf} x^{'}}$ is the largest $(Φ, s)$ -comparison w.r.t. information between $I$ and $I^{'}$ . In the case $I^{'} = I$ , such a relation always exists and is called the largest $(Φ, s)$ -auto-comparison w.r.t. information of $I$ and denoted by $≲_{Φ, s, I}^{\inf}$ .

Given an $s$ -interpretation $I$ , we define $\sim_{Φ, s, I} = ≲_{Φ, s, I}^{\inf} \cap (≲_{Φ, s, I}^{\inf})^{- 1},$ (16) and call $\sim_{Φ, s, I}$ the $(Φ, s)$ -auto-bisimilarity (relation) of $I$ .

4 Preservation results

A concept C of ${ALC}_{Φ}$ is said to be preserved by $(Φ, s)$ -comparisons w.r.t. information if, for any $s$ -interpretations $I$ , $I^{'}$ and any $(Φ, s)$ -comparison w.r.t. information Z between $I$ and $I^{'}$ , if Z (x, x′) holds and $x \in C_{+}^{I}$ , then $x \in C_{+}^{I^{'}}$ .

A TBox $T$ in ${ALC}_{Φ}$ is said to be preserved by $(Φ, s)$ -comparisons w.r.t. information if, for every $s$ -interpretations $I$ and $I^{'}$ such that $I ≲_{Φ, s}^{\inf} I^{'}$ , if $I ⊨_{s} T$ , then $I ⊨_{s} T^{'}$ . A similar notion for ABoxes is defined analogously.

Theorem 1. All concepts of ${ALC}_{Φ}$ are preserved by $(Φ, s)$ -comparisons w.r.t. information.

Proof. This proof is similar to the one of [5, Theorem 3.4]. Let Z be a $(Φ, s)$ -comparison w.r.t. information between $s$ -interpretations $I$ and $I^{'}$ . Suppose that Z (x, x′) holds and $x \in C_{+}^{I}$ , where C is a concept of ${ALC}_{Φ}$ . We show that $x^{'} \in C_{+}^{I^{'}}$ . Without loss of generality, we assume that C is in the negation normal form (i.e., ¬ can occur in C only immediately before subconcepts of the form A, {a} or ∃r . Self). We prove the assertion by induction on the structure of C. The cases when C is of the form ⊤, ⊥, A, ¬A, D ⊔ D′ or D ⊓ D′ are trivial.

Case C = ∃ R . D: Since $x \in C_{+}^{I}$ , there exists $y \in D_{+}^{I}$ such that $R_{+}^{I} (x, y)$ holds. Since Z (x, x′) holds, by (5) and (12), there exists $y^{'} \in Δ^{I^{'}}$ such that Z (y, y′) and $R_{+}^{I^{'}} (x^{'}, y^{'})$ hold. Since Z (y, y′) holds and $y \in D_{+}^{I}$ , by the inductive assumption, $y^{'} \in D_{+}^{I^{'}}$ . Therefore, $x^{'} \in C_{+}^{I^{'}}$ .

Case C = ∀ R . D: Let y′ be an arbitrary element of $Δ^{I^{'}}$ such that $〈 x^{'}, y^{'} 〉 \in R_{+}^{I^{'}}$ (resp. $〈 x^{'}, y^{'} 〉 \notin R_{-}^{I^{'}}$ ) if $s_{\forall \exists Q} = +$ (resp. $s_{\forall \exists Q} = \pm$ ). We need to show that $y^{'} \in D_{+}^{I^{'}}$ . Since Z (x, x′) holds, by (6), (7) and (13), there exists $y \in Δ^{I}$ such that Z (y, y′) holds and $〈 x, y 〉 \in R_{+}^{I}$ (resp. $〈 x, y 〉 \notin R_{-}^{I}$ ) if $s_{\forall \exists Q} = +$ (resp. $s_{\forall \exists Q} = \pm$ ). Since $x \in C_{+}^{I}$ , it follows that $y \in D_{+}^{I}$ . Since Z (y, y′) holds, by the inductive assumption, it follows that $y^{'} \in D_{+}^{I^{'}}$ .

Case O ∈ Φ and C = {a} (resp. C = ¬ {a}): Since $x \in C_{+}^{I}$ , we have that $x = a^{I}$ (resp. $x \neq a^{I}$ ). By (8), it follows that $x^{'} = a^{I^{'}}$ (resp. $x^{'} \neq a^{I^{'}}$ ). Hence $C^{I^{'}} (x^{'})$ holds.

Case Self ∈ Φ and C = ∃ r . Self (resp. C = ¬ ∃ r . Self): Since $x \in C_{+}^{I}$ , we have that $r_{+}^{I} (x, x)$ (resp. $r_{-}^{I} (x, x)$ ) holds. Since Z (x, x′) holds, by (14) (resp. (15)), it follows that $r_{+}^{I^{'}} (x^{'}, x^{'})$ (resp. $r_{-}^{I^{'}} (x^{'}, x^{'})$ ) holds. Hence $C^{I^{'}} (x^{'})$ holds.

Case Q ∈ Φ and C = (≥ n R . D): Since $x \in C_{+}^{I}$ , there exist pairwise different y₁, …, $y_{n} \in D_{+}^{I}$ such that $R_{+}^{I} (x, y_{i})$ hold for all 1 ≤ i ≤ n. Since Z (x, x′) holds, by (9), there exist pairwise different $y_{1}^{'}$ , …, $y_{n}^{'} \in Δ^{I^{'}}$ such that $R_{+}^{I^{'}} (x^{'}, y_{i}^{'})$ and $Z (y_{i}, y_{i}^{'})$ hold for all 1 ≤ i ≤ n. Since $Z (y_{i}, y_{i}^{'})$ holds and $y_{i} \in D_{+}^{I}$ , by the inductive assumption, $y_{i}^{'} \in D_{+}^{I^{'}}$ . It follows that $x^{'} \in C_{+}^{I^{'}}$ .

Case Q ∈ Φ and C = (≤ n R . D): For a contradiction, suppose $x^{'} \notin C_{+}^{I^{'}}$ . Thus, there exist pairwise different $y_{1}^{'}$ , …, $y_{n + 1}^{'} \in Δ^{I^{'}}$ such that $〈 x^{'}, y_{i}^{'} 〉 \in R_{+}^{I^{'}}$ (resp. $〈 x^{'}, y_{i}^{'} 〉 \notin R_{-}^{I^{'}}$ ) if $s_{\forall \exists Q} = +$ (resp. $s_{\forall \exists Q} = \pm$ ), and $y_{i}^{'} \notin D_{-}^{I^{'}}$ , for all 1 ≤ i ≤ n + 1. Since Z (x, x′) holds, by (10) and (11), there exist pairwise different y₁, …, $y_{n + 1} \in Δ^{I}$ such that $Z (y_{i}, y_{i}^{'})$ holds and $〈 x, y_{i} 〉 \in R_{+}^{I}$ (resp. $〈 x, y_{i} 〉 \notin R_{-}^{I}$ ) if $s_{\forall \exists Q} = +$ (resp. $s_{\forall \exists Q} = \pm$ ), for all 1 ≤ i ≤ n + 1. For each 1 ≤ i ≤ n + 1, since $Z (y_{i}, y_{i}^{'})$ holds and $y_{i}^{'} \notin (\neg D)_{+}^{I^{'}}$ , by the inductive assumption, $y_{i} \notin (\neg D)_{+}^{I}$ , which means $y_{i} \notin D_{-}^{I}$ . Therefore, $x \notin C_{+}^{I}$ , a contradiction. ■

Corrolary 1. Let $I$ and $I^{'}$ be $s$ -interpretations. Then, for every $x \in Δ^{I}$ , $x^{'} \in Δ^{I^{'}}$ and every concept C of ${ALC}_{Φ}$ , if $x \sim_{Φ, s} x^{'}$ , then $x \in C_{+}^{I}$ iff $x^{'} \in C_{+}^{I^{'}}$ , and $x \in C_{-}^{I}$ iff $x^{'} \in C_{-}^{I^{'}}$ .

Proof. This corollary immediately follows from Theorem 1 because $x \in C_{-}^{I}$ (resp. $x^{'} \in C_{-}^{I^{'}}$ ) iff $x \in (\neg C)_{+}^{I}$ (resp. $x^{'} \in (\neg C)_{+}^{I^{'}}$ ). ■

Corrolary 2. If U ∈ Φ and $s_{GCI} = w$ , then:

all TBoxes in ${ALC}_{Φ}$ are preserved by $(Φ, s)$ -comparisons w.r.t. information,

if $T$ is a TBox in ${ALC}_{Φ}$ and $I$ , $I^{'}$ are $(Φ, s)$ -bisimilar $s$ -interpretations, then $I ⊨_{s} T$ iff $I ⊨_{s} T^{'}$ .

Proof. The second assertion immediately follows from the first one. Consider the first assertion and suppose that U ∈ Φ and $s_{GCI} = w$ . Let Z be a $(Φ, s)$ -comparison w.r.t. information between $s$ -interpretations $I$ and $I^{'}$ . Suppose that $I ⊨_{s} C ⊑ D$ . We show that $I^{'} ⊨_{s} C ⊑ D$ . Take an arbitrary $x^{'} \in Δ^{I^{'}}$ , we need to show that $x^{'} \in C_{-}^{I^{'}} \cup D_{+}^{I^{'}}$ . By (13), there exists $x \in Δ^{I}$ such that Z (x, x′) holds. Since $I ⊨_{s} C ⊑ D$ , we have that $x \in C_{-}^{I} \cup D_{+}^{I}$ , and hence $x \in (\neg C ⊔ D)_{+}^{I}$ . Since Z (x, x′) holds, by Theorem 1, it follows that $x^{'} \in (\neg C ⊔ D)_{+}^{I^{'}}$ , which means that $x^{'} \in C_{-}^{I^{'}} \cup D_{+}^{I^{'}}$ . ■

An $s$ -interpretation $I$ is said to be $(Φ, s)$ -unreachable-object-free if every element of $Δ^{I}$ is reachable from some $a^{I}$ , where a ∈ I, via a path consisting of edges being instances of relations $R_{+}^{I}$ (resp. $(Δ^{I} \times Δ^{I}) \ R_{-}^{I}$ ) for the case $s_{\forall \exists Q} = +$ (resp. $s_{\forall \exists Q} = \pm$ ), where R is a role of ${ALC}_{Φ}$ different from U.

An $s$ -interpretation $I$ is said to be strongly Φ-unreachable-object-free if every element of $Δ^{I}$ is reachable from some $a^{I}$ , where a ∈ I, via a path consisting of edges being instances of relations $R_{+}^{I}$ and via a path consisting of edges being instances of relations $(Δ^{I} \times Δ^{I}) \ R_{-}^{I}$ , where R is a role of ${ALC}_{Φ}$ different from U.

Theorem 2. Suppose that $s_{GCI} = w$ . Let $I$ and $I^{'}$ be $s$ -interpretations. If $I ≲_{Φ, s}^{\inf} I^{'}$ and $I^{'}$ is $(Φ, s)$ -unreachable-object-free, then, for every TBox $T$ in ${ALC}_{Φ}$ , if $I ⊨_{s} T$ then $I^{'} ⊨_{s} T$ .

Proof. Suppose that Z is a $(Φ, s)$ -comparison w.r.t. information between $I$ and $I^{'}$ , $I^{'}$ is $(Φ, s)$ -unreachable-object-free, and $I ⊨_{s} T$ . We show that $I^{'} ⊨_{s} T$ . Let $(C ⊑ D) \in T$ and $x^{'} \in Δ^{I^{'}}$ . We need to show that $x^{'} \in C_{-}^{I^{'}} \cup D_{+}^{I^{'}}$ . Since $I^{'}$ is $(Φ, s)$ -unreachable-object-free, there exists a sequence $x_{0}^{'}, \dots, x_{k}^{'}$ of elements of $Δ^{I^{'}}$ such that $x_{0}^{'} = a^{I^{'}}$ for some a ∈ I, $x_{k}^{'} = x^{'}$ , and for every 0 < i ≤ k, $〈 x_{i - 1}^{'}, x_{i}^{'} 〉 \in (R_{i})_{+}^{I^{'}}$ (resp. $〈 x_{i - 1}^{'}, x_{i}^{'} 〉 \notin (R_{i})_{-}^{I^{'}}$ ) if $s_{\forall \exists Q} = +$ (resp. $s_{\forall \exists Q} = \pm$ ), where R_i is a role of ${ALC}_{Φ}$ different from U. By (2), (6) and (7), there exists a sequence x₀, …, x_k of elements of $Δ^{I}$ such that $x_{0} = a^{I}$ , x_k = x, and for every 0 < i ≤ k, $Z (x_{i}, x_{i}^{'})$ holds and $〈 x_{i}, x_{i + 1} 〉 \in (R_{i})_{+}^{I}$ (resp. $〈 x_{i}, x_{i + 1} 〉 \notin (R_{i})_{-}^{I}$ ) if $s_{\forall \exists Q} = +$ (resp. $s_{\forall \exists Q} = \pm$ ). Thus, Z (x, x′) holds. Since $I ⊨_{s} C ⊑ D$ , we have $x \in (\neg C ⊔ D)_{+}^{I}$ . Since Z (x, x′) holds, by Theorem 1, it follows that $x^{'} \in (\neg C ⊔ D)_{+}^{I^{'}}$ , which means $x^{'} \in C_{-}^{I^{'}} \cup D_{+}^{I^{'}}$ . This completes the proof. ■

Corrolary 3. Suppose that $s_{GCI} = w$ . Let $I$ and $I^{'}$ be $s$ -interpretations such that they are $(Φ, s)$ -unreachable-object-free and $(Φ, s)$ -bisimilar to each other. Then, for every TBox $T$ in ${ALC}_{Φ}$ , $I ⊨_{s} T$ iff $I^{'} ⊨_{s} T$ .

This corollary follows from Theorem 2.

Theorem 3.An ABox $A$ in ${ALC}_{Φ}$ is preserved by $(Φ, s)$ -comparisons w.r.t. information in the following cases:

$A$ contains only assertions of the form C (a),

O ∈ Φ and $s_{\forall \exists Q} = \pm$ ,

O ∈ Φ and $A$ does not contain assertions of the form ¬R (a, b).

As a consequence, if one of the above conditions holds and

I

I^{'}

are

s

-interpretations

(Φ, s)

-bisimilar to each other, then

I ⊨_{s} A

iff

I^{'} ⊨_{s} A

Proof. This proof is similar to the one of [5, Theorem 3.7]. Assume that some of the conditions of the theorem hold. Let Z be a $(Φ, s)$ -comparison w.r.t. information between $s$ -interpretations $I$ and $I^{'}$ and suppose that $I ⊨_{s} A$ . Let φ be an assertion from $A$ . We need to show that $I^{'} ⊨_{s} φ$ .

Case φ = (a ≐ b): Since $I ⊨_{s} φ$ , we have that $a^{I} = b^{I}$ . By (2), $Z (a^{I}, a^{I^{'}})$ and $Z (b^{I}, b^{I^{'}})$ hold. Since $a^{I} = b^{I}$ , by (8), it follows that $a^{I^{'}} = b^{I^{'}}$ . Hence $I^{'} ⊨_{s} φ$ .

Case φ = (a ≠ b): The proof is similar to the above case (with the three occurrences of = replaced by ≠).

Case φ = C (a): By (2), $Z (a^{I}, a^{I^{'}})$ holds. Since $I ⊨_{s} φ$ , $a^{I} \in C_{+}^{I}$ . By Theorem 1, it follows that $a^{I^{'}} \in C_{+}^{I^{'}}$ . Thus $I^{'} ⊨_{s} φ$ .

Case φ = R (a, b): By (2), $Z (a^{I}, a^{I^{'}})$ holds. Since $I ⊨_{s} φ$ , $R_{+}^{I} (a^{I}, b^{I})$ holds. By (5), there exists $y^{'} \in Δ^{I^{'}}$ such that $Z (b^{I}, y^{'})$ and $R_{+}^{I^{'}} (a^{I^{'}}, y^{'})$ hold. Consider C = {b} (the assumption O ∈ Φ is used here). Since $Z (b^{I}, y^{'})$ and $b^{I} \in C_{+}^{I}$ hold, by Theorem 1, $y^{'} \in C_{+}^{I^{'}}$ , which means $y^{'} = b^{I^{'}}$ . Thus, $R_{+}^{I^{'}} (a^{I^{'}}, b^{I^{'}})$ holds, i.e., $I^{'} ⊨_{s} φ$ .

Case φ = ¬ R (a, b): We must have that O ∈ Φ and $s_{\forall \exists Q} = \pm$ . By (2), $Z (a^{I}, a^{I^{'}})$ holds. Since $I ⊨_{s} φ$ , $R_{-}^{I} (a^{I}, b^{I})$ holds. Since $Z (a^{I}, a^{I^{'}})$ holds, by (7), it follows that $R_{-}^{I^{'}} (a^{I^{'}}, b^{I^{'}})$ holds, otherwise there would exist $y \in Δ^{I}$ such that $Z (y, b^{I^{'}})$ and $\neg R_{-}^{I} (a^{I}, y)$ hold, which implies $y = b^{I}$ and that $R_{-}^{I} (a^{I}, b^{I})$ does not hold (a contradiction). Therefore, $I^{'} ⊨_{s} φ$ . ■

5 The Hennessy-Milner property

An $s$ -interpretation $I$ is said to be modally Φ-saturated w.r.t. kind 1 if:

for every $x \in Δ^{I}$ , every role R of ${ALC}_{Φ}$ different from U and every infinite set Γ of concepts of ${ALC}_{Φ}$ , if for every finite subset Λ of Γ there exists $y \in Δ^{I}$ such that $〈 x, y 〉 \in R_{+}^{I}$ and $y \in Λ_{+}^{I}$ , then there exists $y \in Δ^{I}$ such that $〈 x, y 〉 \in R_{+}^{I}$ and $y \in Γ_{+}^{I}$ ;

if Q ∈ Φ then, for every $x \in Δ^{I}$ , every role R of ${ALC}_{Φ}$ different from U, every infinite set Γ of concepts of ${ALC}_{Φ}$ and every natural number n, if for every finite subset Λ of Γ there exist n pairwise different $y_{1}, \dots, y_{n} \in Δ^{I}$ such that $〈 x, y_{i} 〉 \in R_{+}^{I}$ and $y_{i} \in Λ_{+}^{I}$ for all 1 ≤ i ≤ n, then there exist n pairwise different $y_{1}, \dots, y_{n} \in Δ^{I}$ such that $〈 x, y_{i} 〉 \in R_{+}^{I}$ and $y_{i} \in Γ_{+}^{I}$ for all 1 ≤ i ≤ n;

if U ∈ Φ and $I$ is not strongly Φ-unreachable-objects-free then, for every infinite set Γ of concepts of ${ALC}_{Φ}$ , if $Λ_{+}^{I} \neq \emptyset$ for every finite subset Λ of Γ, then $Γ_{+}^{I} \neq \emptyset$ .

An $s$ -interpretation $I$ is said to be modally Φ-saturated w.r.t. kind 2 (resp. kind 3) if:

for every $x \in Δ^{I}$ , every role R of ${ALC}_{Φ}$ different from U and every infinite set Γ of concepts of ${ALC}_{Φ}$ , if for every finite subset Λ of Γ there exists $y \in Δ^{I}$ such that $〈 x, y 〉 \in R_{+}^{I}$ (resp. $〈 x, y 〉 \notin R_{-}^{I}$ ) and $y \notin Λ_{-}^{I}$ , then there exists $y \in Δ^{I}$ such that $〈 x, y 〉 \in R_{+}^{I}$ (resp. $〈 x, y 〉 \notin R_{-}^{I}$ ) and $y \notin Γ_{-}^{I}$ ;

if Q ∈ Φ then, for every $x \in Δ^{I}$ , every role R of ${ALC}_{Φ}$ different from U, every infinite set Γ of concepts of ${ALC}_{Φ}$ and every natural number n, if for every finite subset Λ of Γ there exist n pairwise different $y_{1}, \dots, y_{n} \in Δ^{I}$ such that $〈 x, y_{i} 〉 \in R_{+}^{I}$ (resp. $〈 x, y_{i} 〉 \notin R_{-}^{I}$ ) and $y_{i} \notin Λ_{-}^{I}$ for all 1 ≤ i ≤ n, then there exist n pairwise different $y_{1}, \dots, y_{n} \in Δ^{I}$ such that $〈 x, y_{i} 〉 \in R_{+}^{I}$ (resp. $〈 x, y_{i} 〉 \notin R_{-}^{I}$ ) and $y_{i} \notin Γ_{-}^{I}$ for all 1 ≤ i ≤ n;

if U ∈ Φ and $I$ is not strongly Φ-unreachable-objects-free then, for every infinite set Γ of concepts of ${ALC}_{Φ}$ , if $Λ_{-}^{I} \neq Δ^{I}$ for every finite subset Λ of Γ, then $Γ_{-}^{I} \neq Δ^{I}$ .

We say that an $s$ -interpretation $I$ is strongly modally Φ-saturated if it is modally Φ-saturated w.r.t. all of the kinds 1, 2 and 3.

Proposition 2. If $s_{C} = s_{R} = 2$ (i.e., $s$ is the two-valued logic), then the three kinds of being modally Φ-saturated are equivalent to each other.

The proof of this proposition is straightforward.

An $s$ -interpretation $I$ is finitely branching (w.r.t. Φ) if, for every $x \in Δ^{I}$ and every role R of ${ALC}_{Φ}$ different from U, the sets ${y \in Δ^{I} ∣ 〈 x, y 〉 \in R_{+}^{I}}$ and ${y \in Δ^{I} ∣ 〈 x, y 〉 \notin R_{-}^{I}}$ are finite.

The following proposition gives examples of modally Φ-saturated interpretations. Its proof is straightforward.

Proposition 3. Every finite interpretation is strongly modally Φ-saturated. Every finitely branching and strongly Φ-unreachable-objects-free interpretation is strongly modally Φ-saturated. If U ∉ Φ then every finitely branching interpretation is strongly modally Φ-saturated.

Let $I$ and $I^{'}$ be $s$ -interpretations, $x \in Δ^{I}$ and $x^{'} \in Δ^{I^{'}}$ . We say that:

x is less than or equal tox′ w.r.t. concepts of ${ALC}_{Φ}$ and the semantics $s$ , denoted by $x \leq_{Φ, s}^{\inf} x^{'}$ , if, for every concept C of ${ALC}_{Φ}$ , $x \in C_{+}^{I}$ implies $x^{'} \in C_{+}^{I^{'}}$ ;

x is $s$ -equivalent tox′ w.r.t. concepts of ${ALC}_{Φ}$ , denoted by $x \equiv_{Φ, s} x^{'}$ , if, for every concept C of ${ALC}_{Φ}$ , $x \in C_{+}^{I}$ iff $x^{'} \in C_{+}^{I^{'}}$ .

For the main theorem of this section, we need [2, Lemma 4.6] and recall it below. The lemma allows us to check the conditions (9)–(11) in another way.

Lemma 1. [2, Lemma 4.6] Let Z ⊆ S × S′ be a binary relation such that, for any natural number n and any pairwise different x₁, …, x_n ∈ S, there exist pairwise different $x_{1}^{'}, \dots, x_{n}^{'} \in S^{'}$ with the property that, for any 1 ≤ j ≤ n, there exists 1 ≤ i ≤ n such that $〈 x_{i}, x_{j}^{'} 〉 \in Z$ . Then, for any natural number n and any pairwise different x₁, …, x_n ∈ S, there exist pairwise different $x_{1}^{'}, \dots, x_{n}^{'} \in S^{'}$ such that $〈 x_{i}, x_{i}^{'} 〉 \in Z$ for all 1 ≤ i ≤ n.

Theorem 4.Let $I$ and $I^{'}$ be $s$ -interpretations such that, for every a ∈ I, $a^{I} \leq_{Φ, s}^{\inf} a^{I^{'}}$ . Suppose that:

$I^{'}$ is modally Φ-saturated w.r.t. kind 1,

if $s_{\forall \exists Q} = +$ (resp. $s_{\forall \exists Q} = \pm$ ), then $I$ is modally Φ-saturated w.r.t. kind 2 (resp. kind 3),

if U ∈ Φ then either both $I$ and $I^{'}$ are strongly Φ-unreachable-object-free, or both of them are not strongly Φ-unreachable-object-free, or both of them are finite.

Then, for every

x \in Δ^{I}

and

x^{'} \in Δ^{I^{'}}

x \leq_{Φ, s}^{\inf} x^{'}

iff

x ≲_{Φ, s}^{\inf} x^{'}

. In particular, the relation

{〈 x, x^{'} 〉 \in Δ^{I} \times Δ^{I^{'}} ∣ x \leq_{Φ, s}^{\inf} x^{'}}

is a

(Φ, s)

-comparison w.r.t. information between

I

and

I^{'}

when it is not empty.

Proof. This proof is similar to the ones of [4, Lemma 4.6] and [2, Theorem 4.7]. First, suppose Z is a $(Φ, s)$ -comparison w.r.t. information between $I$ and $I^{'}$ such that Z (x, x′) holds. We show that $x \leq_{Φ, s}^{\inf} x^{'}$ . Let C be an arbitrary concept of ${ALC}_{Φ}$ such that $x \in C_{+}^{I}$ . Since Z (x, x′) holds, by Theorem 1, $x^{'} \in C_{+}^{I^{'}}$ . Therefore, $x \leq_{Φ, s}^{\inf} x^{'}$ .

Conversely, let $Z = {〈 x, x^{'} 〉 \in Δ^{I} \times Δ^{I^{'}} ∣ x \leq_{Φ, s}^{\inf} x^{'}}$ and assume that Z is not empty. We show that Z is a $(Φ, s)$ -comparison w.r.t. information between $I$ and $I^{'}$ .

The condition (2) immediately follows from the assumption of the theorem.

Consider the condition (3). If Z (x, x′) and $A_{+}^{I} (x)$ hold, then by the definition of Z, $A_{+}^{I^{'}} (x^{'})$ holds.

Consider the condition (4). If Z (x, x′) and $A_{-}^{I} (x)$ hold, then $(\neg A)_{+}^{I} (x)$ holds, and by the definition of Z, $(\neg A)_{+}^{I^{'}} (x^{'})$ holds, which means $A_{-}^{I^{'}} (x^{'})$ holds.

Consider the condition (5). Suppose Z (x, x′) and $R_{+}^{I} (x, y)$ hold. Let $S = {y^{'} \in Δ^{I^{'}} ∣ R_{+}^{I^{'}} (x^{'}, y^{'})}$ . We show that there exists y′ ∈ S such that Z (y, y′) holds. For a contradiction, suppose that, for every y′ ∈ S, Z (y, y′) does not hold, which means that $y ≰_{Φ, s}^{\inf} y^{'}$ . Thus, for every y′ ∈ S, there exists a concept C_y′ of ${ALC}_{Φ}$ such that $y \in (C_{y^{'}})_{+}^{I}$ but $y^{'} \notin (C_{y^{'}})_{+}^{I^{'}}$ . Let Γ = {C_y′ ∣ y′ ∈ S}. Thus, $S \cap Γ_{+}^{I^{'}} = \emptyset$ . Since $I^{'}$ is Φ-saturated w.r.t. kind 1, it follows that there exists a finite subset Λ of Γ such that, for every y′ ∈ S, $y^{'} \notin Λ_{+}^{I^{'}}$ . Consider the concept C = ∃ R . ⊓ Λ of ${ALC}_{Φ}$ . We have $x \in C_{+}^{I}$ , but $x^{'} \notin C_{+}^{I^{'}}$ . This contradicts $x \leq_{Φ, s}^{\inf} x^{'}$ .

Consider the conditions (6) and (7). Suppose that Z (x, x′) holds and, if $s_{\forall \exists Q} = +$ (resp. $s_{\forall \exists Q} = \pm$ ), then $R_{+}^{I^{'}} (x^{'}, y^{'})$ (resp. $\neg R_{-}^{I^{'}} (x^{'}, y^{'})$ ) holds. Let $S = {y \in Δ^{I} ∣ R_{+}^{I} (x, y)}$ (resp. $S = {y \in Δ^{I} ∣ \neg R_{-}^{I} (x, y)}$ ). We show that there exists y ∈ S such that Z (y, y′) holds. For a contradiction, suppose that, for every y ∈ S, Z (y, y′) does not hold, i.e. $y ≰_{Φ, s}^{\inf} y^{'}$ . Thus, for every y ∈ S, there exists a concept C_y of ${ALC}_{Φ}$ such that $y \in (C_{y})_{+}^{I}$ but $y^{'} \notin (C_{y})_{+}^{I^{'}}$ . Let Γ = {¬ C_y ∣ y ∈ S}. Consider any finite subset Λ of Γ and let C = ∃ R . ⊓ Λ. Observe that $x^{'} \notin (\neg C)_{+}^{I^{'}}$ . Since $x \leq_{Φ, s}^{\inf} x^{'}$ , it follows that $x \notin (\neg C)_{+}^{I}$ . This means that there exists y ∈ S such that $y \notin Λ_{-}^{I}$ . Since $I$ is Φ-saturated w.r.t. kind 2 (resp. kind 3), it follows that there exists y ∈ S such that $y \notin Γ_{-}^{I}$ , which contradicts the fact $y \in (C_{y})_{+}^{I}$ .

Consider the condition (8) and the case O ∈ Φ. Suppose Z (x, x′) holds and $x = a^{I}$ (resp. $x \neq a^{I}$ ). Since $x \in {a}_{+}^{I}$ (resp. $x \in (\neg {a})_{+}^{I}$ ) and $x \leq_{Φ, s}^{\inf} x^{'}$ , it follows that $x^{'} \in {a}_{+}^{I^{'}}$ (resp. $x^{'} \in (\neg {a})_{+}^{I^{'}}$ ). Therefore, $x^{'} = a^{I^{'}}$ (resp. $x^{'} \neq a^{I^{'}}$ ).

Consider the condition (9) and the case Q ∈ Φ. Suppose Z (x, x′) holds, i.e., $x \leq_{Φ, s}^{\inf} x^{'}$ . Let $S = {y \in Δ^{I} ∣ R_{+}^{I} (x, y)}$ and $S^{'} = {y^{'} \in Δ^{I^{'}} ∣ R_{+}^{I^{'}} (x^{'}, y^{'})}$ . Let y₁, …, y_n be pairwise different elements of S. Let S″ = {y′∈ S′ ∣ there exists 1 ≤ i ≤ n such that $y_{i} \leq_{Φ, s}^{\inf} y^{'}}$ . To prove the condition (9), by Lemma 1, it is sufficient to prove that # S″ ≥ n. For each y′ ∈ S′ \ S″, there exist concepts D_y′,1, …, D_y′,n of ${ALC}_{Φ}$ such that $y_{i} \in (D_{y^{'}, i})_{+}^{I}$ and $y^{'} \notin (D_{y^{'}, i})_{+}^{I^{'}}$ for every 1 ≤ i ≤ n. For each y′ ∈ S′ \ S″, let C_y′ = D_y′,1 ⊔ … ⊔ D_y′,n, then we have that $y_{i} \in (C_{y^{'}})_{+}^{I}$ for all 1 ≤ i ≤ n, but $y^{'} \notin (C_{y^{'}})_{+}^{I^{'}}$ . Let Γ = {C_y′ ∣ y′ ∈ S′ \ S″}. Note that $Γ_{+}^{I^{'}} \cap (S^{'} \ S^{″}) = \emptyset$ . For every finite subset Λ of Γ and for C = (≥ n R . ⊓ Λ), since $y_{1}, \dots, y_{n} \in Λ_{+}^{I}$ , we have $x \in C_{+}^{I}$ , and since $x \leq_{Φ, s}^{\inf} x^{'}$ , we also have that $x^{'} \in C_{+}^{I^{'}}$ , which means there are at least n pairwise different $y_{1}^{'}, \dots, y_{n}^{'} \in S^{'}$ that belong to $Λ_{+}^{I^{'}}$ . Since $I^{'}$ is Φ-saturated w.r.t. kind 1, it follows that there are at least n pairwise different $y_{1}^{'}, \dots, y_{n}^{'} \in S^{'}$ that belong to $Γ_{+}^{I^{'}}$ . Since $Γ_{+}^{I^{'}} \cap (S^{'} \ S^{″}) = \emptyset$ , it follows that # S″ ≥ n.

Consider the condition (10) (resp. (11)) and the case $s_{\forall \exists Q} = +$ (resp. $s_{\forall \exists Q} = \pm$ ) and Q ∈ Φ. Suppose Z (x, x′) holds, i.e., $x \leq_{Φ, s}^{\inf} x^{'}$ . Let $S = {y \in Δ^{I} ∣ R_{+}^{I} (x, y)}$ and $S^{'} = {y^{'} \in Δ^{I^{'}} ∣ R_{+}^{I^{'}} (x^{'}, y^{'})}$ (resp. $S = {y \in Δ^{I} ∣ \neg R_{-}^{I} (x, y)}$ and $S^{'} = {y^{'} \in Δ^{I^{'}} ∣ \neg R_{-}^{I^{'}} (x^{'}, y^{'})}$ ). Let $y_{1}^{'}, \dots, y_{n}^{'}$ be pairwise different elements of S′. Let S″ = {y∈ S ∣ there exists 1 ≤ i ≤ n such that $y \leq_{Φ, s}^{\inf} y_{i}^{'}}$ . To prove the conditions (10) and (11), by Lemma 1, it is sufficient to prove that # S″ ≥ n. For each y ∈ S \ S″, there exist concepts D_y,1, …, D_y,n of ${ALC}_{Φ}$ such that $y \in (D_{y, i})_{+}^{I}$ and $y_{i}^{'} \notin (D_{y, i})_{+}^{I^{'}}$ for every 1 ≤ i ≤ n. For each y ∈ S \ S″, let C_y = D_y,1 ⊓ … ⊓ D_y,n, then we have that $y \in (C_{y})_{+}^{I}$ , but $y_{i}^{'} \notin (C_{y})_{+}^{I^{'}}$ for all 1 ≤ i ≤ n. Let Γ = {¬ C_y ∣ y ∈ S \ S″}. Consider any finite subset Λ of Γ and let C = (≥ n R . ⊓ Λ). Observe that $x^{'} \notin (\neg C)_{+}^{I^{'}}$ . Since $x \leq_{Φ, s}^{\inf} x^{'}$ , it follows that that $x \notin (\neg C)_{+}^{I}$ . This means there are at least n pairwise different y₁, …, y_n ∈ S such that $y_{i} \notin Λ_{-}^{I}$ for 1 ≤ i ≤ n. Since $I$ is Φ-saturated w.r.t. kind 2 (resp. kind 3), it follows that there are at least n pairwise different y₁, …, y_n ∈ S such that $y_{i} \notin Γ_{-}^{I}$ , and hence y_i ∈ S″, for 1 ≤ i ≤ n. Therefore,# S″ ≥ n.

Consider the condition (12) and the case U ∈ Φ.

If $I$ is strongly Φ-unreachable-objects-free then (12) follows from (2) and (5). Consider the case when $I$ is not strongly Φ-unreachable-objects-free and not finite. Thus, $I^{'}$ is also not strongly Φ-unreachable-objects-free. Since Z is not empty, there exists 〈y, y′〉 ∈ Z. We have $y \leq_{Φ, s}^{\inf} y^{'}$ . Let $x \in Δ^{I}$ . For a contradiction, suppose there is no $x^{'} \in Δ^{I^{'}}$ such that $x \leq_{Φ, s}^{\inf} x^{'}$ . Thus, for every $x^{'} \in Δ^{I^{'}}$ , there exists a concept C_x′ of ${ALC}_{Φ}$ such that $x \in (C_{x^{'}})_{+}^{I}$ but $x^{'} \notin (C_{x^{'}})_{+}^{I^{'}}$ . Let $Γ = {C_{x^{'}} ∣ x^{'} \in Δ^{I^{'}}}$ . For any finite subset Λ of Γ, since $x \in Λ_{+}^{I}$ , we have that $y \in (\exists U . ⊓ Λ)_{+}^{I}$ , which implies that $y^{'} \in (\exists U . ⊓ Λ)_{+}^{I^{'}}$ (since $y \leq_{Φ, s}^{\inf} y^{'}$ ), which means $Λ_{+}^{I^{'}} \neq \emptyset$ . Since $I^{'}$ is modally Φ-saturated w.r.t. kind 1 and not strongly Φ-unreachable-objects-free, it follows that $Γ_{+}^{I^{'}} \neq \emptyset$ , which contradicts the fact that $x^{'} \notin (C_{x^{'}})_{+}^{I^{'}}$ for every $x^{'} \in Δ^{I^{'}}$ . The case when $I$ is finite can be proved analogously as for the above case.

Consider the condition (13) and the case U ∈ Φ.

If $I^{'}$ is strongly Φ-unreachable-objects-free then (13) follows from (2), (6) and (7). Consider the case when $I^{'}$ is not strongly Φ-unreachable-objects-free and not finite. Thus, $I$ is also not strongly Φ-unreachable-objects-free. Since Z is not empty, there exists 〈y, y′〉 ∈ Z. We have $y \leq_{Φ, s}^{\inf} y^{'}$ . Let $x^{'} \in Δ^{I^{'}}$ . For a contradiction, suppose there is no $x \in Δ^{I}$ such that $x \leq_{Φ, s}^{\inf} x^{'}$ . Thus, for every $x \in Δ^{I}$ , there exists a concept C_x of ${ALC}_{Φ}$ such that $x \in (C_{x})_{+}^{I}$ but $x^{'} \notin (C_{x})_{+}^{I^{'}}$ . Let $Γ = {\neg C_{x} ∣ x \in Δ^{I}}$ . Consider any finite subset Λ of Γ and let C = ∃ U . ⊓ Λ. Observe that $x^{'} \notin Λ_{-}^{I^{'}}$ , hence $y^{'} \notin (\neg C)_{+}^{I^{'}}$ . Since $y \leq_{Φ, s}^{\inf} y^{'}$ , it follows that $y \notin (\neg C)_{+}^{I}$ . This implies that $Λ_{-}^{I} \neq Δ^{I}$ . Since $I$ is modally Φ-saturated w.r.t. kind 2 or 3 and not strongly Φ-unreachable-objects-free, it follows that $Γ_{-}^{I} \neq Δ^{I}$ , which contradicts the fact that $x \in (C_{x})_{+}^{I}$ for every $x \in Δ^{I}$ . The case when $I^{'}$ is finite can be proved analogously as for the above case.

Consider the condition (14) and the case Self ∈ Φ. Suppose Z (x, x′) and $r_{+}^{I} (x, x)$ hold. Since $x \in (\exists r . Self)_{+}^{I}$ and $x \leq_{Φ, s}^{\inf} x^{'}$ , it follows that $x^{'} \in (\exists r . Self)_{+}^{I^{'}}$ . Hence, $r_{+}^{I^{'}} (x^{'}, x^{'})$ holds.

Consider the condition (15) and the case Self ∈ Φ. Suppose Z (x, x′) and $r_{-}^{I} (x, x)$ hold. Since $x \in (\neg \exists r . Self)_{+}^{I}$ and $x \leq_{Φ, s}^{\inf} x^{'}$ , it follows that $x^{'} \in (\neg \exists r . Self)_{+}^{I^{'}}$ . Hence, $r_{-}^{I^{'}} (x^{'}, x^{'})$ holds. ■

Corollary 4. Let $I$ and $I^{'}$ be strongly modally Φ-saturated $s$ -interpretations such that $a^{I} \equiv_{Φ, s} a^{I^{'}}$ for every a ∈ I. If U ∉ Φ then, for every $x \in Δ^{I}$ and $x^{'} \in Δ^{I^{'}}$ , $x \equiv_{Φ, s} x^{'}$ iff $x \sim_{Φ, s} x^{'}$ .

This corollary follows from Theorem 4.

6 On applications

In this section, we first mention some cases when one may deal with paraconsistent interpretations. After that we discuss concept learning in paraconsistent DLs.

Consider a domain with individuals described by unary and binary predicates. In the DL language, such predicates are concept names and role names, respectively. The domain can be described by different sources. For example, the individuals can be some objects in an area on the Earth and the information sources can be computer systems of different satellites, the objects are described by some Boolean attributes (standing for atomic concepts) and binary relationships between them (standing for atomic roles). Another example is as follows: some banks cooperate with each other in sharing information about their clients to some extent; the clients of banks are individuals; atomic concepts can be credibility, wealth and financial discipline; atomic roles can be some relationships based on transfers. The sources may provide assertions consistent or inconsistent with each other. Based on them, a paraconsistent interpretation can be created as an integrated information system.

Another situation of dealing with paraconsistent interpretations occurs when an inconsistent knowledge base is given. Such a knowledge base may result from combining or merging different knowledge bases, i.e., ontologies. Usually, matching or merging ontologies is done semi-automatically (by people using software tools). However, when the considered knowledge bases are dynamic, the automatic mode is unavoidable. In general, there are situations in which the considered knowledge base is inconsistent and one still wants to use it to derive only meaningful consequences. Having a knowledge base, sometimes we want to generate its models. For example, for concept learning in DL from a knowledge base KB given as a training information system, generated models of KB can be used to guide the search process [6, 20]. When KB is inconsistent w.r.t. the traditional semantics, it has only paraconsistent models.

Now, consider the concept learning problem set as follows. We are given a training information system $I$ with noisy and/or incomplete data, which is a (paraconsistent) $s$ -interpretation, together with two subsets E₊ and E_- of $Δ^{I}$ , which consist of positive examples and negative examples of an unknown concept C. We want to learn that concept C. We may be told that C is in a restricted language and the learnt concept is allowed to have some small error rate. Restricting the language is not a problem, and for simplicity, we assume no language restrictions. The non-exact learning assumption means that $(C_{+}^{I}, C_{-}^{I})$ need not to be the same as (E₊, E_-), but just approximate (E₊, E_-) closely.

We can compute the relation $Z = ≲_{Φ, s, I}^{\inf}$ (e.g., by the method stated in Remark 2). During that process, we maintain a concept C_x for each $x \in Δ^{I}$ so that $x \in (C_{x})_{+}^{I}$ and, for every $x^{'} \in Δ^{I}$ , 〈x, x′〉 ∈ Z iff $x^{'} \in (C_{x})_{+}^{I}$ . At the end of computing $≲_{Φ, s, I}^{\inf}$ , the relation $\sim_{Φ, s, I}$ (defined by (16)) is an equivalence relation with the following property: the equivalence class $[x]_{\sim_{Φ, s, I}}$ for any $x \in Δ^{I}$ is characterized by C_x in the sense that $x^{'} \in (C_{x})_{+}^{I}$ iff $x^{'} \in [x]_{\sim_{Φ, s, I}}$ . Among the concepts C_x′ with $x^{'} \in [x]_{\sim_{Φ, s, I}}$ we can choose any one to characterize $[x]_{\sim_{Φ, s, I}}$ (some measure can be used here). If $〈 E_{+}, E_{-} 〉 = C^{I}$ for some concept C, then each of E₊ and E_- is the union of some equivalence classes of $\sim_{Φ, s, I}$ . We can approximate C by a concept built from the concepts that characterize those equivalence classes. To do so we need the concepts (inconsistence) when $s_{C} \geq 3$ , and (unknown) when $s_{C} = 4$ , with the following denotation: ^Δ $= 〈 Δ^{I}, Δ^{I} 〉$ and ^Δ $= 〈 \emptyset, \emptyset 〉$ . Details are left for future work.

7 Conclusions

We have introduced the notions of bisimilarity and comparisons w.r.t. information for paraconsistent DLs. We have given preservation results and the Hennessy-Milner property for comparisons w.r.t. information in paraconsistent DLs. We have obtained also invariance results and the Hennessy-Milner property for bisimilarity in paraconsistent DLs. The Hennessy-Milner property shows that our notions of bisimilarity and comparisons w.r.t. information for paraconsistent DLs are proper. As future work, we intend to extend these notions for more expressive paraconsistent DLs and apply them to concept learning in paraconsistent DLs.

Acknowledgments

This work was supported in part by VNU Grant QG-15-22 and done in cooperation with the project 2011/02/A/HS1/00395, which is supported by the Polish National Science Centre (NCN).

References

Blackburn

, de Rijke

and Venema

, Modal Logic. Number 53 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2001.

Divroodi

A.R.

, Bisimulation Equivalence in Description Logics and Its Applications. PhD thesis, University of Warsaw, 2015.

Divroodi

A.R.

and Nguyen

L.A.

, Bisimulation-based comparisons for interpretations in description logics. In Proc of Description Logics’2013, volume 1014 of CEUR Workshop Proceedings, CEUR-WS.org, 2013, pp. 652–669.

Divroodi

A.R.

and Nguyen

L.A.

, Bisimulation-based comparisons for interpretations in description logics. CoRR, abs/1304.56022013.

Divroodi

A.R.

and Nguyen

L.A.

, On bisimulations for description logics, Information Sciences295 (2015), 465–493.

Q.-T.

, Hoang

T.-L.-G.

, Nguyen

L.A.

, Nguyen

H.S.

, Szałas

and Tran

T.-L.

, A bisimulation-based method of concept learning for knowledge bases in description logics. In Proc of SoICT’2012, ACM, 2012, pp. 241–249.

Kurtonina

and de Rijke

, Simulating without negation, J Log Comput7(4) (1997), 501–522.

Kurtonina

and de Rijke

, Expressiveness of concept expressions in first-order description logics, Artif Intell107(2) (1999), 303–333.

Lutz

, Piro

and Wolter

, Description logic TBoxes: Model-theoretic characterizations and rewritability. In Walsh

, editor, Proc of IJCAI’2011, 2011, pp. 983–988.

10.

and Hitzler

, Paraconsistent reasoning for OWL 2. In Polleres

and Swift

, editors, Proc of Web Reasoning and Rule Systems, volume 5837 of LNCS, Springer, 2009, pp. 197–211.

11.

, Hitzler

and Lin

, Paraconsistent reasoning for expressive and tractable description logics, In Proc of Description Logics, 2008.

12.

Meghini

and Straccia

, A relevance terminological logic for information retrieval. Proc of SIGIR’96, ACM, 1996, pp. 197–205.

13.

Nguyen

L.A.

, Paraconsistent and approximate semantics for the OWL 2Web Ontology Language, In Proc of RSCTC’2010, volume 6086 of LNAI, Springer, 2010, pp. 710–720.

14.

Nguyen

L.A.

, Nguyen

T.H.K.

, Nguyen

N.-T.

and Ha

Q.-T.

, Bisimilarity for paraconsistent description logics. A short version (6 pages) of the current paper, accepted for SMC’2016.

15.

Nguyen

L.A.

and Szałas

, Three-valued paraconsistent reasoning for Semantic Web agents. In Jędrzejowicz

et al., editor, Proc of KES-AMSTA 2010, Part I, volume 6070 of LNAI, Springer, 2010, pp. 152–162.

16.

Nguyen

L.A.

and Szałas

, Logic-based roughification. In Skowron

and Suraj

, editors, Rough Sets and Intelligent Systems (To the Memory of Professor Zdzisław Pawlak), Vol. 1, Springer, 2012, pp. 529–556.

17.

Nguyen

L.A.

and Szałas

, Paraconsistent reasoning for semantic web agents, T Computational Collective Intelligence6 (2012), 36–55.

18.

Odintsov

S.P.

and Wansing

, Inconsistency-tolerant description logic, part II: A tableau algorithm for CACL^c, Journal of Applied Logic6(3) (2008), 343–360.

19.

Straccia

, A sequent calculus for reasoning in fourvalued description logics. In Galmiche

, editor, Proc of TABLEAUX’97, volume 1227 of LNCS, Springer, 1997, pp. 343–357.

20.

Tran

T.-L.

, Ha

Q.-T.

, Hoang

T.-L.-G.

, Nguyen

L.A.

and Nguyen

H.S.

, Bisimulation-based concept learning in description logics, Fundam Inform133(2-3) (2014), 287–303.

21.

Tran

T.-L.

, Ha

Q.-T.

, Hoang

T.-L.-G.

, Nguyen

L.A.

, Nguyen

H.S.

and Szałas

, Concept learning for description logicbased information systems. In Proc of KSE’2012, IEEE Computer Society, 2012, pp. 65–73.

22.

Zhang

, Lin

and Wang

, Towards a paradoxical description logic for the semantic web. In Link

and Prade

, editors, Proc of FoIKS’2010, volume 5956 of LNCS, Springer, 2010, pp. 306–325.

23.

Zhang

, Qi

, Ma

and Lin

, Quasi-classical semantics for expressive description logics. In Proc of Description Logics2009.

Bisimilarity for paraconsistent description logics

Abstract

Keywords

1 Introduction

2 Preliminaries

2.1 Syntax of the description logics ALC Φ

2.2 Paraconsistent semantics for description logics

3 Comparison with respect to information and bisimilarity for paraconsistent DLs

5 The Hennessy-Milner property

6 On applications

7 Conclusions

Acknowledgments

References

2.1 Syntax of the description logics ${ALC}_{Φ}$