MAX-PLANCK-INSTITUT FÜR

INFORMATIK

A Multi-Dimensional Terminological Knowledge Representation Language

Preliminary Version

Franz Baader & Hans Jürgen Ohlbach

MPI–I–93–212 August 1993

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

Im Stadtwald W 66123 Saarbrücken Germany Author’s Address

Franz Baader Lehr- und Forschungsgebiet Theoretische Informatik, RWTH Aachen, Ahornstraße 55, D-52074 Aachen, email:baader@informatik.rwth-aachen.de

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

Publication Notes

A short version of this report also appears in the proceedings of the International Conference on Artificial Intelligence (IJCAI) 1993 in Chambery, France.

Acknowledgements

This work was supported by the ESPRIT project 3125 MEDLAR, and 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.

Contents

1 Introduction 1

2 Syntax and Semantics of M-ALC 2

3 The Satisfiability Test 5

4 Proof of Termination and Soundness 8

5 Summary and Open Problems 16

1 Introduction

Knowledge representation languages in the style of kl-one [2], 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., [12, 14, 13, 15, 6, 1, 3, 17]).

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 [10]—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 get the definition

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.

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.

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 [15] that the terminological language ALC is just a syntactic variant of the multi-modal logic K_{m} [4], 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.

However, the requirement that it should be possible to modify roles by modal operators is 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., [15]) 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.

2 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.

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

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.

Definition 2.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 [16]. 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 2.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 p be a role name, q, r be role terms, and let j be the dimension of q.

\begin{aligned}ℑ(p)(d⃗) & = & ℑ_{Σ}(p)(d⃗), \\ ℑ([q]r)(d⃗) & = & ⋂_{x∈ℑ(q)(d⃗)} ℑ(r)(d⃗[j/x]), \\ ℑ(⟨q⟩r)(d⃗) & = & ⋃_{x∈ℑ(q)(d⃗)} ℑ(r)(d⃗[j/x]), \\ ℑ([q]^{+}r)(d⃗) & = & ℑ([q]r)(d⃗) ∩ ℑ(⟨q⟩r)(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⃗ ⊧ ϕ.

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 [11]. 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 2.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.

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. That 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 [8]. 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 1 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.

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 1: Transformation rules of the satisfiability algorithm for M-ALC.

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| := |p| := 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| := |c| and |\overline{q}| := |q|.

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

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

4. |q : a| := |q|.

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

m(l⃗, Γ) := 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

Γ′′ := \{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 [5] 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 Ψ(Γ) := (Ψ_{1}(Γ), Ψ_{2}(Γ)). The first component of this 2-tuple is defined as

Ψ_{1}(Γ) := 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} := 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.^{3} 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⃗,^{4} 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.

(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) An interpretation for a constraint system Γ 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 Γ,

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

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

• 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 2.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 1 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 to 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 Γ.

5 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 have defined a calculus based on the idea of labelled deductive systems. 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 gets do not seem to fall into one of the known decidable subclasses of first-order 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 [9]). 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)] or [believe(car-salesmen)]?

References

[1] Franz Baader and Bernhard 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. Brachman and J. Schmolze. An overview of the KL-ONE knowledge representation system. Cognitive Science, 9(2):171–216, 1985.

[3] 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.

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

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

[6] Francesco M. Donini, Maurizio Lenzerini, Daniele Nardi, and Werner Nutt. The complexity of concept languages. In Proc. of KR’91, Principles of Knowledge Representation and Reasoning, pages 151–162. Morgan Kaufmann, 1991.

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

[8] Dov M. Gabbay. Labelled Deduction Systems. Oxford University Press, 1991, in preparation.

[9] Dov M. Gabbay and Hans Jürgen 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.

[10] A. Kobsa. The SB-ONE knowledge representation workbench. In Preprints of the Workshop on Formal Aspects of Semantic Networks, Two Habours, Calif., 1989.

[11] A. Laux. Integrating a modal logic of knowledge into terminological logics. Research Report RR-92-56, DFKI Saarbrücken, 1992.

[12] Hector J. Levesque and Ron J. Brachman. Expressiveness and tractability in knowledge representation and reasoning. Computational Intelligence, 3:78–93, 1987.

[13] Bernhard Nebel. Reasoning and Revision in Hybrid Representation Systems. LNAI 422, 1990.

[14] Bernhard Nebel and Gert 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.

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

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

[17] William A. Woods and James 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.