MAX-PLANCK-INSTITUT FÜR

INFORMATIK

A Multi-Dimensional Terminological Knowledge Representation Language

Franz Baader Hans Jürgen Ohlbach

MPI–I–95–2–005 January 1995

[figure: I N F O R M A T I K]

Im Stadtwald D 66123 Saarbrücken

Germany Authors’ Addresses

Franz Baader LuFG Theoretische Informatik RWTH Aachen Ahornstraße 55 D-52074 Aachen F. R. Germany email: baader@informatik.rwth-aachen.de

Hans Jürgen Ohlbach Max–Planck–Institut für Informatik Im Stadtwald D-66123 Saarbrücken F. R. Germany email: ohlbach@mpi-sb.mpg.de

Publication Notes

This paper will be forthcoming in the Journal of Applied Non-Classical Logics. A preliminary version had been published in the Proceedings of IJACI-93 and as MPI report MPI-I-93-212.

Acknowledgements

This work was supported by the ESPRIT Project 6471 MEDLAR and by the the BMFT Projects Logo (ITS 9102) and TACOS (ITW 9201).

Abstract

An extension of the concept description language ALC used in kl-one-like terminological reasoning is presented. The extension includes multi–modal operators that can either stand for the usual role quantifications or for modalities such as belief, time etc. The modal operators can be used at all levels of the concept terms, and they can be used to modify both concepts and roles. This is an instance of a new kind of combination of modal logics where the modal operators of one logic may operate directly on the operators of the other logic. Different versions of this logic are investigated and various results about decidability and undecidability are presented. The main problem, however, decidability of the basic version of the logic, remains open.

Contents

1 Syntax and Semantics of M-ALC 3

1.1 An Alternative Presentation of the Semantics . . . . . . . . . . . . . . . . . . . . . 6 2 Relation to Known Systems 6

2.1 n-Dimensional M-ALC with Atomic Role Terms . . . . . . . . . . . . . . . . . . . 7 2.2 M-ALC with Compound Role Terms . . . . . . . . . . . . . . . . . . . . . . . . . . 8

3 The Satisfiability Test 15 4 Proof of Termination and Soundness 17 5 Independence of Some Dimensions 26 6 Summary and Open Problems 30

Introduction

Knowledge representation languages in the style of kl-one [3], so-called terminological KR languages, can be used to define the relevant concepts of a problem domain and the interaction between these concepts. To this purpose, complex concepts are constructed out of atomic concepts (i.e., unary predicates) and roles (i.e., binary predicates) with the help of the language constructs provided by the particular terminological language. Various such languages have been considered in the literature and are used in KR systems (see, e.g., [14, 16, 15, 19, 7, 1, 4, 23]).

They have in common that they are only suitable for representing objective, time-independent facts about the world. Notions like belief, intentions, time—which are essential for systems that model aspects of intelligent agents—can only be represented in a very limited way. Suppose that a terminological system should represent that the agent John believes that new cars have catalytic converters whereas Tom believes that they don’t. One possibility—which has, e.g., been used in sb-one [12]—is that the system keeps two separate terminologies, one for John’s belief context and one for Tom’s belief context:

John’s T-Box: new-car = car ⊓ ∃has-part: catalytic-converter

Tom’s T-Box: new-car = car ⊓ ¬∃has-part: catalytic-converter

This does not work, however, when interactions between different beliefs, e.g., in the sense of a (modal) theory of belief are needed in the application. Modal operators of the form [belief-...]^{1} that satisfy appropriate modal axioms allow for more natural definitions:

[belief-John](new-car = car ⊓ ∃has-part: catalytic-converter),
[belief-Tom](new-car = car ⊓ ¬∃has-part: catalytic-converter).

Things become more complex if the application requires the use of modalities inside of concept expressions as well. Assume that we want to express that a potential customer (for a car salesman) is an adult who eventually wants to own a car. In a traditional terminological language a definition of this concept could be

potential-customer = adult ⊓ ∃eventually-wants-own: car,

where eventually-wants-own is a new role different to the roles own and wants-own. But then there would be no interaction between these roles, whereas one would expect that wants-own implies eventually-wants-own. Again, modal operators with an appropriate modal theory of time and belief can be used to capture such interactions. In our example, we obtain the definition

potential-customer = adult ⊓ ∃(⟨future⟩[want]own): car.

Intuitively, the role-fillers for own now also depend on the point in time and on the intentional world, and not only on the object. The prefix [want] means that one takes only those objects that are role-fillers in all accessible intentional worlds, and the prefix ⟨future⟩ says that this has to be evaluated at some future time point.

In this example, the modal operators modify the own-role. Of course, there are also cases where one would like to modify concepts in this way. In the definition

environment-freak = person ⊓ ∀([want]own):[belief]environment-friendly,

an environment freak is defined as a person that wants to own only things that are believed to be environment friendly. In this case the [belief]-operator modifies the concept environment-friendly.

1The standard modal operators are usually written □ and ◇. In a multi–modal logic with different modal operators referring to different accessibility relations we write [p] and ⟨p⟩ for the parameterized box and diamond operators. These operators can be interpreted as ‘believes’, ‘knows’, ‘wants’, ‘always’ (in the future or past) and the like.

We have motivated by examples that it is desirable to extend terminological languages by various types of modal operators (for time, belief, want, etc.), which should be applicable to definitions as well as inside of concept terms, and there to modify both concepts and roles. Our approach to achieve this goal is based on an observation by Schild [19] that the terminological language ALC is just a syntactic variant of the multi–modal logic K_{m} [5], where m is the number of different box operators. The reason is that quantifications over roles can just be seen as applications of parameterized modal operators to concepts. Thus we propose to treat roles and modalities in a symmetric way by using a multi–modal logic where both role names and modalities such as belief can be used as parameters in boxes and diamonds. To distinguish between roles, which operate on objects, and modalities operating, e.g., on time points or intentional worlds, we shall equip each modal operator with a type (or dimension) such as ‘object’, ‘time-point’ etc. Although in this paper we prefer the notions ‘role’, and ‘concept’, modal logicians should always understand ‘role name’ as ‘parameter of a parameterized modal operator’, ‘role’ as ‘accessibility relation’, ‘role fillers’ as ‘set of accessible worlds’ and ‘concept’ as ‘propositional variable’.

The requirement that it should be possible to modify roles by modal operators is, however, not yet captured by this approach. Until now, the parameterized modal operators are atomic in the sense that the boxes and diamonds may only contain parameter names like own, future, or belief. Applying modal operators to roles means that one obtains complex terms inside boxes and diamonds. For example, in the definition of environment-freak we thus get the modal prefix [[want]own] where the complex (role) term [want]own occurs inside a box-operator.

Our new approach for integrating modalities into terminological KR languages, called M-ALC in the following, thus extends the prototypical terminological language ALC in two respects. First, ‘roles’ may have different types that express in what dimension (e.g., object-dimension, time-point-dimension) they operate. In addition, one can apply role quantification not only to concepts but also to roles, which provides for a very expressive language for building role terms. The expressive power of this language is, for example, demonstrated by the fact that general concept equations (see, e.g., [19]) can be expressed, even if one has only one dimension. This shows that the important inference problems (such as satisfiability of concept terms) must be of very high complexity for our language.^{2} For this reason we shall impose additional restrictions on the syntactic form of certain role terms to get a practical algorithm for satisfiability of concept terms (Section 3). If one further restricts M-ALC to the case where all role terms are atomic, then M-ALC becomes equivalent to ALC in the sense that the same concept terms are satisfiable (see Section 2.1).

The expressive power of M-ALC can further be extended by having roles and concepts depend on only some of the dimensions. For example, it seems reasonable to assume that the role future of dimension ‘time-point’ does not depend on the object-dimension. In Section 5 we shall show, however, that this additional feature makes satisfiability in M-ALC an undecidable property.

1 Syntax and Semantics of M-ALC

As for ALC, the elementary syntax elements in M-ALC are concept and role names. However, with each role name we associate a type that expresses in what dimension (e.g., object-dimension, timepoint-dimension) this role operates. To simplify things, we assume there are n different dimensions, and we count them from 1 to n. Each dimension corresponds to a particular set (domain, universe). For example, the object dimension corresponds to the set of all objects (as used in ALC), the time dimension corresponds to the set of all time points, and the belief dimension corresponds to the set of all belief worlds. In the present paper, however, we do not yet consider structures on these sets; for example, time points are not assumed to be linearly ordered, and the belief worlds are not assumed to satisfy certain belief axioms. This means that the underlying logic is simply the basic modal logic K.

The syntactic form of a modal operator in M-ALC is [p] (box) or ⟨p⟩ (diamond) where p may be an atomic role name or a compound role term. In addition to the usual box-operator of modal logic we shall consider a modified box-operator [...]^{+} that combines the the box- and diamond-operator. In many cases, [...]^{+} makes more sense than the usual box-operator [...]. For example, a sentence ‘All her friends are wealthy’ is usually understood in the sense that the person in question really has friends. Thus it is better modelled by the expression [has-friend]^{+}wealthy than by [has-friend]wealthy.

2Satisfiability modulo concept equations is known to be exp-time complete; this is an easy consequence of a result by Fischer and Ladner [8].

Definition 1.1 The signature Σ of an M-ALC language L_{n} of dimension n > 0 consists of a set Σ_{P} of role names and a disjoint set Σ_{C} of concept names. The concept names include the distinguished symbols ⊤ (for ‘truth’) and ⊥ (for ‘falsity’). Each role name p has a dimension dim(p), which is a positive integer ≤ n.

The sets of role terms and modal operators is defined to be the least set such that

• Each role name p is a role term (of dimension dim(p)). In addition, [p], [p]^{+} and ⟨p⟩ are modal operators of dimension dim(p).

• If p is a role name of dimension i and m is a sequence of modal operators then m p is a role term of dimension i, and [m p], [m p]^{+} as well as ⟨m p⟩ are modal operators of dimension i.

The notation [...]^{∗} will be used for the [...]^{+}-operator as well as for the normal [...]-operator. The set of concept terms is defined to be the least set such that

• Each concept name c is a concept term.

• If c and d are concept terms then ¬c, c ∨ d and c ∧ d are concept terms.

• If p is a role term (of arbitrary dimension) and c is a concept term then [p]c, [p]^{+}c and ⟨p⟩c are concept terms.

A concept equation is a formula m (c = d) where c is a concept name, d a concept term, and m a modal prefix, i.e., a (possibly empty) sequence of box and diamond operators. A T-Box is a set of concept equations.

A concept term is called restricted serial if role terms do not contain normal [...]-operators. <

Even for a single dimension, M-ALC is an extension of ALC since one can build complex role terms. This allows one to express interactions between roles that cannot be captured in ALC. For example, the concept of a ‘woman all of whose children have a common favourite meal’ is expressible by ‘woman ∧ ⟨[has-child]likes⟩meal’.

The semantics of M-ALC is similar to the Kripke style possible worlds semantics for manydimensional modal logic [22]. For each dimension i we introduce a non-empty set D_{i}. The elements of D_{1} × … × D_{n} correspond to worlds in the modal logic sense. As in modal logic, there is always an ‘actual world tuple’ d⃗ = (d_{1}, …, d_{n}) that determines the interpretation of the syntax elements.

Since the domain consists of n-tuples, concept terms correspond to n-ary predicates. If, for example, there are the two dimensions object and time then the extension of the concept term car is a set of tuples (o, t). Another way of looking at this is that car corresponds to a subset of objects, but depending on the time point, i.e., the set of things that are cars changes over the time. Conversely one may also see car as a set of time points, and this set depends on the objects. This yields the time points (lifespan) for which each object is considered as a car.

Accordingly, roles in M-ALC correspond to n+1-ary predicates. For example, the role own of dimension object is not simply a binary relation between objects. For a given object o, the set of role-fillers for this object will depend not only on o but also, say, on the actual belief world and time point.

In the definition of the semantics of M-ALC we shall use the following notational conventions. For a fixed number of dimensions n, the Cartesian product of the sets D_{1}, …, D_{n} is denoted by D⃗. An element (d_{1}, …, d_{n}) of D⃗ is denoted by d⃗, and (d_{1}, …, d_{i−1},x,d_{i+1}, …, d_{n}) by d⃗[i/x].

Definition 1.2 An interpretation ℑ = (D⃗, ℑ_{Σ}) for an n-dimensional M-ALC language L_{n} consists of the Cartesian product D⃗ = D_{1} × … × D_{n} of n non-empty carrier sets (domains), and a signature interpretation ℑ_{Σ}.

The signature interpretation assigns successor functions to role names and n-place relations to concept names. To be more precise, a role name p of dimension i is interpreted as a function ℑ_{Σ}(p) : D⃗ → 2^{D_{i}}, and a concept name c as a set ℑ_{Σ}(c) ⊆ D⃗. The concept name ⊤ is interpreted as D⃗ and ⊥ as the empty set.

The interpretation of a role term q of dimension i is also a function ℑ(q) : D⃗ → 2^{D_{i}} that is inductively defined as follows. Let r be a role name, p, q be role terms, and let j be the dimension of q.

\begin{aligned}ℑ(r)(d⃗) & = & ℑ_{Σ}(r)(d⃗), \\ ℑ([p]q)(d⃗) & = & ⋂_{x∈ℑ(p)(d⃗)} ℑ(q)(d⃗[j/x]), \\ ℑ(⟨p⟩q)(d⃗) & = & ⋃_{x∈ℑ(p)(d⃗)} ℑ(q)(d⃗[j/x]), \\ ℑ([p]^{+}q)(d⃗) & = & ℑ([p]q)(d⃗) ∩ ℑ(⟨p⟩q)(d⃗). \end{aligned}

A satisfiability relation ⊧ between an interpretation ℑ with actual point d⃗ and concept terms and concept equations is defined as follows. Let c be a concept name, e, f be concept terms, p be a role term of dimension i, and ϕ be a concept term or concept equation.

ℑ, d⃗ ⊧ c  iff d⃗ ∈ ℑ_{Σ}(c),
ℑ, d⃗ ⊧ c = e iff (ℑ, d⃗ ⊧ c iff ℑ, d⃗ ⊧ e),
ℑ, d⃗ ⊧ ¬e iff not ℑ, d⃗ ⊧ e,
ℑ, d⃗ ⊧ e ∨ f iff ℑ, d⃗ ⊧ e or ℑ, d⃗ ⊧ f,
ℑ, d⃗ ⊧ e ∧ f iff ℑ, d⃗ ⊧ e and ℑ, d⃗ ⊧ f,
ℑ, d⃗ ⊧ [p]ϕ iff for all x ∈ ℑ(p)(d⃗) : ℑ, d⃗[i/x] ⊧ ϕ,
ℑ, d⃗ ⊧ ⟨p⟩ϕ iff for some x ∈ ℑ(p)(d⃗) : ℑ, d⃗[i/x] ⊧ ϕ,
ℑ, d⃗ ⊧ [p]^{+}ϕ iff ℑ, d⃗ ⊧ [p]ϕ and ℑ, d⃗ ⊧ ⟨p⟩ϕ.

An interpretation ℑ is a model of a T-Box iff for all actual points d⃗ and all equations ϕ of the T-Box one has ℑ, d⃗ ⊧ ϕ. <

The semantics of the nested role terms [p]q and ⟨p⟩q can be illustrated graphically. Suppose we have two dimensions, time (horizontally) and object (vertically). Furthermore we have an own role, relating objects to the other objects they own at a certain time, and a future role, relating for each object a time point to some set of future time points, for example the object’s lifespan.

The grey parts in the diagram below denote the extension of the own–role for a fixed object o at the various points in time. The compound role [future]own is a relation that relates the current point (o, t) with the set of objects that o owns permanently during its lifespan. The compound role ⟨future⟩own relates o with the set of objects it owns at some future time point of its lifespan.

O

T

[future]own(o, t) {

⟨future⟩own(o, t)

{ {

(o, t) future(o,t)

It should be noted that with respect to this semantics, concept equations are treated in the same way as in terminological languages, i.e., they are required to hold for all actual points. This differs from the usual definition of models in modal logics where a formula is only required to hold at one point (world). Only the characteristic axioms of the particular modal system are required to hold at all points. To really capture both cases one would need a more flexible definition of a model where the elements of some dimensions (e.g., objects) are treated as universally quantified, whereas the objects of the remaining dimensions (e.g., belief worlds) are (implicitly) assumed to be existentially quantified. For the case of two dimensions (objects and intentional worlds for a know-operator), equations are treated in this way in [13]. However, there the modal operator for ‘know’ may only occur in front of equations, but not inside of concept terms. Since our concept and role terms already have a very complex structure we shall concentrate on the concept term level, and leave the treatment of T-Boxes—with a possibly more flexible definition of a model—as a topic of further research.

The basic reasoning services every kl-one system provides are to decide whether a given concept term denotes the empty set or not (satisfiability problem) and whether one concept term always denotes a subset of another concept term (subsumption problem).

Definition 1.3 The concept term e subsumes the concept term f iff, for all interpretations ℑ and actual points d⃗, ℑ, d⃗ ⊧ f implies ℑ, d⃗ ⊧ e.

The concept term e is satisfiable iff there is an interpretation ℑ and an actual point d⃗ such that ℑ, d⃗ ⊧ e. <

Since e subsumes f iff f ∧ ¬e is unsatisfiable, it is sufficient to have an algorithm for the satisfiability problem.

1.1 An Alternative Presentation of the Semantics

In the above definition of the semantics we interpret role terms p as functions giving for an n–tuple of worlds the set of accessible worlds. The interpretation function takes care of the dimension information about p. Alternatively one could interpreted role terms p as relations between n– tuples which differ only in the i–th coordinate, where i = dim(p). This means ℑ(p) ⊆ D⃗ × D⃗ with the constraint

(x⃗, y⃗) ∈ ℑ(p) implies y⃗ = x⃗[i/z] for some z.  (1)

The complex role terms are defined accordingly (i = dim(p), j = dim(q)):

(x⃗, x⃗[j/z]) ∈ ℑ([p]q) iff ∀v (x⃗, x⃗[i/v]) ∈ ℑ(p) ⇒ (x⃗[i/v], x⃗[i/v, j/z]) ∈ ℑ(q)  (2)
(x⃗, x⃗[j/z]) ∈ ℑ(⟨p⟩q) iff ∃v (x⃗, x⃗[i/v]) ∈ ℑ(p) ∧ (x⃗[i/v], x⃗[i/v, j/z]) ∈ ℑ(q)  (3)
(x⃗, y⃗) ∈ ℑ([p]^{+}q) iff (x⃗, y⃗) ∈ ℑ([p]q) and (x⃗, y⃗) ∈ ℑ(⟨p⟩q)  (4)

The interpretation function can now be defined in the traditional modal logic style.

ℑ, d⃗ ⊧ [p]ϕ iff for all d⃗′:  (d⃗, d⃗′) ∈ ℑ(p) implies ℑ, d⃗′ ⊧ ϕ
ℑ, d⃗ ⊧ ⟨p⟩ϕ iff there exists d⃗′: (d⃗, d⃗′) ∈ ℑ(p) and ℑ, d⃗′ ⊧ ϕ

As a further simplification of the semantics, we can assume without loss of generality that all domains D_{i} are identical. This means that our n–dimensional space D⃗ is in fact an n–dimensional cube D^{n}.

It is straightforward to show that these two presentations of the semantics are equivalent in the sense that exactly the same formulae are true in both versions. In the sequel we shall therefore make use of both alternatives.

2 Relation to Known Systems

The first question one usually asks about a new logical or mathematical system is of course how it relates to well-known other systems. If the new system is an old system in disguise, one can save a lot of work. If it is some variation of an old system, one can often adapt results and techniques that have been developed for the old system.

2.1 n-Dimensional M-ALC with Atomic Role Terms

The n-dimensional case without nested role terms is the simplest fragment of M-ALC. In this case there is no longer a difference between the 1-dimensional and the n-dimensional case. To be more precise, for a given n-dimensional M-ALC language L_{n}, we obtain a 1-dimensional language L_{1} if we define the dimensions of all role names to be 1. For a given concept term c of L_{n}, we say that c is satisfiable in n dimensions iff it is satisfiable as concept term of L_{n}. The term c is satisfiable in 1 dimension iff it is satisfiable as concept term of L_{1}. We show that satisfiability in L_{n} is identical with satisfiability in L_{1}, provided there are no nested role terms.

Theorem 2.1 Let L_{n} be an n-dimensional M-ALC-language, and let c_{0} be a concept term of this language that contains only atomic role terms. Then c_{0} is satisfiable in one dimension if, and only if, it is satisfiable in n dimensions.

Proof: First, assume that c_{0} is satisfiable in n dimensions. Let ℑ = (D⃗, ℑ_{Σ}) be an n-dimensional interpretation such that ℑ, d⃗_{0} ⊧ c_{0} for some d⃗_{0} ∈ D⃗. The n-dimensional interpretation ℑ yields the following 1-dimensional interpretation ℑ′ = (D′_{1}, ℑ′_{Σ}): We define D′_{1} =^{def} D⃗, for all concept names c, ℑ′_{Σ}(c) =^{def} ℑ_{Σ}(c), and for all role names p, ℑ′_{Σ}(p)(d⃗) =^{def} {d⃗[i/x] | x ∈ ℑ_{Σ}(p)(d⃗)} (where i = dim(p)).

By induction on the structure of concept terms, it is now easy to show that, for all concept terms c containing only atomic role terms, and all d⃗ ∈ D⃗, we have ℑ, d⃗ ⊧ c iff ℑ′, d⃗ ⊧ c. Thus, ℑ′, d⃗_{0} ⊧ c_{0}, which shows that c_{0} is satisfiable in 1 dimension.

Second, assume that c_{0} is satisfiable in 1 dimension. Let ℑ = (D, ℑ_{Σ}) be a 1-dimensional interpretation such that ℑ, d_{0} ⊧ c_{0} for some d_{0} ∈ D. We use ℑ to construct an n-dimensional interpretation ℑ′ = (D⃗, ℑ′_{Σ}) as follows:

• For all i, 1 ≤ i ≤ n, we define D_{i} =^{def} D × IN where IN denotes the set of nonnegative integers. For a tuple d⃗ = ((d_{1}, k_{1}), ..., (d_{n}, k_{n})) ∈ D⃗, let max(d⃗) be (d_{i}, k_{i}) iff k_{i} is strictly greater than all k_{j} for j ≠ i. If such an i does not exist then max(d⃗) is undefined.

• For all concept names c, we define ℑ′_{Σ}(c) =^{def} {d⃗ | max(d⃗) = (d_{i}, k_{i}) and d_{i} ∈ ℑ_{Σ}(c)}.

• For all role names p and all d⃗ ∈ D⃗, we define ℑ′_{Σ}(p)(d⃗) =^{def} ∅, if max(d⃗) is undefined. Otherwise, let max(d⃗) = (d_{i}, k_{i}). Then ℑ′_{Σ}(p)(d⃗) =^{def} {(d, k_{i} + 1) | d ∈ ℑ_{Σ}(p)(d_{i})}. Note that dim(p) may of course be different from i.

By induction on the structure of concept terms c containing only atomic role terms, we show the following claim:

If d⃗ ∈ D⃗ is such that max(d⃗) = (d_{i}, k_{i}) is defined then we have ℑ′, d⃗ ⊧ c iff ℑ, d_{i} ⊧ c.

(1) If c is a concept name then the claim holds by definition of ℑ′_{Σ}(c).

(2) Let c be of the form c_{1} ∧c_{2}. We have ℑ′, d⃗ ⊧ c_{1} ∧c_{2} iff ℑ′, d⃗ ⊧ c_{1} and ℑ′, d⃗ ⊧ c_{2}. By induction, this is the case iff ℑ, d_{i} ⊧ c_{1} and ℑ, d_{i} ⊧ c_{2}, i.e., iff ℑ, d_{i} ⊧ c_{1} ∧ c_{2}.

(3) Disjunction and negation can be treated similarly.

(4) Let c be of the form ⟨p⟩c_{1} where p is a role name of dimension j. First, assume that ℑ′, d⃗ ⊧ ⟨p⟩c_{1}. Thus, there is (d, k) in ℑ′_{Σ}(p)(d⃗) and ℑ′, d⃗[j/(d, k)] ⊧ c_{1}. Since max(d⃗) = (d_{i}, k_{i}), the definition of ℑ′_{Σ}(p) implies that d ∈ ℑ_{Σ}(p)(d_{i}), and k = k_{i} + 1. Consequently, max(d⃗[j/(d, k)]) = (d, k), and by induction, ℑ′, d⃗[j/(d, k)] ⊧ c_{1} yields ℑ, d ⊧ c_{1}. Since we also know that d ∈ ℑ_{Σ}(p)(d_{i}), this implies ℑ, d_{i} ⊧ ⟨p⟩c_{1}. Second, assume that ℑ, d_{i} ⊧ ⟨p⟩c_{1}. Thus, there is d ∈ ℑ_{Σ}(p)(d_{i}) such that ℑ, d ⊧ c_{1}. By definition, ℑ′_{Σ}(p)(d⃗) contains (d, k_{i} + 1). Since max(d⃗[j/(d, k)]) = (d, k_{i} + 1), induction applied to ℑ, d ⊧ c_{1} yields ℑ′, d⃗[j/(d, k)] ⊧ c_{1}. This, together with (d, k_{i} + 1) ∈ ℑ′_{Σ}(p)(d⃗), yields ℑ′, d⃗ ⊧ ⟨p⟩c_{1}.

(5) The case where c is of the form [p]c_{1} can be treated similarly. This completes the proof of the claim.

Now, let d_{0} be such that ℑ, d_{0} ⊧ c_{0}. We define d⃗ = ((d_{1}, k_{1}), ..., (d_{n}, k_{n})) as follows: d_{j} =^{def} d_{0} for all j, 1 ≤ j ≤ n, k_{1} =^{def} 1, and k_{j} =^{def} 0 for all j, 2 ≤ j ≤ n. The above claim yields ℑ′, d⃗ ⊧ c_{0}, which shows that c_{0} is satisfiable in n dimensions. <

By this theorem, as long as one does not use compound role terms, one can just forget about the dimensions: M-ALC collapses to the multi–modal version of the modal system K, which is a syntactic variant of ALC. All results and algorithms of ALC carry over to this fragment of M-ALC. Hence, satisfiability of concept terms can be decided using the well-know algorithm for ALC, and the complexity results for ALC show that the satisfiability problem is PSPACE complete [20].

Unfortunately, if a concept term c contains complex role terms, then satisfiability in one dimension is different from satisfiability in n dimensions.

Theorem 2.2 There is a 2-dimensional M-ALC language L_{2} and a concept term c of L_{2} such that c is satisfiable in 2 dimensions, but not in 1 dimension.

Proof: This is demonstrated by the following example. Assume that e is a concept name, p is a role name of dimension 1, and q is a role name of dimension 2. We consider the term [⟨p⟩q]e ∧ ¬[p][q]e. The 2-dimensional interpretation ℑ is defined as follows:

• D_{1} =^{def} {0, 1} =: D_{2}.

• ℑ_{Σ}(p)(0, 0) =^{def} {1} and ℑ_{Σ}(p)(d⃗) =^{def} ∅ for all d⃗ ∈ D⃗ \ {(0, 0)}.

• ℑ_{Σ}(q)(1, 0) =^{def} {1} and ℑ_{Σ}(q)(d⃗) =^{def} ∅ for all d⃗ ∈ D⃗ \ {(1, 0)}.

• ℑ_{Σ}(e) =^{def} {(0, 0), (0, 1), (1, 0)}.

Since ¬[p][q]e is equivalent to ⟨p⟩⟨q⟩¬e, and since ℑ, (1, 1) ⊧ ¬e, the definitions of ℑ_{Σ}(p) and ℑ_{Σ}(q) yield ℑ, (0, 0) ⊧ ¬[p][q]e.

The definition of the semantics for role terms yields ℑ(⟨p⟩q)(0, 0) = {1}, since ℑ(p)(0, 0) = {1}, and ℑ(q)(1, 0) = {1}. Now, ℑ, (0, 0) ⊧ [⟨p⟩q]e since ℑ, (0, 1) ⊧ e. Thus we have shown that [⟨p⟩q]e ∧ ¬[p][q]e is satisfiable in 2 dimensions.

In one dimension, however, ⟨p⟩q denotes nothing else than the composition of the p and q–roles. Therefore [⟨p⟩q]φ ⇔ [p][q]φ for all φ, which makes [⟨p⟩q]e ∧ ¬[p][q]e inconsistent. <

The reason for the difference between the one–dimensional and the n–dimensional case lies in the interpretation of role terms, as shown in the proof of the theorem. In one dimension the interpretation of the role term ⟨p⟩q is identical to the composition of the interpretations of p and q. This need not be the case if one has more than one dimension.

2.2 M-ALC with Compound Role Terms

A compound role term denotes an accessibility relation in the same way as an atomic role term, except that its interpretation depends on the interpretation of its components. Thus, one could again try to interpret M-ALC as a standard (one-dimensional) multi–modal logic, but with special restrictions on the accessibility relations corresponding to the structure of compound role terms. In this subsection we characterize a class of one–dimensional frames whose theorems coincide with the M-ALC theorems. To this end we exploit some results about how to axiomatize n–dimensional modal logic due to Y. Venema [22]. Venema’s axioms capture the fact that we are operating in an n–dimensional environment. We shall add axioms that express the semantics of compound role terms.

Results about n–Dimensional Modal Logic (Yde Venema)

Venema has investigated a modal logic with coordinate operators □_{i}. Intuitively □_{i} is an operator that moves along the i–th coordinate: the underlying i–th accessibility relation connects all points that can be obtained from each other by just changing the i–th coordinate. Venema gives an axiomatization of these operators which characterizes in fact the n–dimensional cubes. As auxiliary operators, however, constant ‘diagonal operators’ δ_{ij} are needed. Intuitively, δ_{ij} is true in a world (i.e., a tuple) iff its i–th and j–th coordinate are identical. We briefly recall Venema’s main results.

Definition 2.3 Cylindrical Modal Logic The signature of cylindrical modal logic CML_{n} of dimension n contains n normal modal operators □_{i} and the corresponding dual operators ◇_{i}, together with the n^{2} constant operators δ_{ij}.

There are two different versions of the semantics for cylindrical modal logic:

1. n–dimensional semantics: The n–dimensional frames of CML_{n} are the n–cubes D^{n} for sets D. The interesting part of the satisfiability relation is:

(u_{1}, …, u_{n}) ⊧ □_{i}φ iff for all v: (u_{1}, …, u_{i−1}, v, u_{i+1}, …, u_{n}) ⊧ φ

(u_{1}, …, u_{n}) ⊧ δ_{ij} iff u_{i} = u_{j}

2. one–dimensional semantics: The one–dimensional frames of CML_{n} consist of a set W of worlds, for each modal operator □_{i} a binary accessibility relation T_{i}, and for each unary operator δ_{ij} a unary predicate E_{ij}. The accessibility relations satisfy the following conditions (for i ≠ j in B2_{ij} and B4_{ij} and additionally, k ≠ i and k ≠ j in B3_{ijk}):

A1_{i} ∀x T_{i}(x, x)
A2_{i} ∀x, y T_{i}(x, y) ⇒ T_{i}(y, x)
A3_{i} ∀x, y T_{i}(x, y) ∧ T_{i}(y, z) ⇒ T_{i}(x, z)
A4_{ij} ∀x, y (∃z T_{i}(x, z) ∧ T_{j}(z, y)) ⇒ (∃z T_{j}(x, z) ∧ T_{i}(z, y))
B1_{i} ∀x E_{ii}(x)
B2_{ij} ∀x, y, z T_{i}(x, y) ∧ E_{ij}(y) ∧ T_{i}(x, z) ∧ E_{ij}(z) ⇒ y = z
B3_{ijk} ∀x E_{ij}(x) ⇔ (∃y T_{k}(x, y) ∧ E_{ik}(y) ∧ E_{kj}(y))
B4_{ij} ∀x, y, z (E_{ij}(x) ∧ T_{i}(x, y) ∧ T_{j}(y, z) ∧ y ≠ z)
⇒ ∃u (¬E_{ij}(u) ∧ T_{j}(x, u) ∧ T_{i}(u, z))
B5_{i} ∀x, y, z H_{1}(x, y) ∧ T_{2}(x, z) ∧ E_{21}(z) ∧ T_{1}(z, y) ⇒ E_{1i}(y)

where H_{1}(x, y) ⇔ ∃z_{3}, …, z_{n} T_{2}(x, z_{3}) ∧ T_{3}(z_{3}, z_{4}) ∧ … ∧ T_{n}(z_{n}, y).

(B3_{ijk} and B5_{i} are superfluous if n = 2.)

Let us call the frames satisfying the above conditions n–frames.

The satisfaction relation for the operators □_{i} and ◇_{i} are as usual. For the δ_{ij}–operators we have: w ⊧ δ_{ij} iff E_{ij}(w) holds. <

The meaning of the axioms can best be understood by drawing pictures of the situation in the n–dimensional setting. For example, the axiom B4_{ij} can be illustrated by a two–dimensional coordinate system, where one axis stands for dimension i and the other axis stands for dimension j (see the left diagram in Figure 1).

Theorem 2.4 (Venema)

(i) Every n–frame is isomorphic to the disjoint union of some n–cubes, i.e. there is a bijective mapping between the n–frame and the n–cubes which is also a homomorphism and antihomomorphism with respect to the accessibility relations on the n–frame side and the corresponding movements along the coordinates at the n–cube side. (ii) A CML_{n} formula φ is a theorem in the n-dimensional semantics if, and only if, it is a theorem in the one–dimensional semantics. <

In part (i) of the theorem, every n–cubes in the disjoint union corresponds to a connected component of the n–frame.

Now, we merge CML_{n} with M-ALC by adding to CML_{n} our M-ALC–operators. In order to emphasize that the compound role terms are interpreted as accessibility relations in the usual sense, we assume that for each (possibly compound) role term p there is a unique name. For role

[figure: δ_{i,j}; z; u; ≠; y; x; x; u; v; y; p; q; ⟨p⟩q; i; j; j; i]

Figure 1: The left diagram illustrates axiom B4_{ij}, and the right diagram illustrates axiom D1_{pq} (see below).

names, we can use the role name itself. Now assume that p′ is the name for the role term p, and q′ is the name for the role term q. For [p]q we introduce the name b_{p′,q′}, for [p]^{+}q we introduce b_{p′,q′}^{+} and for ⟨p⟩q we introduce d_{p′,q′}. The interpretation of these new role names must, of course, be restricted to mirror the role constructors’ original semantics.

Definition 2.5 (M-ALC–CML_{n}) The syntax of the logic M-ALC–CML_{n} contains the operators of M-ALCand CML_{n} together. Like CML_{n}, the logic M-ALC–CML_{n} has a one–dimensional semantics and an n–dimensional semantics.

• n–dimensional semantics: As in the n–dimensional semantics of CML_{n}, the frames are n–cubes over a set D. The satisfiability relation for the CML_{n}–operators is as in CML_{n}. The M-ALC parts are interpreted according to the alternative presentation of the M-ALC semantics (see Subsection 1.1).

• one–dimensional semantics: A one-dimensional M-ALC–CML_{n}–frame consists of a set W of worlds, the relations T_{i} and E_{ij} of CML_{n}’s one–dimensional semantics, for each primitive role term a binary relation p, and for the names for compound role terms the binary relations b_{p,q}, b_{p,q}^{+} and d_{p,q}. The various relations satisfy the following conditions:

The axioms A1_{i} – A4_{ij} and B1_{i} – B5_{i} of CML_{n} (Definition 2.3,ii). For dim(p) = dim(q) = j:

C1_{pq} T_{j}(x, y) ⇒ (b_{p,q}(x, y) ⇔ (∀z p(x, z) ⇒ q(z, y)))
C2_{pq} d_{p,q}(x, y) ⇔ (∃w p(x, w) ∧ q(w, y))

For i = dim(p) ≠ dim(q) = j:

D1_{pq} ∀x, y d_{p,q}(x, y) ⇒ ∃u, v p(x, u) ∧ q(u, v) ∧ T_{i}(v, y)
D2_{pq} ∀x, y (∃u p(x, u) ∧ q(u, y)) ⇒ (∃v T_{i}(y, v) ∧ d_{p,q}(x, v))
D3_{pq} ∀x, y b_{p,q}(x, y) ⇒ (∀u p(x, u) ⇒ ∃v q(u, v) ∧ T_{i}(v, y))
D4_{pq} ∀x, y (T_{j}(x, y) ∧ (∀u, v (p(x, u) ∧ T_{j}(u, v) ∧ T_{i}(v, y)) ⇒ q(u, v)))
⇒ b_{p,q}(x, y)
E1_{p} ∀x, y p(x, y) ⇒ T_{i}(x, y)
E2_{q} ∀x, y q(x, y) ⇒ T_{j}(x, y)
E3_{pq} ∀x, y b_{p,q}(x, y) ⇒ T_{j}(x, y)
E4_{pq} ∀x, y d_{p,q}(x, y) ⇒ T_{j}(x, y)

Definition of b_{p,q}^{+}

F_{pq} b_{p,q}^{+}(x, y) ⇔ (b_{p,q}(x, y) ∧ d_{p,q}(x, y))

In the sequel we call the n–dimensional frames n–cubes and the one–dimensional frames satisfying the above conditions n–frames. <

As in the CML_{n} semantics, one should read T_{i}(x, y) as ‘y can be obtained from x by changing just the i-th coordinate’. Under this interpretation the axioms for the compound role terms correspond precisely to their definitions in the n–dimensional semantics. The next lemma confirms that the n–cubes are in fact n–frames over a set of worlds consisting of n–tuples.

Lemma 2.6 If in the n–dimensional setting we interpret the coordinate accessibility relations T_{i} as movement along the i^{th} coordinate, i.e. T_{i}(x⃗, y⃗) iff y⃗ = x⃗[i/z], for some z, and we interpret the diagonal predicates E_{ij} as E_{ij}(x⃗) iff x_{i} = x_{j}, then every n–cube is also an n–frame.

Proof : We must show that all conditions on n–frames hold in n–cubes. A trivial corollary of Venema’s results guarantees that the axioms A1_{i} – A4_{ij} and B1_{i} – B5_{i} hold in n–cubes. C1_{pq}, C2_{pq} and F_{pq} are direct consequences of the definitions (2), (3) and (4), and E1_{p} – E4_{pq} follow from the constraint (1). Now, we check the remaining conditions one by one. Let i = dim(p) and j = dim(q) = dim(d_{p,q}) = dim(b_{p,q}) for i ≠ j.

D1_{pq}: Suppose 1: d_{p,q}(x⃗, y⃗)

1 and (1): y⃗ = x⃗[j/z] for some z

1 and (3): ∃u′ p(x⃗, x⃗[i/u′]) ∧ q(x⃗[i/u′], x⃗[i/u′, j/z]):
u⃗ = x⃗[i/u′], v⃗ = x⃗[i/u′, j/z]: ∃u, v p(x⃗, u⃗) ∧ q(u⃗, v⃗) ∧ T_{i}(v⃗, y⃗)
D2_{pq}: Suppose  1: p(x⃗, u⃗) and 2: q(u⃗, y⃗)  for some x⃗, y⃗, u⃗
1 and (1):  u⃗ = x⃗[i/u′], i.e. p(x⃗, x⃗[i/u′])
2 and (1):  y⃗ = x⃗[i/u′, j/v′], i.e. q(x⃗[i/u′], x⃗[i/u′, j/v′])
(3): 3: d_{p,q}(x⃗, x⃗[j/v′])
and 4: T_{i}(y⃗, x⃗[j/v′])
3 and 4: ∃v⃗ T_{i}(y⃗, v⃗) ∧ d_{p,q}(x⃗, v⃗)

D3_{pq}: Suppose 1: b_{p,q}(x⃗, y⃗)

1 and (1): y⃗ = x⃗[j/y] for some y

1 and (2): 2: for all z: p(x⃗, x⃗[i/z]) ⇒ q(x⃗[i/z], x⃗[i/z, j/y])
Suppose 3: p(x⃗, x⃗[i/u])
3 and 2: 4: q(x⃗[i/u], x⃗[i/u, j/y])
interpretation of T_{i}: 5: T_{i}(x⃗[i/u, j/y], x⃗[j/y])
4,5, v⃗ = x⃗[i/u, j/y]: ∃v⃗ q(x⃗[i/u], v⃗) ∧ T_{i}(v⃗, x⃗[j/y])

D4_{pq}: Suppose 1: T_{j}(x⃗, y⃗) where y⃗ = x⃗[j/y]

Suppose 2: p(x⃗, x⃗[i/u]) and T_{j}(x⃗[i/u], x⃗[i/u, j/v]) and

T_{i}(x⃗[i/u, j/v], y⃗) implies q(x⃗[i/u], x⃗[i/u, j/v])
for all u, v

2 and interpretation of T_{i}: 3: v = y

2,3 and (2) b_{p,q}(x⃗, x⃗[j/y]) <

In order to show that the n–dimensional semantics and the one–dimensional semantics of M-ALC–CML_{n} yield the same theorems, a standard technique is to show that one class of frames is a zigzagmorphic image of the other class. A zigzagmorphism φ (p-morphism, bounded morphism) between a frame A and a frame B is a homomorphism from A to B which preserves the structure of the accessibility relations. In particular we have

1. p(a, b) holds in A then p(φ(a), φ(b)) holds in B (homomorphism condition),

2. if p(φ(a), b′) holds in B then there is a b in A with b′ = φ(b) and p(a, b) holds in A (zizag condition).

Lemma 2.7 Every connected one–dimensional frame of M-ALC–CML_{n} is the zigzagmorphic image of an n–dimensional M-ALC–CML_{n}–frame.

Proof: Let F_{1} be a connected one–dimensional frame. It satisfies the conditions A1_{i} – B5_{i} of CML_{n}. Therefore there exists an isomorphism f between an n–cube and F_{1} (Theorem 2.4). In particular this isomorphism guarantees for all i:

T_{i}(f(x⃗), f(y⃗)) ⇔ y⃗ = x⃗[i/z] for some z  (5)
T_{i}(f(x⃗), y) ⇒ ∃z f(x⃗[i/z]) = y  (6)

Moreover, it also guarantees that

∀x, y T_{i}(x, y) ∧ T_{j}(x, y) ⇒ x = y  for i ≠ j  (7)

holds in the one–dimensional frame.

In the main part of the proof we extend this n–cube to a n–dimensional M-ALC–CML_{n}–frame F_{n} and show that f is in fact a zigzag morphism from F_{n} to F_{1}. To simplify the notation, we assume in the sequel that we have only two dimensions, 1 and 2.

First, we must prove one useful property:

∀a, b, c, d, x: T_{1}(f(a, b), x) ∧ T_{2}(f(c, d), x) ⇒ f(c, b) = x  (8)
Suppose  1: T_{1}(f(a, b), x) and 2: T_{2}(f(c, d), x)
1 and (6):  3: x = f(a′, b) for some a′
2 and (6):  4: x = f(c, d′) for some d′
(5):  5: T_{1}(f(a′, b), f(c, b))  ( ⇔ T_{1}(x, f(c, b)) by 3)
(5):  6: T_{2}(f(c, d′), f(c, b))  ( ⇔ T_{2}(x, f(c, b)) by 4)
5, 6 and (7): f(c, b) = x

Since the role terms can be arbitrarily nested we show the homomorphism and zigzag condition for f by induction on the structure of the role terms.

\underline{Base Case:} For a primitive role p with dim(p) = i let p^{1} be its interpretation in F_{1}. We define p^{n}(u⃗, v⃗) iff p^{1}(f(u⃗), f(v⃗)) as the interpretation of p in F_{n}. Because of axiom E1_{p} it is guaranteed that p^{n} moves only along the i’th dimension. Furthermore the homomorphism condition and the zigzag morphism condition are obviously satisfied.

\underline{Induction Step:} Once the primitive roles have an interpretation in F_{n}, the interpretation of the corresponding compound roles is fixed. We must show that the homomorphism conditions and the zigzag conditions are satisfied by this interpretation.

For the case that dim(p) = dim(q), the conditions C1_{pq} and C2_{pq} guarantee that the interpretation of b_{p,q} and d_{p,q} in the one–dimensional case and in the n–dimensional case have a one to one correspondence. The homomorphism and zigzag conditions hold trivially.

By axiom F_{pq}, the homomorphism and zigzag conditions for b_{p,q}^{+} hold once the corresponding conditions for b_{p,q} and d_{p,q} are established (even if the dimensions of p and q are different).

Thus, it remains to check the conditions for b_{p,q} and d_{p,q} in the case of different dimensions of p and q. In the sequel, we assume that the dimension of p is 1 and the dimension of q is 2.

• Homomorphism condition for b_{p,q}:

∀x, y, z b_{pq}^{n}((x, y), (x, z)) ⇒ b_{pq}^{1}(f(x, y), f(x, z)).

Suppose: 1: b_{pq}^{n}((a, b), (a, c)) for some a, b, c. 1 and (2): 2: ∀z p^{n}((a, b), (z, b)) ⇒ q^{n}((z, b), (z, c)) Suppose: 3: T_{2}(u, v) and 4: T_{1}(v, f(a, c)) and 5: p^{1}(f(a, b), u)

(we want to apply D4_{pq} for x = f(a, b) and y = f(a, c))

5, induction hypothesis: 6: p^{n}((a, b), (d, b)) and 6: f(d, b) = u for some d (zigzag condition) 6 and 2: 7: q^{n}((d, b), (d, c)) 7, induction hypothesis: 8: q^{1}(f(d, b), f(d, c)) (homomorphism condition) 3 and 6: 9: T_{2}(f(d, b), v) 4,9, A2_{1} and (8): 10: f(d, c) = v 6, 8 and 10: 11: q^{1}(u, v) 3-11: 12: T_{2}(u, v) ∧ T_{1}(v, f(a, c)) ∧ p^{1}(f(a, b), u) ⇒ q^{1}(u, v) f is an isomorphism: 13: T_{2}(f(a, b), f(a, c)) 12, 13 and D4_{pq}: b_{pq}^{1}(f(a, b), f(a, c))

• Zigzag condition for b_{p,q}: b_{pq}^{1}(f(x, y), z) ⇒ ∃u b_{pq}^{n}((x, y), (x, u)) ∧ f(x, u) = z.

Suppose: 1: b_{pq}^{1}(f(a, b), c) for some a, b, c 1 and D3_{pq}: 2: ∀u p^{1}(f(a, b), u) ⇒ ∃v q^{1}(u, v) ∧ T_{1}(v, c) Suppose: 3: p^{n}((a, b), (y, b)) for some y 3 and induction hypothesis: 4: p^{1}(f(a, b), f(y, b)) 2 and 4: 5: q^{1}(f(y, b), v) and 6: T_{1}(v, c) for some v 5, induction hypothesis: 7: q^{n}((y, b), (y, x)) and 8: f(y, x) = v for some x (zigzag condition) 6 and 8: 9: T_{1}(f(y, x), c) 1 and E3_{pq}: 10: T_{2}(f(a, b), c) 9, 10 and (8): 11: f(a, x) = c Suppose: 12: p^{n}((a, b), (y′, b)) for some y′ As in 3–11 above: 13: q^{n}((y′, b), (y′, x′))

and 14: f(y′, x′) = v′ for some x′,

and 15: f(a, x′) = c

11, 15, f isomorphism: 16: x = x′ 13–15: 17: ∀y′ p^{n}((a, b), (y′, b)) ⇒ q^{n}((y′, b), (y′, x)) 17 and (2): 18: b_{pq}^{n}((a, b), (a, x)) 18 and 11: ∃x b_{pq}^{n}((a, b), (a, x)) ∧ f(a, x) = c

• Homomorphism condition for d_{p,q}:

∀x, y, z d_{pq}^{n}((x, y), (x, z)) ⇒ d_{pq}^{1}(f(x, y), f(x, z)).

Suppose: 1: d_{pq}^{n}((a, b), (a, c)) for some a, b, c 1 and (3): 2: ∃x p^{n}((a, b), (x, b)) ∧ q^{n}((x, b), (x, c)) 2, induction hypothesis: 3: ∃x p^{1}(f(a, b), f(x, b)) ∧ q^{1}(f(x, b), f(x, c)) (homomorphism condition) 3 and D2_{pq}: 4: T_{1}(f(x, c), v) and 5: d_{pq}^{1}(f(a, b), v) for some v 5 and E4_{pq}: 6: T_{2}(f(a, b), v) 4, 6 and (8): 7: f(a, c) = v 7 and 5: d_{pq}^{1}(f(a, b), f(a, c))

• Zigzag condition for d_{p,q}:

d_{pq}^{1}(f(x, y), z) ⇒ ∃u d_{pq}^{n}((x, y), (x, u)) ∧ f(x, u) = z.

Suppose: 1: d_{pq}^{1}(f(a, b), c) for some a, b, c 1 and D1_{pq}: 2: p^{1}(f(a, b), u) and 3: q^{1}(u, v) and

4: T_{1}(v, c) for some u, v

2, induction hypothesis: 5: p^{n}((a, b), (d, b)) and 6: f(d, b) = u for some d (zigzag condition) 3 and 6: 7: q^{1}(f(d, b), v) 7, induction hypothesis: 8: q^{n}((d, b), (d, e)) and 9: f(d, e) = v for some e (zigzag condition) 4 and 9: 10: T_{1}(f(d, e), c) 1 and E4_{pq}: 11: T_{2}(f(a, b), c) 10, 11 and (8): 12: f(a, e) = c 5 and 8 and (3): 13: d_{pq}^{n}((a, b), (a, e)) 12 and 13: ∃u d_{pq}^{n}(a, b, a, u) ∧ f(a, u) = c (choose u = e)

<

Theorem 2.8 A M-ALC–CML_{n}–formula is a theorem in the n–dimensional semantics if, and only if, it is a theorem in the one–dimensional semantics.

Proof: First of all, according to Lemma 2.6, n–dimensional frames are also one–dimensional frames. Therefore, a formula that is true in all one–dimensional frames is also true in all n– dimensional frames.

In every modal logic, a formula is a theorem if, and only if, it holds in every generated subframes. Therefore only one connected component of a frame need to be considered. In Lemma 2.7 we have shown that every connected one–dimensional frame of M-ALC–CML_{n} is the zigzagmorphic image of a n–dimensional M-ALC–CML_{n}–frame. Hence, they have the same modal theory [21].

<

With this theorem we have in principle succeeded in describing M-ALC in the standard multi– modal logic framework with standard operators and standard accessibility relations. But the frame conditions are so complex that it is not clear whether one can employ of this result in some useful way. Thus, the question arises whether it is possible to simplify the set of axioms. A key observation is that the formulae we are interested in are pure M-ALC formulae. These formulae do not contain the diagonal operators δ_{ij} or the coordinate operators □_{i} and ◇_{i}. Hence, one may ask whether these auxiliary^{3} operators are really necessary: Is it possible to simplify the axiomatization such that (i) the predicates E_{ij} and T_{i} do not occur, but (ii) the δ_{ij} and □_{i}–free theorems stay the same. As the next theorem shows, it is in fact possible to eliminate the δ_{ij} part of the logic.

Theorem 2.9 Let L be the δ_{ij}–free part of the logic M-ALC–CML_{n} with one–dimensional semantics. This means that all frame conditions except the conditions B1_{i}–B5_{i} are assume to hold. For all δ_{ij}–free M-ALC–CML_{n} formula φ the formula φ is a M-ALC–CML_{n} theorem if, and only if, φ is a L theorem.

Proof: By definition, all M-ALC–CML_{n}–frames are also L–frames. If φ is a L–theorem then it holds in all L–frames and therefore also in all M-ALC–CML_{n}–frames. Thus, the nontrivial part is the other direction. Here we must show that the conditions on the E_{ij}–predicates have no influence on the theorem-hood of δ_{ij}–free formulae.

Suppose φ is a M-ALC–CML_{n}–theorem. It is well known that for any multi–modal logic theorem φ, the ‘relationally’ translated predicate logic formula π(φ) [17] is a predicate logic consequence of the predicate logic axiomatization of the frame conditions. The relational translation maps every propositional variable to a one–place predicate which takes a ‘world term’ as argument. The modal part of the language is translated using the modal operators’ semantics definitions as rewrite rules:

\begin{aligned}π([p]ψ, w) & = & ∀v p(w, v) ⇒ π(ψ, v) \\ π(⟨p⟩ψ, w) & = & ∃v p(w, v) ∧ π(ψ, v) \\ π(δ_{ij}, w) & = & E_{ij}(w) \end{aligned}

This means that Ψ ⇒ π(φ) is a predicate logic theorem where Ψ is an axiomatization of the frame conditions for M-ALC–CML_{n}, consisting of the axioms A1_{i}–B5_{i}, C1_{pq}–C2_{pq} and D1_{ij}–E4_{pq}. Thus, Ψ ∧ ¬π(φ) is unsatisfiable in predicate logic. By the completeness of the hyperresolution strategy [18], there is a hyperresolution deduction of the empty clause from the clause form of Ψ ∧ ¬π(φ) together with the equality formulae. We show that the axioms B1_{i}–B5_{i} cannot participate in this refutation. The clause form of B1_{i}–B5_{i} is

\begin{matrix}B1_{i} & E_{ii}(x) \\ B2_{ij} & ¬T_{i}(x, y), ¬E_{ij}(y), ¬T_{i}(x, z), ¬E_{ij}(z), y = z \\ B3_{ijk}, 1 & ¬E_{ij}(x), T_{k}(x, f_{2}(x)) \\ B3_{ijk}, 2 & ¬E_{ij}(x), E_{ik}(f_{2}(x)) \\ B3_{ijk}, 3 & ¬E_{ij}(x), E_{kj}(f_{2}(x)) \\ B3_{ijk}, 4 & E_{ij}(x), ¬T_{k}(x, y), ¬E_{ik}(y), ¬E_{kj}(y) \\ B4_{ij}, 1 & ¬E_{ij}(x), ¬T_{i}(x, y), ¬T_{j}(y, z), y = z, ¬E_{ij}(f_{3}(x, y, z)) \\ B4_{ij}, 2 & ¬E_{ij}(x), ¬T_{i}(x, y), ¬T_{j}(y, z), y = z, T_{j}(x, f_{3}(x, y, z)) \\ B4_{ij}, 3 & ¬E_{ij}(x), ¬T_{i}(x, y), ¬T_{j}(y, z), y = z, T_{i}(f_{3}(x, y, z), z) \\ B5_{i} & ¬H_{1}(x, y), ¬T_{2}(x, z), ¬E_{21}(z), ¬T_{1}(z, y), E_{1i}(y). \end{matrix}

3from the standpoint of pure M-ALC

Besides B1_{i} there are only clauses with literals of mixed sign. They can only play the role of a nucleus of a hyperresolution step. Since all of these clauses contain negative E_{ij}–literals, they need a clause with only positive literals and at least one such clause with a positive E_{ij}–literal as electron. Neither the equality clauses nor the remaining clauses of Ψ nor the clause form of ¬π(φ) contains such a clause (φ is δ_{ij}–free). Thus, no hyperresolution step with these clauses is possible. B1_{i} = E_{ii}(x) cannot participate either because in all other clauses with E_{ij}, i ≠ j is required.

Hence, (Ψ \ B1_{i}–B5_{i}) ⇒ π_{r}(φ) is a predicate logic theorem. This means that φ is a L–theorem.

<

It is, however, not clear how to eliminate the relations T_{i} that correspond to the coordinate operators. It could be the case that any reasonable axiomatization needs such auxiliary relations. The conclusion of this section is not quite satisfactory. We did manage to describe M-ALC in terms of classical multi–modal logics. We have shown that the nested role terms can be understood as ordinary parameters of a parameterized modal operator, where the structure of the frames is specified by the conditions A1_{i} – A4_{i}, C1_{pq},C2_{pq}, D1_{pq} – D4_{pq}, E1_{p} – E4_{pq} and F_{pq}. However, no further simplification of these rather complex conditions seems possible, even under the assumption that the theorems we want to prove do not contain the coordinate operators. The naturally asked question whether there is a Hilbert style axiomatization for M-ALC therefore also remains open. The difficult conditions which do not have an obvious corresponding Hilbert axiom are D4_{pq} and the ⇒–part of C2_{pq}.

So far, it is not clear whether this relational description of M-ALC can be used to support the development of decision algorithms. In the next section we present an algorithm for testing the satisfiability of a restricted class of M-ALC–formulae. This algorithm is based on M-ALC’s original semantics, and not on the axiomatic description developed in this section. Soundness and termination of the algorithm are shown, but completeness remains an open problem.

3 The Satisfiability Test

In ALC a subsumption algorithm for concept terms is fully sufficient for computing the concept hierarchy in T-Boxes. The reason is that the concept equations are interpreted universally, and that the T-Boxes are deterministic and cycle free. This means no pairs c = d and c = d′ with d ≠ d′ are in the T-Box, and no chains c_{1} = d_{1}[c_{2}], …, c_{n} = d_{n}[c_{1}] are in the T-Box. With this restriction, all defined concepts in a concept term can be expanded with their definition prior to the subsumption test.

In the general case where modal concept equations m(c = d) either hold everywhere, or at some point only, or at one point in some dimensions and everywhere in others, this is no longer possible. A quite complex specification and control mechanism for the application of concept equations would be necessary, which is out of the scope of this paper. Therefore we only present a satisfiability algorithm for concept terms (which is in fact a general theorem prover for the modal logic M-ALC).

The algorithm we shall present works only for the restricted serial case where no [...]-operators occur in the role terms. The following example demonstrates the expressive power the unrestricted language has. Assume that we have only one dimension, and that the object o is an element of the concept term [[p]q]c ∧ [p]⊥. The term [p]⊥ (which is also allowed in the restricted case) forces the set of p-fillers of o to be empty. This in turn means that o is connected with all objects of the domain by the role term [p]q (which is not allowed in the restricted case). Because o is also an element of [[p]q]c this implies that all objects have to be in c. This shows that concept terms of M-ALC can be used to simulate general concept equations of the form c = ⊤ where c is a complex concept term. As mentioned in the introduction, general concept equations are very hard to handle algorithmically. If M-ALC terms are assumed to satisfy the seriality restriction concept equations can no longer be expressed. In the following we assume that all concept terms we consider are restricted serial.

In the satisfiability algorithm we assume that all concept terms are in negation normal form, i.e., negation symbols occur only in front of the atomic names. The following rules transform a given concept term into an equivalent term in negation normal form:

\begin{matrix}¬⊤  → & ⊥ & ¬⊥ → & ⊤ \\ ¬¬ϕ  → & ϕ & ¬[p]ϕ → & ⟨p⟩¬ϕ \\ ¬(ϕ ∨ ψ) → & ¬ϕ ∧ ¬ψ & ¬⟨p⟩ϕ → & [p]¬ϕ \\ ¬(ϕ ∧ ψ) → & ¬ϕ ∨ ¬ψ & ¬[p]^{+}ϕ → & ⟨p⟩¬ϕ ∨ [p]⊥ \end{matrix}

In order to be as close to the semantics as possible, we write the satisfiability test as a labelled deductive system [9]. The control structure, however, is a tableau expansion. Each data item is a pair l⃗: ϕ where l⃗ = (l_{1}, …, l_{n}) consists of constant symbols generated during the expansion of the tableau. The label l⃗ is the syntactic counterpart of the ‘actual world tuple’ d⃗ in an interpretation. That means l⃗: ϕ describes ϕ in the context l⃗. Here ϕ may be a concept term or a role term with an argument. The expression l⃗ : p : a for example means that a is a p-successor of l_{dim(p)}. The constraint systems that are generated by our satisfiability algorithm will always have a specified initial label l⃗_{0}. The algorithm calls itself recursively with ‘negated’ role terms \overline{p} in role constraints. The intended interpretation of \overline{p} is simply as complement: ℑ(\overline{p})(d⃗) = D_{dim(p)} \ ℑ(p)(d⃗). Since we must avoid [...]-operators in the role terms, the rules for building negation normal form are more complex for role terms than they are for concept terms. These rules are not applied in a preprocessing step. Instead, they are integrated into the satisfiability algorithm.

The rules for building negation normal forms of role terms generate so-called role terms with negation, which are slightly more general than simple negated role terms: if p and q are role terms (without negation) then \overline{p}, [p]^{+}\overline{q}, and ⟨p⟩\overline{q} are role terms with negation. The dimension of a role term with negation is just the dimension of the corresponding role term without negation: dim(\overline{p}) = dim(p), dim([p]^{+}\overline{q}) = dim([p]^{+}q), and dim(⟨p⟩\overline{q}) = dim(⟨p⟩q). In the following, the expression ‘role term’ will always mean a role term with or without negation. Since the negation occurs only in a very restricted setting in such terms (in particular, not inside of box or diamond operators), allowing for such terms does not mean that we introduce general role negation.

More formally, the rules of the satisfiability algorithm work on so-called constraint systems, which are defined as follows.

Definition 3.1 For an n-dimensional M-ALC language, constraints are built from constant symbols (points), n-tuples of constant symbols (labels), and role and concept terms. Each constant symbol has a dimension between 1 and n, and it may occur in a label as i–th component only if its dimension is i.

A role constraint is a triple l⃗ : p : a, where l⃗ is a label, p is a role term (with or without negation), and a is a point of dimension dim(p). A concept constraint is a tuple l⃗ : c consisting of a label l⃗ and a concept term c. A constraint system is a set of role constraints and concept constraints. <

The constraints in one system will be interpreted conjunctively (i.e., all of them must be satisfied to satisfy the whole system), whereas sets of constraint systems will be interpreted disjunctively (i.e., only one of the systems must be satisfied to satisfy the whole set of systems).

The algorithm depends on a function d that, for a given point in a constraint system, measures its distance from the initial label l⃗_{0}, i.e., it counts with how many atomic steps l⃗: p : x or l⃗: \overline{p} : x (where p is a role name) it can be reached from the initial label. For general constraint systems, the notion of depth may depend on the path chosen to reach the point, and it may even be undefined if the point cannot be reached from the initial label.

Definition 3.2 For a role term p we define |p| to be the number of occurrences of role names in p. For a constraint set Γ with initial label l⃗_{0} = (l_{01}, …, l_{0n}) we define

• d(l_{0i}, Γ) = 0 for i = 1, …, n.

• d(l⃗, Γ) = max_{1≤i≤n}d(l_{i}, Γ).

• If n = d(l⃗, Γ) is already defined, and l⃗:p:b ∈ Γ is selected by some selection function for b then d(b, Γ) = n + |p|. <

It will be shown (see Lemma 4.2 below) that for the constraint systems generated by the satisfiability algorithm, this definition determines for every point and label in the system a unique depth (i.e., one that is independent of the selection function). We are now ready to formulate the algorithm. Because of the presence of disjunction in our language we will actually have to consider finite sets of constraint systems.

Definition 3.3 The satisfiability algorithm takes as input a restricted serial M-ALC concept term c_{0} in negation normal form. It then constructs an initial label l⃗_{0} and builds the constraint system {l⃗_{0}:c_{0}}. Then it calls the function apply-rules with the singleton set Δ_{0} = {{l⃗_{0}:c_{0}}}. This function iteratively applies the rules of Figure 2 to the constraint systems already obtained. It returns ‘unsatisfiable’ if the ∅-rule applies, and ‘satisfiable’ if the ⊤-rule applies. <

A small example shall illustrate how the algorithm works. In the one-dimensional case, the concept terms [⟨p⟩q]c and [p][q]c are equivalent. We prove that the second term subsumes the first by applying the satisfiability algorithm to [⟨p⟩q]c ∧ ¬[p][q]c.

The initial constraint set for this input term contains the constraint l_{0}:[⟨p⟩q]c ∧ ⟨p⟩⟨q⟩¬c. By an application of the ∧-rule one obtains the two constraints

(1) l_{0}:[⟨p⟩q]c and (2) l_{0}:⟨p⟩⟨q⟩¬c.

The ⟨⟩-rule, applied to (2), adds the constraints

(3) l_{0}:p:a and (4) a:⟨q⟩¬c.

The ⟨⟩-rule, applied to (4), adds

(5) a:q:b and (6) b:¬c.

Now d(b, Γ) = 2 = d(l_{0}, Γ)+|⟨p⟩q|. For this reason, we have to make a recursive call of the function apply-rules to determine whether the []^{∗}-rule fires for (1) and b.

In this recursive call we consider the constraints (3) and (5) together with the new negated role constraint l_{0}:\overline{⟨p⟩q}:b. An application of the \overline{⟨⟩}-rule yields two new systems, one with the additional constraint

(7) l_{0}:[p]^{+}\overline{q}:b,

and the other with the additional constraint l_{0}:[p]⊥. In the following we restrict our attention to the first system. (The alternative l_{0}:[p]⊥ also leads to ‘unsatisfiable.’) Now the []^{∗}-rule becomes applicable for (7) and a. In fact, the recursive call of apply-rules with the constraint (3) and the new negated role constraint (8) l_{0}:\overline{p}:a immediately returns unsatisfiable. Application of the []^{∗}-rule for (7) and a yields the new constraint (9) a:\overline{q}:b, which clashes with (5). Thus the first recursive call also yields unsatisfiable.

This shows that in our original system the []^{∗}-rule can fire for (1) and b. From this we get (10) b:c, and thus a clash with (6).

4 Proof of Termination and Soundness

First, it will be shown that, for constraint systems generated by the algorithm, the depth function is always uniquely defined (i.e., independent of the selection function). In addition, the depth of all points and labels is bounded by a positive integer, which depends linearly on the size of the input term.

To define an appropriate bound on the depth of all points and labels occurring in a constraint system generated by the algorithm, we extend the notion of length of a role term to concept terms and expressions of the form p:a.

Definition 4.1 For concept names c and role names p we define |c| =^{def} |p| =^{def} 1. Now assume that a is a point, q is a role term without negation, e, f are concept terms, and ϕ is a concept term or an expression of the form q:a.

1. |¬c| =^{def} |c| and |\overline{q}| =^{def} |q|.

2. |e ∨ f| =^{def} |e ∧ f| =^{def} max{|e|, |f|}.

3. |[q]^{∗}ϕ| =^{def} |⟨q⟩ϕ| =^{def} |p| + |ϕ|.

4. |q:a| =^{def} |q|.

For a constraint system Γ and a label l⃗ in Γ we define

m(l⃗, Γ) =^{def} max{|ϕ| | l⃗:ϕ ∈ Γ}

as the length of l⃗ in Γ. <

Lemma 4.2 Let c_{0} be a concept term of length |c_{0}| = n_{0}, and assume that the function apply-rules is called with the singleton set {Γ_{0}}, where Γ_{0} = {l⃗_{0}:c_{0}}.

1. The depths of points and labels is uniquely defined, and it remains invariant during the execution of the function apply-rules.

2. For any constraint system Γ generated during the execution of apply-rules and any label l⃗ in

Γ, we have d(l⃗, Γ) + m(l⃗, Γ) ≤ n_{0}. Proof: by induction on the number of rule applications.

In the initial state there is only the label l⃗_{0}, and no points other than the ones occurring in l⃗_{0}. For these the first part is obviously true: their depth is uniquely defined to be zero, and thus d(l⃗_{0}, Γ_{0}) = 0. In addition, we have m(l⃗_{0}, Γ_{0}) = |c_{0}| = n_{0}, which shows that the second part of the lemma is true as well.

Obviously, an application of the ∧- or ∨-rule does not change the depth of points and labels, and it is easy to see that this also holds for the length of labels.

The two rules dealing with negated role terms are also unproblematic. We restrict our attention to the \overline{[]^{+}}-rule. (The other rule can be treated analogously.) In the first alternative, the \overline{[]^{+}}-rule introduces a new role constraint l⃗:⟨p⟩\overline{q}:a. Since the system already contains the constraint l⃗:\overline{[p]^{+}q}:a, which satisfies |\overline{[p]^{+}q}| = |⟨p⟩\overline{q}|, this additional constraint neither changes the depth of a nor the length of l⃗. In the second alternative, the rule adds the constraint l⃗:[p]⊥. This new constraint does not change the length of l⃗. The reason is that the system already contains the constraint l⃗:\overline{[p]^{+}q}:a, which satisfies |\overline{[p]^{+}q}| ≥ |p| + 1 = |[p]⊥|.

Thus the only remaining cases in the induction step are the ⟨⟩- and the []^{∗}-rules. Assume that Γ′ is obtained from Γ by application of such a rule.

(1) First, let us consider the ⟨⟩-rule. In this case, we may without loss of generality assume that Γ contains l⃗:⟨p⟩ϕ and Γ′ = Γ ∪ {l⃗:p:a, l⃗[i/a]:ϕ} where i = dim(p). (The case where Γ contains l⃗:[p]^{+}ϕ can be treated in exactly the same way.) The interesting case is where ϕ is a role constraint, i.e., ϕ is of the form q:a′. (The case where ϕ is a concept constraint is similar, but easier.)

(1.1) To prove the first part of the lemma, we show that in Γ′ the old constants (i.e., constants different from a) have a unique depth, which is identical to their depth in Γ. This is done by induction on the depth of these constants in Γ.

The only constants of depth 0 in Γ are the components of the tuple l⃗_{0}. In fact, any other constant b must have been introduced by a ⟨⟩-rule. Thus there exists a role constraint of the form g⃗:r:b in Γ, which shows that d(b, Γ) ≥ |r| ≥ 1. For the components of l⃗_{0} we have the unique depth d(l⃗_{0i}, Γ′) = 0 = d(l⃗_{0i}, Γ′) by definition, and this coincides with the depth they have in Γ.

Let b be a constant of depth greater than 0. First, assume that b ≠ a′. We know that there exists a role constraint g⃗:r:b, and

(∗) d(b, Γ) = d(g⃗, Γ) + |r|.

In addition, for any other role constraint g′:r′:b ∈ Γ, we also have

(∗∗) d(b, Γ) = d(g′, Γ) + |r′|,

by our induction assumption on Γ. From the equations (∗) and (∗∗) one can deduce that the components of g⃗ and g′ have a depth (in Γ) that is smaller than the one of b. For this reason, we know d(g⃗, Γ) = d(g⃗, Γ′) and d(g′, Γ) = d(g′, Γ′) by induction. This, together with the equations (∗) and (∗∗) shows that in Γ′ both role constraints give us the same depth for b, namely the one b already had in Γ. Since we have assumed b ≠ a′, the system Γ′ does not contain new role constraints for b.

Now assume that b = a′. As above, one can show that the old role constraints for a′ provide us with the same depth for a′ as in Γ. Note that the constraint l⃗:⟨p⟩q:a′ ∈ Γ shows that d(a′, Γ) = d(l⃗, Γ) + |p| + |q|.

It remains to be shown that the new constraint l⃗[i/a]:q:a′ does not give a different result. To determine the depth induced by this constraint, we have to find out what the depth of the new constant a is in Γ′. There is exactly one role constraint for a in Γ′, namely l⃗:p:a. Because l⃗:⟨p⟩q:a′ ∈ Γ, we know that the components of l⃗ have a smaller depth than a′ in Γ. By induction, we thus know that d(l⃗, Γ′) = d(l⃗, Γ) is uniquely defined. But then d(a, Γ′) = d(l⃗, Γ′)+|p| = d(l⃗, Γ)+|p| is also uniquely defined. Obviously, this implies that d(l⃗[i/a], Γ′) = d(a, Γ′) since a is the component of maximal depth in l⃗[i/a].

The constraint l⃗[i/a]:q:a′ induces for a′ in Γ′ the depth d(l⃗[i/a], Γ′) + |q|. However, we know that this is equal to d(a, Γ′) + |q| = d(l⃗, Γ′) + |p| + |q| = d(l⃗, Γ) + |p| + |q| = d(a′, Γ), as was to be shown.

(1.2) Now let us turn to the second part of the lemma. First, we consider the length of old labels, i.e., labels not containing a. Obviously, l⃗ is the only such label having an additional constraint in Γ′. But this new constraint, l⃗:p:a, cannot increase the length of l⃗ since Γ already contains l⃗:⟨p⟩ϕ, and |⟨p⟩ϕ| ≥ |p| = |p:a|. Thus, for all old labels g⃗ we have m(g⃗, Γ′) = m(g⃗, Γ), and since the depth of these labels also coincides in Γ and Γ′ (by (1.1)), the second part of the lemma is satisfied for g⃗ by induction.

The only new label in Γ′ is l⃗[i/a], and its only constraint is l⃗[i/a]:ϕ. By induction, we know

n_{0} ≥ m(l⃗, Γ) + d(l⃗, Γ),

and in (1.1) we have seen that

d(l⃗[i/a], Γ′) = d(a, Γ′) = d(l⃗, Γ′) + |p| = d(l⃗, Γ) + |p|.

Since Γ contains the constraint l⃗:⟨p⟩ϕ, we obtain

m(l⃗, Γ) ≥ |⟨p⟩ϕ| = |p| + |ϕ|,

and since l⃗[i/a]:ϕ is the only constraint for l⃗[i/a], we also have

m(l⃗[i/a], Γ′) = |ϕ|.

These facts imply that n_{0} ≥ m(l⃗, Γ) + d(l⃗, Γ) ≥ |p| + |ϕ| + d(l⃗, Γ) = d(l⃗[i/a], Γ′) + m(l⃗[i/a], Γ′), as was to be shown.

(2) Second, we consider an application of the []^{∗}-rule. In this case, Γ contains the constraint l⃗:[p]^{∗}ϕ and Γ′ = Γ ∪ {l⃗[i/a]:ϕ}. Since the rule applies to a, we know that d(a, Γ) = d(l⃗, Γ) + |p|.

(2.1) To prove the first part of the lemma, we show by induction on the depth of constants in Γ that all constants have the same depth in Γ′ as they had in Γ. Again, the constants of depth 0 in Γ and Γ′ are exactly the components of the tuple l⃗_{0}.

The only new constraint in Γ′ is l⃗[i/a]:ϕ. If ϕ is not a role constraint, the depth of labels and constants is obviously not changed by its introduction. Thus assume that ϕ = q:a′. Since Γ contains the constraint l⃗:[p]^{∗}q:a′ we have d(a′, Γ) = d(l⃗, Γ) + |p| + |q|. Since we also know that d(a, Γ) = d(l⃗, Γ)+|p| this shows that a is of smaller depth than a′ in Γ. For this reason, we already know by induction that d(a, Γ′) = d(a, Γ) = d(l⃗, Γ) + |p| = d(l⃗, Γ′) + |p|. In particular, this means that d(l⃗[i/a], Γ′) = d(l⃗, Γ) + |p|.

The constraint l⃗[i/a]:q:a′ thus gives us d(l⃗, Γ) + |p| + |q| as depth of a′ in Γ′. This is just the depth of a′ in Γ. It is easy to see that the role constraints for a′ that were already present in Γ yield the same depth for a′ in Γ′ as they did in Γ.

(2.2) Finally, we show that the second part of the lemma holds in this case as well. Since the only new constraint in Γ′ is l⃗[i/a]:ϕ, the only label for which the length can change is l⃗[i/a]. If this does not happen, i.e., if m(l⃗[i/a], Γ) = m(l⃗[i/a], Γ′), then the second part of the lemma follows by induction and (2.1).

Thus assume that m(l⃗[i/a], Γ) < m(l⃗[i/a], Γ′). This means that the length m(l⃗[i/a], Γ′) must be equal to |ϕ|. From (2.1) we know that d(l⃗[i/a], Γ′) = d(l⃗, Γ) + |p|. Together, these to facts yield m(l⃗[i/a], Γ′) + d(l⃗[i/a], Γ′) = |ϕ| + |p| + d(l⃗, Γ). Since l⃗:[p]^{∗}ϕ is a constraint in Γ, we also know that m(l⃗, Γ) ≥ |ϕ| + |p|. Thus, we know m(l⃗[i/a], Γ′) + d(l⃗[i/a], Γ′) ≤ m(l⃗, Γ) + d(l⃗, Γ), and by induction, this is smaller or equal n_{0}, which concludes the proof of the lemma. <

We have to show that the system Γ′′ for which the satisfiability algorithm is recursively called in the []^{∗}-rule satisfies the lemma as well.

Lemma 4.3 Let c_{0} be a concept term of length |c_{0}| = n_{0}, and assume that the function applyrules is called with the singleton set {Γ_{0}} where Γ_{0} = {l⃗_{0}:c_{0}}. Let Γ be a constraint system generated during the execution of apply-rules. Let l⃗:[p]^{∗}ϕ ∈ Γ, and a be a constant in Γ with d(a, Γ) = n = d(l⃗, Γ) + |p|. We consider the system

Γ′′ =^{def} \{l⃗′:q:b | d(b, Γ) ≤ n\} ∪ \{l⃗:\overline{p}:a)\}.

1. The depth of all constants in Γ′′ is uniquely defined, and it coincides with their depth in Γ.

2. d(l⃗, Γ′′) + m(l⃗, Γ′′) ≤ n_{0}.

Proof: by induction on the depth of the constants in Γ. The components of l⃗_{0} are the only constants of depth 0 in Γ. By definition, they also have depth 0 in Γ′′.

Let b be a constant of depth greater than 0 in Γ. There is a constraint g⃗:q:b in Γ, and d(b, Γ) = d(g⃗, Γ)+|q|. If b occurs in Γ′′ then this depth is not larger than n. For this reason, the components of g⃗ are of depth smaller than n, and thus also occur in Γ′′. By induction, we know d(g⃗, Γ′′) = d(g⃗, Γ). This shows that the constraint g⃗:q:b yields the same depth for b in Γ′′ as it did in Γ.

If b ≠ a, we are finished (since the above argument applies to any constraint of the form g⃗:q:b that is both in Γ and Γ′′). Otherwise, we have to take into account that for a we have the new constraint l⃗:\overline{p}:a. But this gives us the depth d(l⃗, Γ′′) + |p| for a. By induction, we know that d(l⃗, Γ′′) = d(l⃗, Γ), and by our assumption on a, d(l⃗, Γ) + |p| is the depth of a in Γ. Thus we have proved the first part of the lemma.

For the second part, we note that for g⃗ ≠ l⃗ we have m(g⃗, Γ′′) ≤ m(g⃗, Γ). This is so because g⃗ does not have more constraints in Γ than it has in Γ′′. For l⃗, we also have m(l⃗, Γ′′) ≤ m(l⃗, Γ). In fact, the only new constraint is l⃗:\overline{p}:a, and we know m(l⃗, Γ) ≥ |p| (since Γ contains the constraint l⃗:[p]^{∗}ϕ). <

The fact that labels are of bounded depth plays an important role in the proof of termination.

Theorem 4.4 The satisfiability algorithm described above terminates. <

Before we can prove the theorem we have to introduce some notation. We say that a constraint system Γ′ is a descendant of the constraint system Γ iff one of the following two conditions holds:

• Γ′ is obtained from Γ by applying the ∧-, ∨-, \overline{[]^{+}}-, \overline{⟨⟩}-, ⟨⟩-, or []^{∗}-rule.

• Γ is a system for which applicability of the []^{∗}-rule for a constraint l⃗:[p]^{∗}ϕ is tested by recursively calling the function apply-rules with input Γ′.

Assume that the algorithm does not terminate. It is easy to see that this implies the existence of an infinite chain Γ_{0}, Γ_{1}, … of constraint systems such that Γ_{i+1} is a descendant of Γ_{i}. To prove that this leads to a contradiction, we define a mapping Ψ of constraint systems into a set Q, which will be equipped with a well-founded strict partial ordering ≫. Since the ordering is well-founded, there cannot be an infinitely decreasing chain Ψ(Γ_{0}) ≫ Ψ(Γ_{1}) ≫ ⋯ of constraint systems. Thus it will be sufficient to show that Ψ(Γ) ≫ Ψ(Γ′) whenever Γ′ is a descendant of Γ.

The elements of the set Q will have a rather complex structure. They are 2-tuples where the first component is a nonnegative integer. The second component is a finite multiset of 4-tuples. Each component of these 4-tuples is either a finite multiset of nonnegative integers (for the third and fourth component) or a nonnegative integer (for the first and second component). Multisets are like sets, but allow for multiple occurrences of identical elements. For example, {2, 2, 2} is a multiset that is distinct from the multiset {2}. A given ordering on a set T can be used to define an ordering on the finite multisets over T. In this ordering, a finite multiset M is larger than a finite multiset M′ iff M′ can be obtained from M by replacing one or more elements in M by any finite number of elements taken from T, each of which is smaller than one of the replaced elements. For example, {2, 2, 2} is larger than {2} and {2, 2, 1, 1, 0}. In [6] it is shown that the induced ordering on finite multisets over T is well-founded if the original ordering on T is so.

The nonnegative integer components of our 4-tuples are compared with respect to the usual ordering on integers, and the finite multiset components by the multiset ordering induced by this ordering. The whole 4-tuples are ordered lexicographically from left to right, i.e., (c_{1}, ..., c_{4}) is larger than (c′_{1}, ..., c′_{4}) iff there exists i, 1 ≤ i ≤ 4, such that c_{1} = c′_{1}, ..., c_{i−1} = c′_{i−1}, and c_{i} is larger than c′_{i}. Since the orderings on the components are well-founded, the lexicographical ordering on the tuples is well-founded as well. Finite multisets of these tuples are now compared with respect to the multiset ordering induced by this lexicographical ordering. Finally, the 2-tuples consisting of a nonnegative integer in the first component, and a multiset of 4-tuples in the second component are again ordered lexicographically from left to right. This is the well-founded ordering ≫ on Q mentioned above.

Before we can define the mapping Ψ from constraint systems to elements of Q, we need some more notation. For a concept term c in negation normal form we denote the number of ‘ ∧ ’ and ‘ ∨’ operators occurring in c by oas(c). For a role term p with negation, we denote the length of the over-lined part of p by nol(p).

Definition 4.5 Let c_{0} be a concept term of length |c_{0}| = n_{0}, and assume that the function applyrules is called with the singleton set {{l⃗_{0}:c_{0}}}. Let Γ be a constraint system generated during the execution of apply-rules. Then Ψ(Γ) =^{def} (Ψ_{1}(Γ), Ψ_{2}(Γ)). The first component of this 2-tuple is defined as

Ψ_{1}(Γ) =^{def} max{d(l⃗, Γ) + m(l⃗, Γ) | l⃗ is a label occurring in Γ}.

The second component, Ψ_{2}(Γ), is the multiset that contains for each label l⃗ occurring in Γ a 4-tuple ψ(l⃗, Γ) defined as follows:

1. The first component of ψ(l⃗, Γ) is the integer k_{1} =^{def} n_{0} − d(l⃗, Γ). By Lemma 4.2, k_{1} is welldefined and nonnegative.

2. The second component of ψ(l⃗, Γ) is the number of constraints g⃗:[p]^{∗}ϕ in Γ that satisfy

• l⃗ = g⃗[i/a],

• d(a, Γ) = d(g⃗, Γ) + |p|, and

• l⃗:ϕ ∉ Γ.

Note that in this case d(l⃗, Γ) = d(a, Γ) > d(g⃗, Γ).

3. The third component of ψ(l⃗, Γ) is the multiset that consists of all numbers oas(c ∧ d) (resp. oas(e ∨ f), nol(\overline{p})) such that l⃗:c ∧ d (resp. l⃗:e ∨ f, l⃗:\overline{p}:a) is in Γ, and the ∧-rule (resp. ∨-rule, \overline{⟨⟩}- or \overline{[]^{+}}) is still applicable to this constraint.

4. The fourth component of ψ(l⃗, Γ) is the multiset that consists of all numbers |p| such that l⃗:⟨p⟩ϕ or l⃗:[p]^{+}ϕ is in Γ, and the ⟨⟩-rule is still applicable to this constraint. < Lemma 4.6 Assume that Γ is a system for which applicability of the []^{∗}-rule for a constraint l⃗:[p]^{∗}ϕ is tested by recursively calling the function apply-rules with input Γ′. Then Ψ_{1}(Γ) ≫ Ψ_{1}(Γ′), and thus Ψ(Γ) ≫ Ψ(Γ′).

Proof: We have l⃗:[p]^{∗}ϕ ∈ Γ, and a constant a in Γ such that d(a, Γ) = n = d(l⃗, Γ) + |p|. The system Γ′ is defined as

Γ′ = \{g⃗:q:b | d(b, Γ) ≤ n\} ∪ \{l⃗:\overline{p}:a\}.

First, we show that for any label g⃗ in Γ′ we have d(g⃗, Γ′)+m(g⃗, Γ′) ≤ n. Let g⃗:q:b be the constraint for which |q:b| = m(g⃗, Γ′).

Assume that g⃗ is different from l⃗. By definition of Γ′ we know d(b, Γ) ≤ n, and in the proof of Lemma 4.3 we have seen that d(b, Γ) = d(b, Γ′). In addition, the presence of g⃗:q:b in Γ′ shows that d(b, Γ′) = d(g⃗, Γ′) + |q|. Thus d(g⃗, Γ′) + m(g⃗, Γ′) = d(g⃗, Γ′) + |q:b| = d(g⃗, Γ′) + |q| = d(b, Γ′) = d(b, Γ) ≤ n.

If g⃗ = l⃗, then the additional constraint l⃗:\overline{p}:a must be taken into account. Since d(a, Γ) = n = d(l⃗, Γ) + |p| and |\overline{p}| = |p|, however, the same argument as above can be used.

Second, we show that d(l⃗, Γ) + m(l⃗, Γ) > n, which obviously concludes the proof of the lemma. We know that l⃗:[p]^{∗}ϕ is in Γ, and that d(l⃗, Γ) = n−|p|. But the first fact implies m(l⃗, Γ) ≥ |[p]^{∗}ϕ| > |p| since |ϕ| must be at least 1. <

The proof of the second part of Lemma 4.2 shows that Ψ_{1}(Γ) is not changed by applying an ∧-, ∨-, \overline{⟨⟩}-, \overline{[]^{+}}-, ⟨⟩-, or []^{∗}-rule. Thus, if Γ′ is a descendant of Γ obtained by applying one of these rules it is sufficient to show that the second component of the tuple Ψ(Γ) = (Ψ_{1}(Γ), Ψ_{2}(Γ)) decreases.

Lemma 4.7 If Γ′ is obtained from Γ by application of the ∧-rule then Ψ_{2}(Γ) ≫ Ψ_{2}(Γ′).

Proof: Assume that the ∧-rule is applied to the constraint l⃗:c ∧ d.

(1) Consider the tuple corresponding to l⃗. As shown in Lemma 4.2 we have d(l⃗, Γ′) = d(l⃗, Γ), and thus the first component of ψ(l⃗, Γ′) coincides with the first component of ψ(l⃗, Γ).

The second component of the tuple cannot increase. In fact, this could only happen if a constraint of the form g⃗:[p]^{∗}ϕ is added for a label g⃗ with d(l⃗, Γ) > d(g⃗, Γ). But the only label for which constraints are added is l⃗.

The third component of ψ(l⃗, Γ) decreases: oas(c ∧ d) is removed from this multiset, and possible replaced by the smaller elements oas(c) and oas(d) (if these terms have a top-level conjunction or disjunction).

(2) Consider the tuple corresponding to a label g⃗ different from l⃗. Since Γ and Γ′ contain the same constraints for g⃗, the only component that may change is the second one. This may happen if Γ′ contains a new constraint of the form l⃗:[p]^{∗}ϕ. But this new constraint can only increase the tuple of g⃗ if d(l⃗, Γ) < d(g⃗, Γ). In this case, the first component of ψ(l⃗, Γ) is larger than the first component of ψ(g⃗, Γ′). Assume that g⃗_{1}, …, g⃗_{k} are the labels for which such an increase of the tuple takes place. Then the multiset Ψ_{2}(Γ′) can be obtained from Ψ_{2}(Γ) by first removing all tuples ψ(g⃗_{i}, Γ), and then replacing ψ(l⃗, Γ) by the smaller tuples ψ(l⃗, Γ′), ψ(g⃗_{1}, Γ′), …, ψ(g⃗_{k}, Γ′). Obviously, this shows that Ψ_{2}(Γ) ≫ Ψ_{2}(Γ′). <

Lemma 4.8 If Γ′ is obtained from Γ by application of the ∨-rule then Ψ_{2}(Γ) ≫ Ψ_{2}(Γ′).

Proof: very similar to the one for the ∧-rule. <

Lemma 4.9 If Γ′ is obtained from Γ by application of the \overline{[]^{+}}-rule then Ψ_{2}(Γ) ≫ Ψ_{2}(Γ′).

Proof: Assume that the \overline{[]^{+}}-rule is applied to the constraint l⃗:\overline{[p]^{+}q}:a. We have to consider two cases: Γ′ may contain the additional constraint l⃗:⟨p⟩\overline{q}:a or l⃗:[p]⊥.

(1) First, we consider the case where Γ′ = Γ ∪ \{l⃗:⟨p⟩\overline{q}:a\}.

(1.1) Consider the tuple corresponding to l⃗. The proof of Lemma 4.2 shows that ψ(l⃗, Γ) and ψ(l⃗, Γ′) coincide in the first component. The second component of the tuple does not increase since there are no constraints added to labels of depth smaller than l⃗. The third component of ψ(l⃗, Γ) decreases: nol(\overline{[p]^{+}q}) is removed from this multiset, and no new tuple added (since the new role constraint does not have the negation on top level).

(1.2) Consider the tuple corresponding to a label g⃗ different from l⃗. Since Γ and Γ′ contain the same constraints for g⃗, we can apply the same argument as in the corresponding case in the proof of Lemma 4.7.

(2) Second, we consider the case where Γ′ = Γ ∪ {l⃗:[p]⊥}. Here the same arguments as in the first case can be employed. <

Lemma 4.10 If Γ′ is obtained from Γ by application of the \overline{⟨⟩}-rule then Ψ_{2}(Γ) ≫ Ψ_{2}(Γ′).

Proof: very similar to the one for the \overline{[]^{+}}-rule. <

Lemma 4.11 If Γ′ is obtained from Γ by application of the ⟨⟩-rule then we have Ψ_{2}(Γ) ≫ Ψ_{2}(Γ′).

Proof: Without loss of generality we consider the case where Γ contains a constraint of the form l⃗:⟨p⟩ϕ, and Γ′ = Γ ∪ {l⃗:p:a, l⃗[i/a]:ϕ}.

(1) Consider the tuple corresponding to l⃗. Again, the proof of Lemma 4.2 shows that the first components of ψ(l⃗, Γ′) and ψ(l⃗, Γ) are the identical.

The second component of the tuple does not increase. The reason is that the only labels for which constraints are added are l⃗ and l⃗[i/a]. But these labels have a depth that is not smaller than the depth of l⃗. The second component of the tuple, however, can only increase if a constraint of the form g⃗:[p′]^{∗}ϕ′ is added for a label g⃗ of smaller depth.

The third component is not changed since the only new constraint for l⃗ is a role constraint without negation.^{4} Thus no concept constraints with top-level ‘ ∨ ’ or ‘ ∧ ’ are added for l⃗, and also no role constraints with negation.

The fourth component of the tuple decreases. In fact, |p| is removed from this multiset. If p is of the form ⟨q⟩r or [q]^{+}r then |q| is added to the multiset, but obviously |q| < |p|.

(2) Next, we consider the tuple of l⃗[i/a]. Since a is a new constant, this is a new tuple in Ψ_{2}(Γ′) (i.e., one that was not present in Ψ_{2}(Γ)). We know, however that d(l⃗[i/a], Γ′) = d(l⃗, Γ′) + |p| = d(l⃗, Γ) + |p|, and thus the first component of this tuple is smaller than the one of ψ(l⃗, Γ).

(3) Finally, consider the tuple corresponding to a label g⃗ different from l⃗ and l⃗[i/a]. Obviously, the changes for the constraints on l⃗ and l⃗[i/a] can only increase this tuple in the second component. But then the depth of g⃗ must be larger than the one of l⃗,^{5} which means that the first component of the tuple corresponding to g⃗ is smaller than the first component of ψ(l⃗, Γ). <

Lemma 4.12 If Γ′ is obtained from Γ by application of the []^{∗}-rule then Ψ_{2}(Γ) ≫ Ψ_{2}(Γ′).

Proof: We have a constraint of the form l⃗:[p]^{∗}ϕ in Γ, and Γ′ = Γ ∪ {l⃗[i/a]:ϕ}.

(1) Consider the tuple corresponding to l⃗. Since there are no new constraints on l⃗ in Γ′, the only component in which this tuple could increase is the second one. But this cannot be the case since the label l⃗[i/a] (which is the only one with a new constraint) is of larger depth than the label l⃗.

(2) Next, we consider the tuple corresponding to l⃗[i/a]. By Lemma 4.2 its first component does not change.

The second component of the tuple decreases. In fact, the constraint l⃗:[p]^{∗}ϕ is no longer counted since l⃗[i/a]:ϕ has been added. Since labels g⃗ of smaller depth than the one of l⃗[i/a] do not obtain new constraints, this really results in a decrease of the second component.

4Inside of diamond-operators we do not allow the use of negated roles.

5Note that the depth of l⃗[i/a] is larger than the depth of l⃗.

(3) Finally, consider the tuple corresponding to a label g⃗ different from l⃗ and l⃗[i/a]. The additional constraint on l⃗[i/a] can only increase this tuple in the second component. But then the depth of g⃗ must be larger than the one of l⃗[i/a], which means that the first component of the tuple corresponding to g⃗ is smaller than the first component of ψ(l⃗[i/a], Γ). <

This completes the proof of termination. When the algorithm has terminated it returns either ‘unsatisfiable,’ if all constraint systems have been eliminated by the ⊥-rule since they contain clashes, or it returns ‘satisfiable,’ if there remains at least one system without a clash. The next theorem shows that in the first case the answer ‘unsatisfiable’ is correct.

Theorem 4.13 Let c_{0} be a concept term of M-ALC, and assume that the function apply-rules is called with the singleton set {{l⃗_{0}:c_{0}}}. If it returns ‘unsatisfiable’ then the input term c_{0} is in fact unsatisfiable. <

In order to prove the theorem we have to extend the notion of a model to constraint systems.

Definition 4.14 (Semantics of Constraint Systems) Let Γ be a constraint system. An interpretation of Γ is an interpretation of the underlying M-ALC-language that, in addition,

• assigns an element of D_{i} to each constant of dimension i occurring in Γ,

• interprets over-lined role terms \overline{p} of dimension i as ℑ(\overline{p})(d⃗) = D_{i} \ ℑ(p)(d⃗).

More general role terms with negation are interpreted according to the semantics for box- and diamond-operators on roles given in Definition 1.2. The interpretation of a label l⃗ = (l_{1}, …, l_{n}) is ℑ(l⃗) = (ℑ(l_{1}), …, ℑ(l_{n})).

The interpretation ℑ satisfies the concept constraint l⃗:c iff ℑ(l⃗) ∈ ℑ(c), and it satisfies the role constraint l⃗:p:a iff ℑ(a) ∈ ℑ(p)(ℑ(l⃗)). It is a model of Γ iff it satisfies all constraints in Γ. The interpretation ℑ is a model of a set Δ of constraint systems iff it is a model of one of the systems in Δ. A constraint system (set of constraint systems) is satisfiable iff it has a model. <

The following three lemmas show that application of rules keeps the satisfiability of sets of constraint systems unchanged.

Lemma 4.15 If the application of the ∨-, \overline{⟨⟩}-, or \overline{[]^{+}}-rule replaces the system Γ by Γ_{1} and Γ_{2} then Γ is satisfiable iff Γ_{1} or Γ_{2} is satisfiable.

Proof: (1) This is rather obvious for the ∨-rule.

(2) Thus, consider the \overline{[]^{+}}-rule. This means that Γ contains the constraint l⃗:\overline{p}:a for p = [q]^{+}r, and Γ_{1} = Γ ∪ \{l⃗:⟨q⟩\overline{r}:a\} whereas Γ_{2} = Γ ∪ \{l⃗:[q]⊥\}.

The ‘if’ direction of the lemma is trivially satisfied since both Γ_{1} and Γ_{2} are supersets of Γ. To show the ‘only-if’ direction of the lemma, we assume that the interpretation ℑ satisfies the

constraint l⃗:\overline{p}:a, i.e., ℑ(a) ∉ ℑ(p)(ℑ(l⃗)). Since p = [q]^{+}r this means that either ℑ(q)(ℑ(l⃗)) = ∅, or this set is non-empty but contains an element x such that ℑ(a) ∉ ℑ(r)(x). In the first case, ℑ satisfies the constraint l⃗:[q]⊥, and thus Γ_{2} is satisfiable. In the second case, ℑ(a) ∈ ℑ(\overline{r})(x), and thus ℑ(a) ∈ ℑ(⟨q⟩\overline{r})(ℑ(l⃗)). This shows that ℑ satisfies Γ_{1}.

(3) The \overline{⟨⟩}-rule can be treated similarly. <

Lemma 4.16 If the application of the ∧-, ⟨⟩-, or []^{∗}-rule replaces the system Γ by Γ′ then Γ is satisfiable iff Γ′ is satisfiable.

Proof: The proof is obvious for the ∧- and the ⟨⟩-rule.

Thus consider the []^{∗}-rule. If Γ′ is satisfiable then Γ is satisfiable as well since Γ is a subset of Γ′. To prove the other direction it obviously suffices to show the following property:

If the recursive call of the function apply-rules returns ‘unsatisfiable’ then we have ℑ(a) ∈ ℑ(p)(ℑ(l⃗)) for all models ℑ of Γ.

Assume to the contrary that ℑ is a model of Γ such that

(∗) ℑ(a) ∉ ℑ(p)(ℑ(l⃗)).

Obviously, ℑ is a model of the subset {l⃗′:q:b | d(b, Γ) ≤ n} of Γ. Because of the assumption (∗), ℑ satisfies the constraint l⃗:\overline{p}:a as well. This means that the recursive call returns ‘unsatisfiable’ even though the input system is satisfiable. By induction, we can assume, however, that Theorem 4.13 already holds for this smaller system. <

Lemma 4.17 If the ⊥-rule applies to a constraint system Γ then Γ is unsatisfiable.

Proof: obvious by the semantics for concept and role negation and for ⊥. <

Now we can prove Theorem 4.13. Assume that the concept term c_{0} is satisfiable, and that we call the function apply-rules with input {{l⃗_{0}:c_{0}}}. Since c_{0} is satisfiable, the constraint system Γ_{0} = {l⃗_{0}:c_{0}} is satisfiable as well. Let Δ be a set of constraint systems obtained by repeatedly applying the rules of Figure 2 to this input. Since Γ_{0} is satisfiable, the Lemmas 4.15, 4.16, and 4.17 obviously imply that there exists a constraint systems in Δ that is satisfiable. For this reason, Δ cannot be empty, which shows that the ∅-rule cannot be applied to Δ. This completes the proof of Theorem 4.13.

Unfortunately, we did not succeed in showing the opposite direction of the statement in Theorem 4.13, but we strongly conjecture that it holds. Since subsumption is reduced to unsatisfiability this means that we have presented a sound (but possibly incomplete) algorithm for subsumption in M-ALC. In order to prove the conjecture it is sufficient to show that a constraint to which the ⊤-rule applies is in fact satisfiable. The main problem in the proof is to show that the []^{∗}-rule is complete, i.e., that that the restrictions on its applicability are not too severe.

In the above proofs we have never used the restriction that role terms must not contain [...]- operators. If this restriction did not hold, however, the algorithm would obviously be incomplete. This is illustrated by the following example, which is a modification of an example given in Section 3. We consider a 1-dimensional M-ALC language, and are interested in the satisfiability of the concept term

c_{0} = [[p]q]c ∧ [p]⊥ ∧ ¬c.

Note that the first conjunct of this term is not restricted serial. In Section 3 we have shown the following fact: If ℑ is an interpretation such that ℑ([[p]q]c ∧ [p]⊥) ≠ ∅ then any object o in the carrier set of ℑ is an element of ℑ(c). Obviously, this implies that c_{0} is unsatisfiable.

Our algorithm, however, does not recognize the unsatisfiability of c_{0}. The algorithm starts with the constraint system {l_{0}:c_{0}}. By applying the ∧-rule twice we obtain the system Γ = {l_{0}:[[p]q]c, l_{0}:[p]⊥, l_{0}:¬c}. At this point, none of the rules other than the ⊤-rule can be applied. In fact, the only possible rule could be the []^{∗}-rule. But there is no constant a of depth d(l_{0}, Γ) + |p| or d(l_{0}, Γ) + |p| + |q| in Γ.

Completeness of the satisfiability algorithm for the case of restricted serial terms is still an open problem. We close this section by showing that the algorithm is complete in the case where all role terms are atomic, i.e., role names are the only role terms occurring in the concept term to be tested for satisfiability.

In order to see this we first reconsider the []^{∗}-rule under this restriction. Since all roles are atomic it is easy to see that

apply-rules(\{\{l⃗′:q:b ∈ Γ | d(b, Γ) ≤ n\} ∪ \{l⃗:\overline{p}:a)\}\}) = ‘unsatisfiable’

iff l⃗:p:a is in Γ. In fact, since all role terms are atomic, the only rule that may apply is the ⊥-rule, and this is only possible if l⃗:p:a is in Γ. For this reason, the []^{∗}-rule can be replaced by the simpler rule of Figure 3.

Obviously, this also means that we can dispense with the \overline{[]^{+}}- and the \overline{⟨⟩}-rule. Thus, we obtain an algorithm that is a simple multi–dimensional variant of the well-known satisfiability algorithm for ALC. This should not be surprising since in Section 2.1 we have shown that a concept term without compound role terms is satisfiability in one dimension if, and only if, it is satisfiable in n dimensions.

Termination and soundness of this algorithm is an immediate consequence of termination and soundness of the (more general) satisfiability algorithm for the restricted serial case. The proof of completeness for the case of atomic role terms is very similar to the proof for ALC. Assume that the ⊤-rule is applied to Γ, i.e., Γ is a constraint system to which no other rule applies. We show that Γ has a model.

Definition 4.18 Let Γ be a constraint system such that all role terms occurring in Γ are atomic role terms. The canonical interpretation ℑ^{Γ} is defined as follows:

• For all i, 1 ≤ i ≤ n, the carrier sets D_{i} consists of all constants of dimension i that occur in Γ.

• For all concept names c, the signature interpretation yields ℑ_{Σ}^{Γ}(c) = {l⃗ | l⃗:c ∈ Γ}.

• For all role names p and all labels l⃗, the signature interpretation yields ℑ_{Σ}^{Γ}(p)(l⃗) = {a | l⃗:p:a ∈ Γ}. <

Lemma 4.19 If Γ is a constraint system such that all role terms occurring in Γ are atomic role terms, and if the ⊤-rule applies to Γ, then ℑ^{Γ} is a model of Γ.

Proof: First, consider a constraint of the form l⃗:p:a. By definition, ℑ^{Γ} satisfies this constraint iff l⃗:p:a is in Γ. Thus, all role constraints of Γ are satisfied by ℑ^{Γ}.

Now, assume that l⃗:c ∈ Γ for a concept term c. By induction on the structure of c, we show that ℑ^{Γ} satisfies l⃗:c. If c is a concept name then this is the case by definition of the canonical interpretation. Now, assume that c is of the form [p]c′ where p is a role name of dimension i. (The other cases can be treated similarly.) We must show that ℑ^{Γ}, l⃗ ⊧ [p]c′. In order to see this, assume that there is a constant a of dimension i such that a ∈ ℑ^{Γ}(p)(l⃗). By definition of ℑ^{Γ}, this implies that l⃗:p:a ∈ Γ. Since the []^{∗}-rule is not applicable to Γ, we can deduce that l⃗[i/a]:c′ ∈ Γ, and thus induction yields ℑ^{Γ}, l⃗[i/a] ⊧ c′. To sum up, we have shown that ℑ^{Γ}, l⃗ ⊧ [p]c′. <

Now, assume that a system Γ is reached from {l⃗_{0}:c_{0}} by application of the rules of the satisfiability algorithm, and that the ⊤-rule applies to Γ. If all role terms occurring in c_{0} are atomic then Γ satisfies the assumption of the lemma. Since {l⃗_{0}:c_{0}} is a subset of Γ, we know that ℑ^{Γ} is also a model of l⃗_{0}:c_{0}. This shows that c_{0} is satisfiable.

Theorem 4.20 Let c_{0} be a concept term of M-ALC that contains only atomic role terms, and assume that the function apply-rules is called with the singleton set {{l⃗_{0}:c_{0}}}. If it returns ‘satisfiable’ then the input term c_{0} is in fact satisfiable. <

5 Independence of Some Dimensions

As mentioned in the introduction, it would often be desirable to have roles and concepts depend on only some of the dimensions. For example, assume that we have an object and a time dimension, and that the role future has dimension time. As defined until now, an interpretation ℑ may interpret future by an arbitrary function

ℑ_{Σ}(future):D⃗ → 2^{Dtime}.

Thus, if one considers two different individuals John and Mary (who are elements of D_{object}), and a time point t_{0} ∈ D_{time}, the future time points reached from the tuple (John,t_{0}) may differ from the future time points reached from (Mary,t_{0}). Considering this as a possibility may give rise to interesting philosophical discussion, but it does not agree with our usual understanding of time. With respect to this understanding, the role future should be independent of the dimension object.

In order to account for the fact that some roles (or concepts) may depend on only a subset of the set of all dimensions, we extend the syntax as follows.

Definition 5.1 An M-ALC language with dimension independence is an M-ALC language where, in addition to its dimension, dim(p), each role name p has a set of relevant dimensions, δ(p) ⊆ {1, …, n}, i.e., the set of dimensions it depends on. Accordingly, each concept name c is equipped with a set δ(c) ⊆ {1, …, n}. <

Before we can give a formal definition of what it means that concepts and roles depend on the relevant dimensions only, we must introduce one more piece of notation. Let D⃗ = D_{1} ×…×D_{n} be the Cartesian product of n non-empty sets, and let δ be a subset of {1, …, n}. For tuples d⃗, e⃗ ∈ D⃗ we define

d⃗ ≡_{δ} e⃗ iff d_{i} = e_{i} for all i ∈ δ.

Definition 5.2 An interpretation ℑ = (D⃗, ℑ_{Σ}) of an M-ALC language with dimension independence is an interpretation of the underlying M-ALC language that satisfies the following two additional conditions:

1. For all concept names c, and all d⃗, e⃗ ∈ D⃗ such that d⃗ ≡_{δ(c)} e⃗, the signature interpretation satisfies d⃗ ∈ ℑ_{Σ}(c) iff e⃗ ∈ ℑ_{Σ}(c).

2. For all role names p, and all d⃗, e⃗ ∈ D⃗ such that d⃗ ≡_{δ(p)} e⃗, the signature interpretation satisfies ℑ_{Σ}(p)(d⃗) = ℑ_{Σ}(p)(e⃗). <

If all sets δ(c) and δ(p) are equal to {1, …, n}, the set of all dimension, then this yields the semantics of M-ALC, as defined in Section 1. Otherwise, the set of admissible interpretations is restricted. Thus, a given concept term of an M-ALC language with dimension independence may be unsatisfiable, even though it is satisfiable with respect to the semantics of the underlying M-ALC language.

As an example, assume that n = 2, and that we have two roles p and q such that dim(p) = 1, dim(q) = 2, δ(p) = {1}, and δ(q) = {2}. Consider the concept term

c_{0} = ⟨p⟩⟨q⟩c ∧ [q][p]¬c.

The interpretation ℑ = (D⃗, ℑ_{Σ}) is defined as follows: D_{1} =^{def} {a_{0}, a_{1}}, D_{2} =^{def} {b_{0}, b_{1}}; ℑ_{Σ}(p)(a_{0}, b_{0}) = {a_{1}} and ℑ_{Σ}(p)(d⃗) = ∅ for all d⃗ ≠ (a_{0}, b_{0}); ℑ_{Σ}(q)(a_{1}, b_{0}) = {b_{1}} and ℑ_{Σ}(q)(d⃗) = ∅ for all d⃗ ≠ (a_{1}, b_{0}); ℑ_{Σ}(c) = {(a_{1}, b_{1})}.

It is easy to see that ℑ, (a_{0}, b_{0}) ⊧ c_{0}. However, ℑ is not an admissible interpretation of the language with dimension independence. For example, we have (a_{0}, b_{0}) ≡_{δ(p)} (a_{0}, b_{1}), but ℑ_{Σ}(p)(a_{0}, b_{0}) = {a_{1}} ≠ ∅ = ℑ_{Σ}(p)(a_{0}, b_{1}). More generally, it can be shown that there cannot be an interpretation of the language with dimension independence that interprets the concept term c_{0} by a non-empty set. Indeed, since p does not depend on q’s dimension and vice versa, applications of the p-role and the q-role commute. For this reason, the concept terms ⟨p⟩⟨q⟩c and ⟨q⟩⟨p⟩c are equivalent, and this obviously shows unsatisfiability of c_{0}.

In the remainder of this section we show that allowing for arbitrary role terms and dimension independence of roles in M-ALC leads to an undecidable satisfiability problem.

Theorem 5.3 Satisfiability of concept terms is undecidable for the class of M-ALC languages with dimension independence. <

In order to prove the theorem we reduced the domino problem [2, 11] to the satisfiability problem for M-ALC languages with dimension independence.

Definition 5.4 An instance of the domino problem consists of a finite set C = {1, …, n} of ‘colours’, and a finite set T = {t_{1}, …, t_{m}} of ‘domino types’, where each domino type is a 4–tuple t_{i} = (l_{i}, r_{i}, a_{i}, b_{i}) ∈ {1, …, n}^{4}.

Let IN denote the set of nonnegative integers. A solution of the domino problem (C, T) is a mapping L : IN × IN → T such that, for all (i, j) ∈ IN × IN, the following two conditions hold:

• If L(i, j) = t_{ν} = (l_{ν}, r_{ν}, a_{ν}, b_{ν}) and L(i + 1, j) = t_{μ} = (l_{μ}, r_{μ}, a_{μ}, b_{μ}) then r_{ν} = l_{μ}.

• If L(i, j) = t_{ν} = (l_{ν}, r_{ν}, a_{ν}, b_{ν}) and L(i, j + 1) = t_{ξ} = (l_{ξ}, r_{ξ}, a_{ξ}, b_{ξ}) then a_{ν} = b_{ξ}. <

Intuitively, a domino type is a square such that each side has a colour from the set of available colours C. In the tuple (l_{i}, r_{i}, a_{i}, b_{i}), the number l_{i} describes the colour of the left side of the square, r_{i} describes the colour of the right side, a_{i} describes the colour we see from above, and b_{i} describes the colour we see from below. For each type, one assumes that there are infinitely many dominos of this type. The domino problem is concerned with the question of whether it is possible to tile the upper right quadrant of the plain with dominos of the available types (without rotating or reflecting the domino types), where an admissible tiling must satisfy the restriction that the sides where dominos touch have identical colour. As shown by Berger [2], this problem is undecidable.

The reduction. Let (C, T) be an instance of the domino problem. We shall use this instance to define a 2-dimensional M-ALC language with dimension independence, and a concept term c_{0} of this language such that (C, T) has a solution iff c_{0} is satisfiable.

The set of role names of the M-ALC language defined by (C, T) consists of the names p, q, l, r, a, b, and s, and the set of concept names consists of the names c_{1}, …, c_{n}, where n is the number of different colours in C. We define dim(p) = dim(l) = dim(r) = dim(a) = dim(b) = dim(s) = 1, dim(q) = 2, δ(p) = {1}, δ(q) = {2}, and δ(l) = δ(r) = δ(a) = δ(b) = δ(s) = δ(c_{1}) = … = δ(c_{n}) = {1, 2}.

Intuitively, the concepts c_{1}, …, c_{n} are used to represent the n different colours. The roles l, r, a, b represent the corresponding components of a domino type. The role p goes to the right in the 2-dimensional grid IN × IN (i.e., it is meant to increment the first component of a tuple in IN × IN), and the role q goes up in the 2-dimensional grid. Finally, s is an auxiliary role, whose function will become clear later on.

In order to facilitate the definition of c_{0} we shall introduce some abbreviations for concept terms. First, let us show how the colours will be represented. We cannot directly use the concept names c_{1}, …, c_{n} to this purpose, because we must make sure that a side of a domino has one colour only. Thus, we need concept terms that are always interpreted as pairwise disjoint sets. This can, for example, be achieved by using the terms

ĉ_{i} =^{def} c_{i} ∧ ⋀_{j≠i} ¬c_{j} (for i = 1, …, n).

Second, we introduce the concept terms that represent the domino types. For t_{i} = (l_{i}, r_{i}, a_{i}, b_{i}) (i = 1, …, m) we define

d_{i} =^{def} [l]^{+}ĉ_{l_{i}} ∧ [r]^{+}ĉ_{r_{i}} ∧ [a]^{+}ĉ_{a_{i}} ∧ [b]^{+}ĉ_{b_{i}}.

Third, we need a term that expresses that a point in the grid is assigned one of the types, and that the types of the adjacent grid points have appropriate colours at the sides where the dominos touch:

d =^{def} ⋁_{i=1}^{m} d_{i} ∧ ([p]^{+}[l]ĉ_{r_{i}}) ∧ ([q]^{+}[b]ĉ_{a_{i}}).

Finally, the concept term c_{0} is defined as

c_{0} =^{def} [s]⊥ ∧ [[s]p] ([s]⊥ ∧ [[s]q]d) .

In order to understand this definition, one should reconsider the example given at the beginning of Section 3. There we have shown that, in the 1-dimensional case, a concept term of the form [[s]p]c ∧ [s]⊥ is satisfiable in an interpretation ℑ only if all elements of the carrier set D_{1} belong to the concept c. In the 2-dimensional case, we make the same construction, but it must be nested to handle both dimensions.

Lemma 5.5 If the domino problem (C, T) has a solution then the corresponding concept term c_{0} is satisfiable.

Proof: Let L : IN×IN → T be a solution of (C, T). This solution is used to define an interpretation ℑ = (D⃗, ℑ_{Σ}) of our 2-dimensional M-ALC language with dimension independence:

• D_{1} =^{def} D_{2} =^{def} IN,

• ℑ_{Σ}(c_{i}) =^{def} {(i, j) | j ∈ IN} for i = 1, …, n,

• ℑ_{Σ}(p)(i, j) =^{def} {i + 1} and ℑ_{Σ}(q)(i, j) =^{def} {j + 1},

• ℑ_{Σ}(l)(i, j) =^{def} {l_{ν}}, ℑ_{Σ}(r)(i, j) =^{def} {r_{ν}}, ℑ_{Σ}(a)(i, j) =^{def} {a_{ν}},

and ℑ_{Σ}(b)(i, j) =^{def} {b_{ν}}, where L(i, j) = t_{ν} = (l_{ν}, r_{ν}, a_{ν}, b_{ν})

• ℑ_{Σ}(s)(i, j) =^{def} ∅ for all i, j ∈ IN.

By definition of ℑ_{Σ}(p) and ℑ_{Σ}(q), this interpretation is an admissible interpretation for the language with dimension independence. Indeed, for p the image depends only on the first component i of the tuple (i, j), and for q it depends only on the second component j. The sets ℑ_{Σ}(c_{i}) (i = 1, …, n) are already pairwise disjoint. For this reason the interpretation of the concept name c_{i} coincides with the interpretation of the concept term ĉ_{i} = c_{i} ∧ ⋀_{j≠i} ¬c_{j}.

In the following, we shall show that ℑ, (0, 0) ⊧ c_{0}. First, note that the definition of ℑ_{Σ}(s) obviously implies ℑ, (0, 0) ⊧ [s]⊥. Second, this definition also implies that ℑ([s]p)(0, 0) = IN. Thus, it remains to be shown that ℑ, (i, 0) ⊧ [s]⊥ ∧ [[s]q]d holds for all i ∈ IN. The definition of ℑ_{Σ}(s) obviously implies ℑ, (i, 0) ⊧ [s]⊥, and ℑ([s]q)(0, 0) = IN. Hence it is sufficient to show that ℑ, (i, j) ⊧ d holds for all i, j ∈ IN.

Let (i, j) ∈ IN×IN with L(i, j) = t_{ν} = (l_{ν}, r_{ν}, a_{ν}, b_{ν}) be given. First, we show that ℑ, (i, j) ⊧ d_{ν}. By definition, we have ℑ_{Σ}(l)(i, j) = {l_{ν}}, and (l_{ν}, j) ∈ ℑ_{Σ}(c_{l_{ν}}). The second fact implies that ℑ, (l_{ν}, j) ⊧ ĉ_{l_{ν}}, and thus we have ℑ, (i, j) ⊧ [l]^{+}ĉ_{l_{ν}}. Accordingly, we can show that ℑ, (i, j) ⊧ [r]^{+}ĉ_{r_{ν}}, ℑ, (i, j) ⊧ [a]^{+}ĉ_{a_{ν}}, and ℑ, (i, j) ⊧ [b]^{+}ĉ_{b_{ν}}, which yields ℑ, (i, j) ⊧ d_{ν}.

Second, we show that ℑ, (i, j) ⊧ [p]^{+}[l]ĉ_{r_{ν}}. By definition, we have ℑ_{Σ}(p)(i, j) = {i + 1}, and thus it remains to be shown that ℑ, (i + 1, j) ⊧ [l]ĉ_{r_{ν}}. By our interpretation of the role l we have ℑ_{Σ}(l)(i+1, j) = {l_{μ}}, where L(i+1, j) = (l_{μ}, r_{μ}, a_{μ}, b_{μ}). Hence we must show that ℑ, (l_{μ}, j) ⊧ ĉ_{r_{ν}}. Since L was assumed to be a solution of the domino problem, we know that r_{ν} = l_{μ}. Consequently, we have ℑ_{Σ}(c_{r_{ν}}) = ℑ_{Σ}(c_{l_{μ}}) = {(l_{μ}, k) | k ∈ IN}, which yields the desired property ℑ, (l_{μ}, j) ⊧ ĉ_{r_{ν}}.

Accordingly, ℑ, (i, j) ⊧ [q]^{+}[b]ĉ_{a_{ν}} can be shown, which completes proof of the lemma. <

Lemma 5.6 If the concept term c_{0} corresponding to the domino problem (C, T) is satisfiable then the domino problem has a solution.

Proof: Let ℑ = (D⃗, ℑ_{Σ}) be an interpretation of our 2-dimensional M-ALC language with dimension independence, and let (d_{0}, e_{0}) ∈ D⃗ be such that ℑ, (d_{0}, e_{0}) ⊧ c_{0}. We shall use ℑ and (d_{0}, e_{0}) for defining a solution L of the domino problem.

From ℑ, (d_{0}, e_{0}) ⊧ c_{0} we can deduced that ℑ, (x, y) ⊧ d holds for all (x, y) ∈ D⃗. Indeed, ℑ, (d_{0}, e_{0}) ⊧ [s]⊥ implies ℑ_{Σ}(s)(d_{0}, e_{0}) = ∅, and thus ℑ_{Σ}([s]p)(d_{0}, e_{0}) = D_{1}. Therefore, we can deduce that ℑ, (x, e_{0}) ⊧ [s]⊥ ∧ [[s]q]d holds for all x ∈ D_{1}. For similar reasons this implies ℑ, (x, y) ⊧ d for all y ∈ D_{2}.

In order to define a mapping L : IN × IN → T, we construct a sequence of tuples (d_{i}, e_{i}) ∈ D⃗, i ≥ 0, starting with the already given (d_{0}, e_{0}). Now assume that (d_{i}, e_{i}) is already defined. From ℑ, (d_{i}, e_{i}) ⊧ d we can deduce that there exist ν, 1 ≤ ν ≤ m such that

ℑ, (d_{i}, e_{i}) ⊧ d_{ν} ∧ ([p]^{+}[l]ĉ_{r_{ν}}) ∧ ([q]^{+}[b]ĉ_{a_{ν}}).

Because of the ‘[p]^{+}’ and ‘[q]^{+}’ in this concept term, we know that there exist d′ ∈ ℑ_{Σ}(p)(d_{i}, e_{i}) and e′ ∈ ℑ_{Σ}(q)(d_{i}, e_{i}). We define d_{i+1} =^{def} d′ and e_{i+1} =^{def} e′.

The mapping L : IN × IN → T is now defined as follows. For (i, j) ∈ IN × IN we consider the tuple (d_{i}, e_{j}) ∈ D⃗. From ℑ, (d_{i}, e_{j}) ⊧ d we can deduce that there exists an index ν_{i,j} such that ℑ, (d_{i}, e_{j}) ⊧ d_{ν_{i,j}}. Note that there is exactly one such ν_{i,j}. This follows from the definition of the d_{ν}’s and the fact that the concept terms ĉ_{μ} are necessarily interpreted by pairwise disjoint sets. We define L(i, j) =^{def} t_{ν_{i,j}}.

It remains to be shown that L is a solution of the domino problem. Thus, consider L(i, j) = t_{ν_{i,j}} = (l_{ν_{i,j}}, r_{ν_{i,j}}, a_{ν_{i,j}}, b_{ν_{i,j}}) and L(i + 1, j) = t_{ν_{i+1,j}} = (l_{ν_{i+1,j}}, r_{ν_{i+1,j}}, a_{ν_{i+1,j}}, b_{ν_{i+1,j}}). We show that r_{ν_{i,j}} = l_{ν_{i+1,j}}. (The fact b_{ν_{i,j}} = a_{ν_{i,j+1}} can be proved analogously.)

We know that d_{i+1} ∈ ℑ_{Σ}(p)(d_{i}, e_{i}), and since δ(p) = {1} this implies d_{i+1} ∈ ℑ_{Σ}(p)(d_{i}, e_{j}). Because ℑ, (d_{i}, e_{j}) ⊧ d_{ν_{i,j}}, and since ν_{i,j} is unique with this property, we have ℑ, (d_{i}, e_{j}) ⊧ [p]^{+}[l]ĉ_{r_{ν_{i,j}}}. Thus, we can deduce ℑ, (d_{i+1}, e_{j}) ⊧ [l]ĉ_{r_{ν_{i,j}}}. On the other hand, ℑ, (d_{i+1}, e_{j}) ⊧ d_{ν_{i+1,j}}, and this concept term has the term [l]^{+}ĉ_{l_{ν_{i+1,j}}} as a conjunct. Pairwise disjointness of the concept terms ĉ_{μ} thus implies r_{ν_{i,j}} = l_{ν_{i+1,j}}. <

To sum up, we have shown that, for a given instance of the domino problem, we can construct a concept term c_{0} of an M-ALC language with dimension independence such that the domino problem has a solution iff the concept term c_{0} is satisfiable. Since the domino problem is in general undecidable, this yields a proof of Theorem 5.3.

In the reduction we have used both unrestricted role terms (i.e., terms not satisfying restricted seriality) and independence of some of the dimensions for roles. Thus, it remains an open problem whether satisfiability becomes decidable if one of these two means of representation is disallowed. For the case where one only has atomic roles, but independence of dimensions is allowed, we strongly conjecture that satisfiability is decidable, but we do not have a proof yet.

6 Summary and Open Problems

The present paper is a first investigation of a new kind of multi–dimensional modal logic. The logic M-ALC is a combination of modal logics K_{m}, but the combination is of an unusual type. The modal operators of the component logics do not only operate on the formulae in the combined logic, but also directly on the operators of the other logics. As we have seen, this gives rise to quite complicated interactions between the component logics. This kind of logic was motivated by applications in the area of kl-one-like knowledge representation systems, and in particular by the need of modelling the knowledge of intelligent agents.

In this paper, we have only worked out the basic framework and related it to the standard multi–modal case. In particular, we have shown that Venema’s axiomatization, which reduces the n–dimensional semantics to a one–dimensional semantics, can be extended in such a way that it captures the semantics of compound role terms. We have defined a calculus based on the idea of labelled deductive systems. We have shown that the calculus is terminating and sound, but completeness remains an open problem for the case of restricted serial terms. Completeness was shown for the case where all role terms are atomic. This result is not surprising because we have also shown that in this case there is no difference between satisfiability in n dimensions and satisfiability in 1 dimension. Finally, we have shown that an extension of M-ALC, in which it is possible to specify independence of some dimensions for roles, leads to an undecidable satisfiability problem. There are various interesting questions that remain open.

First, of course, is the question whether the algorithm is also complete for unsatisfiability. If the answer is yes, this would show decidability of the satisfiability problem for restricted serial M-ALC terms. If the answer is no, decidability remains an open question. The semantics of M-ALC allows for a straightforward translation of concept terms into first-order predicate logic. But the translated versions of even small concept terms may already become very complicated. The formulae one obtains do not seem to fall into one of the known decidable subclasses of firstorder logic. This is in contrast to ALC where concept terms can be translated into formulae of the Gödel class.

More generally, one can ask whether the methods described above can be adapted to the case where arbitrary [...]-operators are allowed at the role term level. Related is the question whether satisfiability for arbitrary M-ALC terms is decidable?

An adequate representation of modalities such as know, belief, or time require component logics that are stronger than K_{m}; for example S4.3 for knowledge, linear structures for time etc. More generally, one can ask whether it is possible to modify the satisfiability algorithm such that it can take additional modal axioms into account. A possible way of attacking this problem could be to translate the modal axiom schemas into properties of the accessibility relations (see [10]). Complex correlations between different modal operators can thus be investigated, and turned into additional rules of the satisfiability algorithm. However, without additional restrictions, the rule set one thus obtains will usually not be terminating.

As already mentioned, a flexible treatment of T-Box axioms would be desirable. Can such axioms be handled by a satisfiability algorithm? Also, the interaction with A-Boxes has not yet been considered. In this context, is it possible to parameterize the role terms with A-Box elements or concept terms, e.g., by writing [know(John)] where John is an A-Box individual or [believe(car-salesmen)] where car-salesmen is a concept that is defined in the T-Box?

Finally, it is still an open question whether satisfiability is decidable in the case where one has only atomic role terms, but allows for independence of dimensions for roles.

References

[1] F. Baader and B. Hollunder. A terminological knowledge representation system with complete inference algorithms. In Michael M. Richter and Harold Boley, editors, Proc. of PDK 91. LNAI 567, 1991.

[2] R. Berger. The Undecidability of the Domino Problem. Memoirs of the AMS, volume 66, 1966.

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

[4] R.J. Brachman, D.L. McGuinness, P.F. Patel-Schneider, L.A. Resnick, and A. Borgida. Living with CLASSIC: When and how to use a KL-ONE-like language. In J. Sowa, editor, Principles of Semantic Networks, pages 401–456. Morgan Kaufmann, San Mateo, Calif., 1991.

[5] B.F. Chellas. Modal Logic: An Introduction. Cambridge University Press, Cambridge, 1980.

[6] N. Dershowitz and Z. Manna. Proving termination with multiset orderings. Communications of the ACM, 8(22):465–476, 1979.

[7] F.M. Donini, M. Lenzerini, D. Nardi, and W. Nutt. The complexity of concept languages. In Proc. of KR’91, Principles of Knowledge Representation and Reasoning, pages 151–162. Morgan Kaufmann, 1991.

[8] M.J. Fischer and R.E. Ladner. Propositional dynamic logic of regular programs. Journal of Computer and System Science, 18:194–211, 1979.

[9] D.M. Gabbay. Labelled Deduction Systems. Oxford University Press, 1991, in preparation.

[10] D.M. Gabbay and H.J. Ohlbach. Quantifier elimination in second-order predicate logic. South African Computer Journal, 7:35–43, July 1992. Also in Proc. of KR92, Morgan Kaufmann, 1992, pp 425–436.

[11] D.E. Knuth. The Art of Computer Programming (Volume I): Fundamental Algorithms Addison-Wesley, Reading, MA, 1973.

[12] A. Kobsa. First experiences with the SB-ONE knowledge representation workbench in natural language applications. SIGART Bulletin, 2:70–76, 1991.

[13] A. Laux. Integrating a modal logic of knowledge into terminological logics. In H. Geffner, editor, Proceedings of the 4th Iberoamerican Congress on Artificial Intelligence, pages 76–92, Caracas, Venezuela, 1994.

[14] H.J. Levesque and R.J. Brachman. Expressiveness and tractability in knowledge representation and reasoning. Computational Intelligence, 3:78–93, 1987.

[15] B. Nebel. Reasoning and Revision in Hybrid Representation Systems. LNAI 422, 1990.

[16] B. Nebel and G. Smolka. Representation and reasoning with attributive descriptions. In K.H. Bläsius, U. Hedtstück, and C.-R. Rollinger, editors, Sorts and Types in Artificial Intelligence, pages 112–139. LNAI 418, 1990.

[17] Hans Jürgen Ohlbach. Semantics based translation methods for modal logics. Journal of Logic and Computation, 1(5):691–746, 1991.

[18] John Alan Robinson. Automated deduction with hyper-resolution. International Journal of Computer Mathematics, 1(3):227–234, 1965.

[19] K. Schild. A correspondence theory for terminological logics: Preliminary report. In Proc. of IJCAI 91, pages 466–471. Morgan Kaufmann, 1991.

[20] M. Schmidt-Schauß and G. Smolka. Attributive concept descriptions with complements. Artificial Intelligence, 48:1–26, 1991.

[21] Johan van Benthem. Correspondence theory. In Gabbay Dov M and Franz Guenthner, editors, Handbook of Philosophical Logic, Vol. II, Extensions of Classical Logic, Synthese Library Vo. 165, pages 167–248. D. Reidel Publishing Company, Dordrecht, 1984.

[22] Y. Venema. Many-Dimensional Modal Logic. PhD thesis, University of Amsterdam, Amsterdam, The Netherlands, 1992.

[23] W.A. Woods and J.G. Schmolze. The kl-one family. Computers and Mathematics with Applications, 23(2–5):133–177, 1992. Special Issue on Semantic Networks in Artificial Intelligence.

[figure: I N F O R M A T I K]

Below you find a list of the most recent technical reports of the research group Logic of Programming at the Max-Planck-Institut für Informatik. They are available by anonymous ftp from our ftp server ftp.mpi-sb.mpg.de under the directory pub/papers/reports. Most of the reports are also accessible via WWW using the URL http://www.mpi-sb.mpg.de. If you have any questions concerning ftp or WWW access, please contact reports@mpi-sb.mpg.de. Paper copies (which are not necessarily free of charge) can be ordered either by regular mail or by e-mail at the address below.

Max-Planck-Institut für Informatik Library attn. Regina Kraemer Im Stadtwald D-66123 Saarbrücken GERMANY

e-mail: kraemer@mpi-sb.mpg.de

MPI-I-95-2-002 H. J. Ohlbach, R. A. Schmidt Functional Translation and Second–Order Frame Properties

MPI-I-95-2-001 S. Vorobyov Subject Reduction and Proof Normalization in Extensions of Fsub

MPI-I-94-261 P. Barth, A. Bockmayr Finite Domain and Cutting Plane Techniques in CLP(PB)

MPI-I-94-257 S. Vorobyov Structural Decidable Extensions of Bounded Quantification

MPI-I-94-254  Report and abstract not published

MPI-I-94-252 P. Madden A Survey of Program Transformation With Special Reference to Unfold/Fold Style Program Development

MPI-I-94-251  P. Graf  Substitution Tree Indexing

MPI-I-94-246 M. Hanus On Extra Variables in (Equational) Logic Programming

MPI-I-94-241 J. Hopf Genetic Algorithms within the Framework of Evolutionary Computation: Proceedings of the KI-94 Workshop

MPI-I-94-240 P. Madden Recursive Program Optimization Through Inductive Synthesis Proof Transformation

MPI-I-94-239 P. Madden, I. Green A General Technique for Automatically Optimizing Programs Through the Use of Proof Plans

MPI-I-94-238 P. Madden Formal Methods for Automated Program Improvement

MPI-I-94-235  D. A. Plaisted  Ordered Semantic Hyper-Linking
MPI-I-94-234  S. Matthews, A. K. Simpson  Reflection using the derivability conditions

MPI-I-94-233 D. A. Plaisted The Search Efficiency of Theorem Proving Strategies: An Analytical Comparison

MPI-I-94-232  D. A. Plaisted  An Abstract Program Generation Logic

MPI-I-94-230 H. J. Ohlbach Temporal Logic: Proceedings of the ICTL Workshop

MPI-I-94-229  Y. Dimopoulos  Classical Methods in Nonmonotonic Reasoning

MPI-I-94-228 H. J. Ohlbach Computer Support for the Development and Investigation of Logics

In the rules below, c and d are concept terms, ϕ is either a concept term or a role term like p:a, and i = dim(p). The suffix ‘&Γ’ stands for the unmodified part of the constraint system under consideration, and ‘& Δ’ stands for the other constraint systems currently not under consideration.

( ∧) {l⃗:c ∧ d & Γ} & Δ → {l⃗:c ∧ d, l⃗:c, l⃗:d & Γ} & Δ if not both l⃗:c and l⃗:d are in Γ.

( ∨) {l⃗:c ∨ d & Γ} & Δ → {l⃗:c ∨ d, l⃗:c & Γ},

{l⃗:c ∨ d, l⃗:d & Γ} & Δ

if neither l⃗:c nor l⃗:d is in Γ.

(\overline{[]^{+}}) \{l⃗:\overline{[p]^{+}q}:a & Γ\} & Δ → \{l⃗:\overline{[p]^{+}q}:a, l⃗:⟨p⟩\overline{q}:a & Γ\},

\{l⃗:\overline{[p]^{+}q}:a, l⃗:[p]⊥ & Γ\} & Δ

if neither l⃗:⟨p⟩\overline{q}:a nor l⃗:[p]⊥ is in Γ.

(\overline{⟨⟩}) \{l⃗:\overline{⟨p⟩q}:a & Γ\} & Δ → \{l⃗:\overline{⟨p⟩q}:a, l⃗:[p]^{+}\overline{q}:a & Γ\},

\{l⃗:\overline{⟨p⟩q}:a, l⃗:[p]⊥ & Γ\} & Δ

if neither l⃗:[p]^{+}\overline{q}:a nor l⃗:[p]⊥ is in Γ.

(⟨⟩) {l⃗:⟨p⟩ϕ & Γ} & Δ → {l⃗:⟨p⟩ϕ, l⃗:p:a, l⃗[i/a]:ϕ & Γ} & Δ {l⃗:[p]^{+}ϕ & Γ} & Δ → {l⃗:[p]^{+}ϕ, l⃗:p:a, l⃗[i/a]:ϕ & Γ} & Δ if l⃗:p:b, l⃗[i/b]:ϕ is not in Γ for some b. Here a is assumed to be a new constant of dimension i.

([]^{∗}) {l⃗:[p]^{∗}ϕ, & Γ} & Δ → {l⃗:[p]^{∗}ϕ, l⃗[i/a]:ϕ & Γ} & Δ if a is a constant of dimension i, d(l⃗, Γ) + |p| = d(a, Γ) =: n, l⃗[i/a]:ϕ ∉ Γ, and apply-rules(\{\{l⃗′:q:b ∈ Γ | d(b, Γ) ≤ n\} ∪ \{l⃗:\overline{p}:a)\}\}) = ‘unsatisfiable’

(⊥) {l⃗:c, l⃗:¬c & Γ} & Δ → Δ \{l⃗:p:a, l⃗:\overline{p}:a & Γ\} & Δ → Δ {l⃗:⊥ & Γ} & Δ → Δ

(⊤) Γ & Δ → ‘satisfiable’ if none of the other rules is applicable to Γ

(∅) ∅ → ‘unsatisfiable’

Figure 2: Transformation rules of the satisfiability algorithm for M-ALC.

([]^{∗}) {l⃗:[p]^{∗}ϕ, & Γ} & Δ → {l⃗:[p]^{∗}ϕ, l⃗[i/a]:ϕ & Γ} & Δ if a is a constant of dimension i and l⃗:p:a ∈ Γ.

Figure 3: Simplified []^{∗}-rule for the case of atomic role terms.