PUBLICATIONS DE L’INSTITUT MATHÉMATIQUE Nouvelle série, tome 82(96) (2007), 25–35 DOI 102298/PIM0796025M

DISJUNCTION IN MODAL DESCRIPTION LOGICS

Milenko Mosurović

Abstract. We investigate the complexity of satisfaction problems in modal description logics without disjunction between formulae. It is shown that simulation of disjunction in the class of all models of these logics is possible, so that the complexity remains same no matter the logics is with or without disjunction of formulae. However, the omission of disjunction, in the class of the models based on the universal relation, “turns down” the complexity of satisfaction problem i.e., if P ≠ NP, it is not possible to simulate disjunction.

1. Introduction

Description logics are invented for knowledge representation and reasoning in systems of artificial intelligence (see e.g. [6, 5, 1] and [8] for more references). An apparent general requirement to such logics is “to be sufficiently expressive and effective.” However, the concrete balance between their expressive power and complexity depends on the application domain the logic is designed for. There is a wide spectrum of description logics, from relatively weak ones, like ALER, the (un)satisfaction problem for concepts in which is NP-complete, more complex ALC which is PSPACE-complete (see [7]), to very expressive ones, like CIQ of De Giacomo and Lenzerini [10] and De Giacomo [9].

The conventional description logics were designed to represent knowledge about static application domains only. To capture various dynamic features, for instance, intensional knowledge (in multi-agent systems), dependence on time or actions (in distributed systems), description logics are combined with suitable “modal” (propositional) logics, say epistemic, temporal, or dynamic. Again, there is a variety of possible combinations (see e.g [15, 12, 2, 3]). Some of them are rather simple and do not increase substantially the complexity of the combined logic (for example, the temporal description logic of Schild [15] is EXPTIME-complete); others are too expressive and undecidable (e.g. the multi-dimensional description logic of Baader and Ohlbach [3]).

2000 Mathematics Subject Classification: Primary 03B70; Secondary 68T27, 68Q17.

Various kinds of balances between the expressive power and decidability have been found in the series of papers [16, 17, 18, 19], where expressive and yet decidable description logics with epistemic, temporal, and dynamic operators were constructed. However, the complexity of the satisfaction problem in almost all of these logics is NEXPTIME-hard [14](some of these logics are NEXPTIME-complete e.g.

[17] and some EXPSPACE-complete e.g. [18]).

The disjunction is usually source of non-determinism, and we recall that in modal description logics it can arise between concepts and between formulae. It is possible that the presence of disjunction of formulae cause such levels of complexity. The syntax of logics ALC_{M} of Baader and Laux does not have disjunction of formulae, so that we can expect the lower complexity for them.

In this paper we show that disjunction of ALC_{M}-formulae of Wolter and Zakharyaschev can be simulated in ALC_{M}-formulae of Baader and Laux in the class K and the satisfiability problem for ALC_{M}-formulae of Baader and Laux in the class K is NEXPTIME-hard. On the other hand, ALC_{M}-formulae of Baader and Laux in the class S5 is EXPTIME-complete (i.e. assuming P ≠ NP, the disjunction of ALC_{M}-formulae of Wolter and Zakharyaschev can not be simulated in ALC_{M}- formulae of Baader and Laux in the class S5).

2. Syntax and Semantics

We begin by defining the modal concept description language ALC_{M} and its semantics. The primitive symbols of ALC_{M} are:

concept names C_{0}, C_{1}, …, role names R_{0}, R_{1}, …, and object names a_{0}, a_{1}, . . .. Starting from primitive symbols, we can form compound concepts and formulae

using the following constructs. Suppose R is a role name and C, D are concepts (for the basis of our inductive definition we assume concept names to be atomic concepts). Then ⊤, C ∧ D, ¬C, ∃R.C, and ♢C are concepts.

Atomic formulae are expressions of the form ⊤, C = D, a : C, and aRb, where a, b are object names. If φ and ψ are formulae, then so are φ ∧ ψ, ¬φ, and ♢φ.

The corresponding modal description language is denoted by ALC_{M}.

Other standard logical connectives are defined in the usual way. For instance, C ∨ D is an abbreviation for ¬(¬C ∧ ¬D), ⊥ for ¬⊤,C → D for ¬(C ∧ ¬D), C ⊆ D for C ∧ D = C, and □ for ¬♢¬.

Note that, in the definition above, we did not impose any restriction on the form of conceptual assertional axioms. Baader and Laux [2] consider only atomic formulae prefixed by sequences of modal operators.

We recall to the syntax of ALC_{M^{B}} introduced by Baader and Laux [2].

Terminological axioms of ALC_{M^{B}} are of the form m(C = D) where C and D are concepts of ALC_{M} and m is a (possibly empty) sequence of modal operators. Assertional axioms of ALC_{M^{B}} are of the form m(aRb) or m(a : C) where a and b are object names, R is a role name, C is a concept, and m is a (possibly empty) sequence of modal operators (♢ and □). An ALC_{M^{B}}-formula is either a terminological or an assertional axiom.

A model of ALC_{M} based on a frame 𝔉 = ⟨W, ◁⟩ is a pair 𝔐 = ⟨𝔉, I⟩ in which I is a function associating with each w ∈ W a structure

I(w) = ⟨Δ^{I,w}, R_{0}^{I,w}, …, C_{0}^{I,w}, …, a_{0}^{I,w}, … ⟩,

where Δ^{I,w} is a nonempty set of objects, the domain of w, R_{i}^{I,w} are binary relations on Δ^{I,w}, C_{i}^{I,w} are subsets of Δ^{I,w}, and a_{i}^{I,w} are objects in Δ^{I,w} such that a_{i}^{I,w} = a_{i}^{I,v}, for any v, w ∈ W.

One can distinguish between three types of models: those with constant, expanding, and varying domains. In models with constant domains Δ^{I,v} = Δ^{I,w}, for all v, w ∈ W. In models with expanding domains Δ^{I,v} ⊆ Δ^{I,w} whenever v ◁ w. And models with varying domains are just arbitrary models.

Given a model 𝔐 and a world w in it, we define the value C^{I,w} of a concept C in w and the satisfaction relation (𝔐, w) ⊧ φ (or simply w ⊧ φ, if 𝔐 is understood) by taking:

⊤^{I,w} = Δ^{I,w} and
C^{I,w} = C_{i}^{I,w}, for C = C_{i};
(C ∧ D)^{I,w} = C^{I,w} ∩ D^{I,w};
(¬C)^{I,w} = Δ^{I,w} − C^{I,w};
x ∈ (♢C)^{I,w} iff ∃v ▷ w x ∈ C^{I,v};
x ∈ (∃R.C)^{I,w} iff ∃y ∈ C^{I,w} xR^{I,w}y;
w ⊧ C = D iff C^{I,w} = D^{I,w};
w ⊧ a : C iff a^{I,w} ∈ C^{I,w};
w ⊧ aRb iff a^{I,w}R^{I,w}b^{I,w};
w ⊧ ♢φ iff ∃v ▷ w v ⊧ φ;
w ⊧ φ ∧ ψ iff w ⊧ φ and w ⊧ ψ;
w ⊧ ¬φ iff w |̸= φ.

A formula φ is satisfiable in a class of models M if there is a model 𝔐 ∈ M and a world w in 𝔐 such that w ⊧ φ. Usually, we consider following classes of models:

K the class of all models; S5 the class of models based on frames with the universal relations, i.e., u◁v

for all u and v; KD45 the class of transitive, serial (∀u∃v u ◁ v) and Euclidean (u ◁ v ∧ u ◁ w →

v ◁ w) models; S4 the class of all quasi-ordered models; K4 the class of transitive models; GL the class of transitive Noetherian models (i.e., containing no infinite as-

cending chains); N the class of models based on ⟨ℕ, <⟩.

It is obvious that finite conjunction of ALC_{M^{B}}-formulae is a ALC_{M}-formula.

A set {F_{1}, …, F_{n}} of ALC_{M^{B}}-formulae is satisfiable in a class of models M if there is a model 𝔐 ∈ M and a world w in 𝔐 such that w ⊧ F_{i}, for i = 1, …, n.

3. Complexity in the class K

Lower bounds of the satisfaction problem for some modal description logics with constant domain assumption follows from [14] and [13]. For instance, the satisfaction problem for ALC_{M}-formulae free from role names in each of the classes K, S4, and K4 is NEXPTIME-hard.

Now we will establish the lower bound for the satisfaction problem in the class K with expanding domain assumption.

Theorem 3.1. Testing satisfiability of a finite set {F_{1}, …, F_{n}} of ALC_{M^{B}}- formulas in a class K with expanding domains is NEXPTIME-hard.

The key step in the proof of Theorem 3.1 lies in showing that disjunction of ALC_{M}-formulae can be simulated in ALC_{M^{B}} in class K.

Proposition 3.1. Let 𝔐 = (W, <, I) be a model of ALC_{M}, let w be a world in W, and let E, F are concept names. If 𝔐, w ⊧ (F = ♢E) ∧ □(E = ⊤), then 𝔐, w ⊧ (F = ⊤) ∨ (F = ⊥).

Proof. Let 𝔐, w ⊧ (F = ♢E) ∧ □(E = ⊤). If ∃v ∈ W w < v, then F^{I,w} = (♢E)^{I,w} = △^{I,w} (i.e., 𝔐, w ⊧ F = ⊤), else F^{I,w} = (♢E)^{I,w} = ∅ (i.e., 𝔐, w ⊧ F = ⊥). □

Proof. (Theorem 3.1) We will show here the lower bound for the testing satisfiability of a finite set of ALC_{M^{B}}-formulae in a class K with expanding domains by reducing to it the n × n tiling problem, n given in binary, which is known to be NEXPTIME-complete [4]. Namely, for a set T = {t_{1}, …, t_{s}} of tiles and n < ω, we construct a finite set of ALC_{M^{B}}-formulae F = {φ_{1}, …, φ_{m}} such that F is satisfied in an ALC_{M}-model from K iff T tiles 2^{n} × 2^{n}.

To encode the 2^{n} × 2^{n} grid, we define 2^{2n} concepts B_{ij}, 0 ⩽ i, j < 2^{n}, using 2n concept names C_{0}, …, C_{2n−1}, a role name R, and an object name a.

Let F_{1} be the set of the following formulae (that are similar to those of [11, p. 371] and [14]):

∃R.⊤ = ⊤, a : ¬C_{0} ∧ ⋯ ∧ ¬C_{2n−1},

⋀_{j=0}^{i−1} C_{j} → (C_{i} → ∀R.¬C_{i}) ∧ (¬C_{i} → ∀R.C_{i}) = ⊤, for i = 0, …, 2n − 1,

⋁_{j=0}^{i−1} ¬C_{j} → (C_{i} → ∀R.C_{i}) ∧ (¬C_{i} → ∀R.¬C_{i}) = ⊤, for i = 0, …, 2n − 1.

For any i, j ∈ {0, …, 2^{n}−1} written in binary as (d_{2n−1}, …, d_{n}) and (d_{n−1}, …, d_{0}), respectively, we put B_{ij} = C_{0}^{d_{0}} ∧ ⋯ ∧ C_{2n−1}^{d_{2n−1}}, where C^{d} is C if d = 1 and ¬C otherwise. If F_{1} is satisfied in a world w in an ALC-model, then the sets B_{ij} in this model are nonempty, pairwise disjoint and cover the domain △^{I,w} of the world w of the model.

For each tile t_{i} ∈ T we introduce a concept name T_{i}. Its intended meaning is as follows: we will say that t_{k} covers an element (i, j) in the grid iff B_{ij} ⊆ T_{k} (i.e., B_{ij} → T_{k} = ⊤). The problem now is to guarantee that every element of the grid is covered by precisely one tile and that the colours of adjacent tiles match without using too many formulae. To this end we require 2n new concept names Q_{0}, …, Q_{2n−1}; they will encode 2^{2n} worlds w_{ij}, 0 ⩽ i, j < 2^{n}.

Precisely we will describe a binary tree of depth 2n, using 2n concept names Q_{0}, …, Q_{2n−1}. This will provide us with 2^{2n} nodes (on the level 2n) each encoding a world w_{ij}, 0 ⩽ i, j < 2^{n}.

Let F_{2} be the set of the following formulae (that are similar to those of [11], p. 354 and [14]):

□^{i}♢(Q_{i} = ⊤), □^{i}♢(Q_{i} = ⊥), for i = 0, …, 2n − 1

□^{i}(Q_{j} = □Q_{j}), □^{i}(Q_{j} = ♢Q_{j}), for i = 1, …, 2n; j = 0, …, i − 1,

□^{2n}♢(Q_{i} = ♢A_{i}), □^{2n+2}(A_{i} = ⊤), for i = 0, …, 2n − 1 (see Proposition 3.1).

Let F_{3} be the set of formulae

C_{i} = □^{2n}C_{i}, C_{i} = ♢^{2n}C_{i}, for i = 0, …, 2n − 1,
T_{i} = □^{2n}T_{i}, T_{i} = ♢^{2n}T_{i}, for i = 1, …, s.

The meaning of the set F_{3} is that each C_{i} (T_{j}) contains the same objects of domain △^{I,w} (w is root of tree) in every world (on the level 2n) w_{ij} (i.e., C_{k}^{I,w} ⊆ C_{k}^{I,w_{ij}}).

Let B, B^{r}, B^{u} are three other concept names. B will coincide with B_{ij}, B^{r} with B_{i,j+1}, and B^{u} with B_{i+1,j} in the world w_{ij} determined by the condition w_{ij} ⊧ Q_{0}^{d_{0}} ∧ ⋯ ∧ Q_{2n−1}^{d_{2n−1}} = ⊤, where (d_{2n−1}, …, d_{n}) and (d_{n−1}, …, d_{0}) are binary representations of i and j, respectively. This will be ensured by the set of formulae F_{4}:

♢^{2n}B = ⊤, □^{2n}(B = ⋀_{i=0}^{2n−1}((C_{i} ∧ Q_{i}) ∨ (¬C_{i} ∧ ¬Q_{i}))).

□^{2n}(B^{r} = ⋁_{k=0}^{n−1}(¬Q_{k} ∧ ⋀_{j=0}^{k−1} Q_{j} ∧ ⋀_{i=0}^{k−1} ¬C_{i} ∧ C_{k} ∧ ⋀_{i=k+1}^{2n−1}((C_{i} ∧ Q_{i}) ∨ (¬C_{i} ∧ ¬Q_{i})))),

□^{2n}(B^{u} = ⋁_{k=n}^{2n−1}(¬Q_{k}∧ ⋀_{j=n}^{k−1} Q_{j}∧ ⋀_{i=n}^{k−1} ¬C_{i}∧C_{k}∧ ⋀_{i∉{n,...,k}}((C_{i}∧Q_{i})∨(¬C_{i}∧¬Q_{i})))).

Let F_{5} be the set of formulae

□^{2n}(F_{i} ∧ F_{j} = ⊥), for i ≠ j,
□^{2n}(F_{i} = ♢F_{i}), □^{2n}(F_{i} = □F_{i}), for i = 1, …, s,

□^{2n}♢(F_{i} = ♢E_{i}), □^{2n+2}(E_{i} = ⊤), for i = 1, …, s (see Proposition 3.1).

This means that ∃_{⩽1}i ∈ {1, …, s}F_{i} = ⊤ and F_{j} = ⊥ for all j ≠ i.

Let F_{6} be the set of formulae

□^{2n}( ⋁_{j=1}^{s} T_{j} = ⊤),

□^{2n}(B ∧ T_{i} = B ∧ F_{i}), for i = 1, …, s.

This means that ∃!i ∈ {1, …, s}B ⊆ T_{i} and B ∧ T_{j} = ⊥ for all j ≠ i.

Now we are in a position to write down the set F_{7} of formulae which says that the colors of adjacent tiles match:

□^{2n}(B^{r} ⊆ ( ⋀_{i=0}^{n−1} Q_{i}) ∨ (⋁_{i=1}^{s} ⋁_{right(i)=left(j)} F_{i} ∧ T_{j})),

□^{2n}(B^{u} ⊆ ( ⋀_{i=n}^{2n−1} Q_{i}) ∨ (⋁_{i=1}^{s} ⋁_{up(i)=down(j)} F_{i} ∧ T_{j})).

We remark that if B ⊆ T_{k} than F_{k} = ⊤ and F_{i} = ⊥ for all i ≠ k, so we have

B^{u} ⊆ (⋁_{i=1}^{s} ⋁_{up(i)=down(j)} F_{i} ∧ T_{j}) ≡ ⋁_{i=1}^{s}(F_{i} ∧ ( ⋁_{up(i)=down(j)} T_{j})) ≡

F_{k} ∧ ( ⋁_{up(k)=down(j)} T_{j}) ≡ ⋁_{up(k)=down(j)} T_{j}.

One can show that F = F_{1} ⋃ ⋯ ⋃ F_{7} is as required. □

Corollary 3.1. The satisfaction problem for ALC_{M}-formulae in the class K,with the expanding domain assumption, is NEXPTIME-hard.

Corollary 3.2. Testing satisfiability of a finite set {F_{1}, …, F_{n}} of ALC_{M^{B}}- formulas in a class K with expanding domains is NEXPTIME-complete.

Proof. The upper bound follows from [2] and the lower from Theorem 3.1. □

Also, from the Theorem 3.1 follows that the satisfaction problem for ALC_{M}- formulae in each of the classes K, N, GL, S4, and K4, with the expanding domain assumption, is NEXPTIME-hard.

Theorem 3.2. The satisfaction problem for ALC_{M}- and ALC_{M^{B}}-formulae in the class K is NEXPTIME-complete (no matter whether the models have constant or expanding domains).

Proof. The upper bound follows from [2] and [17] and the lower bound from the Theorem 3.1 (Corollary 3.1). □

4. Complexity in the class S5

In the proof of the Theorem 3.1 we have used only one assertional axiom of the form (a : C). The usage of (a : C) enabled us to claim that at least one of the concepts is not empty. All other formulae were terminological axioms.

Now we will consider satisfaction problem for ALC_{M^{B}}-formulae in the class S5, supposing that we have at most one assertional axiom of the form (a : C) (let us call them ALC_{M^{B^{−}}} -formulae).

Using rules □(C_{1} = ⊤) ∧ □(C_{2} = ⊤) ≡ □(C_{1} ∧ C_{2} = ⊤), □□φ ≡ □φ, ♢□φ ≡ □φ, □♢φ ≡ ♢φ and ♢♢φ ≡ ♢φ, every set of formulae can be transformed into the equivalent set of formulae of the following form:

□(C_{0} = ⊤), (C_{1} = ⊤), (a : C1^{′}), ♢(C_{2} = ⊤), …, ♢(C_{s} = ⊤).

Now we define s-quasimodel (simple quasimodel) for finite sets of formulae. We fix a finite set F of ALC_{M^{B}}-formulas in the class S5 such that

F = {□(C_{0} = ⊤), (C_{1} = ⊤), (a : C1^{′}), ♢(C_{2} = ⊤), …, ♢(C_{s} = ⊤)}

i.e., ALC_{M} formula

φ_{F} = □(C_{0} = ⊤) ∧ (C_{1} = ⊤) ∧ (a : C1^{′}) ∧ ♢(C_{2} = ⊤) ∧ ⋯ ∧ ♢(C_{s} = ⊤).

With con φ_{F} we denote the closure under negation of the set of all concepts in φ_{F}. Without loss of generality we may identify C and ¬¬C, for every concept C; so the set con φ_{F} is finite and | con φ_{F} | < 2∥φ_{F} ∥, where ∥φ_{F} ∥ is the number of symbols in the formula φ_{F}. We also suppose that ♢D_{1}, ♢D_{2},…, ♢D_{m} are all concepts from con φ_{F} of the form ♢C.

Definition 4.1. A concept type t for φ_{F} is a subset of con φ_{F} such that 1) C ∧ D ∈ t iff C, D ∈ t, for every C ∧ D ∈ con φ_{F},

2) ¬C ∈ t iff C ∉ t, for every C ∈ con φ_{F}.

Let 𝔗_{F} be a set of all concept types for φ_{F}. For t ∈ 𝔗_{F} we will denote t_{|R} = {C ∈ con φ_{F} | ∀R.C ∈ t} and t_{|♢} = {D ∈ con φ_{F} | ♢D ∈ t}.

Definition 4.2. A set of s-quasiworld for φ_{F} is a set T = {T_{0}, T_{1}, …, T_{s}} such that

3) T_{i} ⊂ 𝔗_{F} , for every i ∈ {0, 1, ⋯, s},

4) T_{i} ≠ ∅ , for every i ∈ {0, 1, ⋯, s},

5) (∀t ∈ T_{i})C_{i} ∈ t , for every i ∈ {0, 1, ⋯, s},

6) (∀t ∈ T_{i})(∀(∃R.C) ∈ con φ_{F})(∃R.C ∈ t iff (∃t′ ∈ T_{i})t_{|R} ⊂ t′ ∧ C ∈ t′), for every i ∈ {0, 1, ⋯, s},

7) (∃t = t_{a} ∈ T_{1})C1^{′} ∈ t, for (a : C1^{′}) ∈ F,

Definition 4.3. A run in T = {T_{0}, T_{1}, …, T_{s}} is a function r : {−m, …, −1, 0, 1, …, s} → ⋃_{i=1}^{s} T_{i} such that

8) r(i) ∈ T_{i}, for every i ∈ {0, 1, …, s} and r(−k) ∈ T_{0}, for every k ∈

{1, …, m},
9) r(i)_{|♢} = r(j)_{|♢}, for every i, j ∈ {−m, …, 1, 0, 1, …, s}

10) For every k ∈ {1, ⋯, m}, if D_{k} ∈ r(0)_{|♢}, then D_{k} ∈ r(−k).

Definition 4.4. Let T = {T_{0}, …, T_{s}} be a set of s-quasiworld for φ_{F} and ρ set of run in it. The pair (T, ρ) is called a s-quasimodel for φ_{F} if the following holds:

11) (∀T_{i} ∈ T)(∀t ∈ T_{i})(∃r ∈ ρ)r(i) = t.

Lemma 4.1. If the set of formulae F is satisfiable, then there exists s-quasimodel for φ_{F}.

Proof. If the set of formulae F is satisfiable, then there exists at least one model for F. Let us consider arbitrary non-empty family of models MC = {𝔐_{c} = (W_{c}, W_{c} × W_{c}, I_{c}) | 𝔐_{c} ⊧ F and c ∈ C}, where C = |MC| ⩾ 1. We will construct s-quasimodel for φ_{F} which corresponds to the family MC.

For every model 𝔐_{c} = (W_{c}, W_{c} × W_{c}, I_{c}) ∈ MC, for every world w ∈ W_{c} and for every object x ∈ Δ^{I_{c},w}, let us define the concept type t^{I_{c},w}(x) = {C ∈ con φ_{F} | x ∈ C^{I_{c},w}}.

Let T_{i} = ⋃_{c∈C}{t^{I_{c},w}(x) | w ∈ W_{c}, w ⊧ (C_{i} = ⊤), x ∈ Δ^{I_{c},w}}. For arbitrary t ∈ T_{i}, i = 0, …, s, let us construct the run r = r_{t} such that r(i) = t. It follows that, for every t ∈ T_{i}, there exists a model 𝔐 = (W, W × W, I) ∈ MC and there exists a world w ∈ W and there exists an objects x ∈ Δ^{I,w}, such that w ⊧ (C_{i} = ⊤) ∧ t = t^{I,w}(x). Since 𝔐 ⊧ F, it follows that (∀j ∈ {0, …, s})(∃w_{j} ∈ W)w_{j} ⊧ (C_{j} = ⊤). Let t_{j} = t^{I,w_{j}}(x). Obviously t_{j} ∈ T_{j}. If ♢D_{k} ∉ t, put t_{−k} = t_{0}. Now suppose that ♢D_{k} ∈ t. Since ♢D_{k} ∈ t iff ♢D_{k} ∈ t^{I,w}(x) iff x ∈ (♢D_{k})^{I,w} iff (∃v_{k} ∈ W)x ∈ (D_{k})^{I,v_{k}}, we can define t_{−k} = t^{I,v_{k}}(x). Since v_{k} ⊧ (C_{0} = ⊤), it follows that t_{−k} ∈ T_{0}. Now, we put r(j) = t_{j} for every j ∈ {−m, …, s}. Let ρ be the set of all runs constructed in that way. Then, by construction, the tuple ({T_{0}, T_{1}, …, T_{s}}, ρ) is a s-quasimodel for φ_{F}. □

Lemma 4.2. If there exists a s-quasimodel for φ_{F}, then the set of formulae F is satisfiable.

Proof. Let Q = ({T_{0}, T_{1}, …, T_{s}}, ρ) be a s-quasimodel for φ_{F}. Based on Q, we will construct the model for F as follows. Let ρ′ = {r′ = r′(r, k) | r ∈ ρ, k ∈ {0, …, m} }, where

r′(r, 0) = r,

r′(r, k)(i) = r′(i) = r(i) for k ≠ 0 and i ∉ {0, −k},
r′(r, k)(0) = r′(0) = r(−k) for k ≠ 0 and i = 0,
r′(r, k)(−k) = r′(−k) = r(0) for k ≠ 0 and i = −k.

From the set of all runs ρ′ that goes through t_{a} we extract one run which we denote by r_{a}. Now we construct the model for the set F. Let

V = {v_{−m}, …, v_{−1}, v_{0}, v_{1}, …, v_{s}} be the set of worlds,

let ◁ = V × V be the relation,

let I(v_{j}) = ⟨Δ^{I,v_{j}}, R_{0}^{I,v_{j}}, …, A_{0}^{I,v_{j}}, …, a^{I,v_{j}}⟩ be the interpretation, where

Δ^{I,w} = Δ^{I} = {r | r ∈ ρ′}, A^{I,v_{j}} = {r ∈ Δ^{I} | A ∈ r(j)} (for atomic concepts A), R^{I,v_{j}} = {(r′, r′′) ∈ (Δ^{I})^{2} | r′(j)_{|R} ⊆ r′′(j)} and a^{I,v_{j}} = r_{a}, so that the model for the set F is 𝔐 = (V, ◁, I).

It still remains to prove, by the induction on concept complexity, that C ∈ r(i) iff r ∈ C^{I,v_{i}}. The most important cases are C ≡ ♢D_{k} and C ≡ (∃R.D):

In the first case we have: ♢D_{k} ∈ r(i) iff D_{k} ∈ r(−k) (if i = −k take simetrically r′(i)) iff r ∈ D_{k}^{I,v_{−k}} iff (∃v_{−k})(v_{i} ◁ v_{−k})(r ∈ D_{k}^{I,v_{−k}}) iff r ∈ (♢D_{k})^{I,v_{i}}

In the second case we have: (∃R.D) ∈ r(i) iff (∃t′ ∈ T_{i})r(i)_{|R} ⊆ t′ ∧ D ∈ t′ (notice that (∃r′ ∈ ρ)r′(i) = t′) iff (∃r′(i) ∈ T_{i})r(i)_{|R} ⊆ r′(i) ∧ D ∈ r′(i) iff (∃r′ ∈ Δ^{I})(r, r′) ∈ R^{I,v_{i}} ∧ r′ ∈ D^{I,v_{i}} iff r ∈ (∃R.D)^{I,v_{i}}

Finally we notice that, for arbitrary i ∈ {0, …, s}, we have (∀t ∈ T_{i})C_{i} ∈ t iff (∀r ∈ ρ′)C_{i} ∈ r(i) ∈ T_{i} iff r ∈ C_{i}^{I,v_{i}} iff C_{i}^{I,v_{i}} = Δ^{I} iff v_{i} ⊧ (C_{i} = ⊤). It is now obvious that in the model 𝔐 we have v_{1} ⊧ F. □

We now give the algorithm of satisfiability: Starting from the set F, construct the sets con φ_{F} and 𝔗_{F}. Let T_{0} = {t ∈ 𝔗_{F} | C_{0} ∈ t} and T_{i} = {t ∈ T_{0} | C_{i} ∈ t}, i = 1, …, s.

Repeat steps (a)-(c) as many times as it is possible:

(a) If there exists T_{i} = ∅ or C′_{1} ∉ t for all t ∈ T_{1}, then the algorithm returns the answer “NO”.

(b) If there exists t ∈ T_{i}, for which condition 6) of the definition 4.2 fails, then exclude t from T_{i}.

(c) If t ∈ T_{i} is such that we can not construct a run through it, then exclude t from T_{i}.

If none of the rules (a)-(c) can be applied, then the algorithm returns the answer “YES”.

Lemma 4.3. If the algorithm for the set F returns “YES”, then there exists a s-quasimodel for φ_{F} i.e. the set of formulae F is satisfiable.

Proof. The algorithm constructs set T = {T_{0}, T_{1}, …, T_{s}}. The conditions 3) and 5) of definition 4.2 are fulfilled by construction. Since the rule (a) of the algorithm was not applied, the conditions 4) and 7) of definition 4.2 are met, and since we can not apply the rule (b) of the algorithm, it follows that condition 6) of definition 4.2 is fulfilled. Hence, T is set of s-quasiworld.

For each t ∈ T_{i}, there exists a run r = r_{t} which goes through it, since otherwise, we would be able to apply rule (c) of algorithm. If ρ is the set of all runs, the pair (T, ρ) is s-quasimodel for φ_{F}. □

Lemma 4.4. If the algorithm for the set F returns “NO”, then s-quasimodel for φ_{F} does not exist, so the set of formulae F is not satisfiable.

Proof. Assume the opposite, let (T′, ρ′) be s-quasimodel for φ_{F}, where T′ = {T′_{0}, T′_{1}, …, T′_{s}}. In the very beginning, the algorithm constructs sets T_{0}, T_{1}, …, T_{s} such that T′_{i} ⊆ T_{i}. Applying the rules (b) and (c) of the algorithm, we can not exclude elements from T_{i} which belong to T′_{i}, so that rule (a) can never be applied.

□

Corollary 4.1. The algorithm is correct.

Lemma 4.5. The algorithm stops in at most exponential number of steps, according to the size of the input.

Proof. Since |𝔗_{F} | ⩽ 2^{| con φ_{F} |} and T_{i} ⊂ T, for i = 0, 1, …, s, it is clear that the construction of 𝔗_{F} and T_{i} requires EXPTIME. Hence, we have at most exponential number of concept types to which rules (a)-(c) can be applied. Also, after each step, there is one type less, so that the rules (b) and (c) of the algorithm can be applied at most exponential number of times. To check whether we can apply some rule, we need at most exponential time. Hence, the algorithm will return the answer after at most exponential number of steps. □

Note that the satisfaction problem for ALC_{M}-formulae without modal operators is EXPTIME-hard (see e.g [13]), so that we have the following theorem.

Theorem 4.1. The satisfaction problem for ALC_{M^{B^{−}}} -formulae in the class S5 is EXPTIME-complete

Lemma 4.6. The satisfaction problem for ALC_{M}-formulae in the class S5 is NEXPTIME-complete

Proof. See [14] and [13]. □

If the simulation of disjunction between formulae in description logics with modal operators based on the class S5 had been possible, then the complexity of satisfaction problems in ALC_{M} and ALC_{M^{B^{−}}} -formulae would have been the same. These means that, assuming P ≠ NP (i.e. EXPTIME ≠ NEXPTIME), the Theorem 4.1 and the Lemma 4.6 tells us that the simulation of disjunction is not possible in ALC_{M^{B^{−}}}.

References

[1] F. Baader and B. Hollunder, A terminological knowledge representation system with complete inference algorithms, in: Proceedings of the workshop on Processing Declarative Knowledge, PDK-91, Springer Verlag, 1991, 67–86.

[2] F. Baader and A. Laux, Terminological logics with modal operators, in: Proceedings of the 14th International Joint Conference on Artificial Intelligence, Morgan Kaufman, Montreal, Canada, 1995, 808–814.

[3] F. Baader and H. Ohlbach, A multi-dimensional terminological knowledge representation language, in: Proceedings of the 13th International Joint Conference on Artificial Intelligence, 1993, 690–695.

[4] van Emde Boas, The convenience of tilings, Tehnical Report CT-96-01, Institute for Logic, Language and Computation, University of Amsterdam.

[5] A. Borgida, R. J. Brachman, D. L. McGuiness, and L. A. Resnick, CLASSIC: A structural data model for objects, in: Proceedings of the ACM SIGMOD International Conference on Management of Data, Portland, Oreg., 1989, 59–67.

[6] R. J. Brachman and J. G. Schmolze, An overview of the KL-ONE knowledge representation system, Cognitive Science 9 (1985), 171–216.

[7] F. Donini, M. Lenzerini, D. Nardi, and W. Nutt, The complexity of concept languages, Technical Report RR-95-07, Deutsches Forchungszentrum für Künstliche Intelligenz (DFKI), 1995.

[8] F. Donini, M. Lenzerini, D. Nardi, and A. Schaerf, Reasoning in description logics, in: G. Brewka, Principles of Knowledge Representation, CSLI Publications, 1996, 191–236.

[9] G. De Giacomo, Decidability of Class-Based Knowledge Representation Formalisms, PhD thesis, Univ. di Roma, 1995.

[10] G. De Giacomo and M. Lenzerini, TBox and ABox reasoning in expressive description logics, in: Proceedings of the fifth Conference on Principles of Knowledge Representation and Reasoning,Morgan Kaufman, Montreal, Canada, 1996.

[11] J. Halpern and Yo. Moses. A guide to completeness and complexity for modal logics of knowledge and belief, Artificial Intelligence 54 (1992),319–379.

[12] A. Laux. Beliefs in multi-agent worlds: a terminological approach, in: Proceedings of the 11th European Conference on Artificial Intelligence, Amsterdam, 1994, 299–303.

[13] M. Mosurović. Složenost opisnih logika s modalnim operatorima, Doktorska disertacija, Univerzitet u Beogradu, 2000.

[14] M. Mosurović and M. Zakharyaschev, On the complexity of description logics with modal operators, in: P. Kolaitos and G. Koletos, Proceedings of the 2nd Panhellenic Logic Symposium, Delphi, 1999, 166–171.

[15] K. Schild, Combining terminological logics with tense logic, in: Proceedings of the 6th Portuguese Conference on Artificial Intelligence, Porto, 1993, 105–120.

[16] F. Wolter and M. Zakharyaschev, Dynamic description logic, Advances in Modal Logic. Volume II, CSLI Publications, Stanford, 1999.

[17] F. Wolter and M. Zakharyaschev, Satisfiability problem in description logics with modal operators, in: Proceedings of the sixth Conference on Principles of Knowledge Representation and Reasoning, Morgan Kaufman, Montreal, Canada, 1998, 512–523.

[18] F. Wolter and M. Zakharyaschev, Temporalizing description logics, Frontiers of Combining Systems, Kluwer Academic Publishers, 1999.

[19] F. Wolter and M. Zakharyaschev, Multi-dimensional description logics, in: Proceedings of IJCAI’99, Stockholm, 1999.

Prirodno-matematički fakultet 81000 Podgorica Montenegro

milenko@cg.ac.yu