A Multi-Dimensional Terminological Knowledge Representation Language

1 Introduction

Knowledge representation languages in the style of KL­ ONE [3] , so-<:alled terminological KR languages , can be used to define the relevant concepts of a problem do­ main 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 con­ structs provided by the particular terminological lan­ guage. Various such languages have been considered in the literature and are used in KR systems (see, e.g., [12, 14, 13, 15, 6, 1, 4, 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 n 3has-part: catalytic-converter

·This work was supported by the ESPRIT project 312.5 MEDLAR, and the BMFT Projects Logo (ITS 9102) and TACOS (ITW 9201)

Franz Baader

German Research Center for AI (DFKI) Stuhlsatzenhausweg 3

6600 Saarbriicken 11 , Germany

email: baader@dfki . uni-sb.de

Tom's T-Box:

new-car = car n -,:Jhas-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- .. .jl that satisfy appropriate modal axioms allow for more natural definitions:

[belief-John] (new-car =

car n 3has-part : catalytic-converter),

[belief-Tom](new-car =

car n -,:Jhas-part: catalytic-converter) .

Things become more complex if the application re­ quires 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 eventu­ ally wants to own a car. In a traditional terminological language a definition of this concept could be

pot-customer= adult n 3eventually-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 in­ teraction 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

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 n

1 The standard modal operators are usually written 0 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.

'v'([ want] own):[ l1elie~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 [ belie~-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 lan­ guage A.CC is just a syntactic variant of the multi-modal logic I<m [5], where m is the number of different box op­ erators. The reason is that quantifications over roles can just be seen as applications of parametrized modal op­ erators 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 parametrized modal operators are atomic in the sense that the boxes and di­ amonds may only contain parameter names like own , fu­ ture, or belief Applying modal operators to roles means that one obtains complex terms inside boxes and dia­ monds . 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 ter­ minological KR languages, called M-A.CC in the follow­ ing, thus extends the prototypical terminological la~­ guage A.CC in two respects. First, 'roles' may have dif­ ferent types that express in what dimension (e.g., object­ dimension, time-point-dimension) they operate. In ad­ dition , one can apply role quantification not only to con­ cepts but also to roles, which provides for a very expres­ sive 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 satis­ fiability of concept terms.

2 Satisfiability ·modulo concept equations is known to be exp-time complete; this is an ea.~y consequence of a result hy Fischer and Ladner [7].

2 Syntax and Semantics of M-A.CC

As for A.CC, the elementary syntax elements in M-A.CC are concept and role names . However, with each role name we associate a type that expresses in what dimen­ sion (e.g., object-dimension, time-point-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 (do­ main, universe) . For example, the object dimension cor­ responds to the set of all objects (as used in A.CC), 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 ax­ ioms. This means that the underlying logic is simply the basic modal logic K.

The syntactic form of a modal operator in M-A.CC 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 under­ stood in the sense that the person in question really has friends . Thus it is better modelled by the expression [has-friem~+ wealthy than by [has-friend] wealthy.

Definition 2.1 The signature E of an M-A.CC lan­ guage .Cn of dimension n > 0 consists of a set Ep of role names and a disjoint set Ec of concept names. The concept names include the distinguished symbols T {for 'truth') and ..l (for 'falsity'). Each role name p has a dimension dim(p), which is a positive integer :S n .

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

• Each role name pis 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 dimen­ sion 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 V d and c 1\ 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 cis a concept name, d a concept term, and m a modal pre­ fix, i.e., a (possibly empty) sequence of box and diamond operators. A T-Box is a set of concept equations.

A concept term is ca./led restricted serial if role ter·ms do not contain normal [ ... ]-operator·s. <l

Even for a single dimension, M-A.CC is an extension of A.CC since one can build complex role terms. This allows one to express interactions between roles that. cannot. be captured in A.CC. For example, the concept. of a 'woman all of whose children have a common favourite meal ' is expressible by woman 1\ ({llas-childjlikes)meal.

The semantics of M-A.CC is similar to the Kripke style possible worlds semantics for many-dimensional modal logic {16] . For each dimension i we introduce a non­ empty set D; . The elements of D1 x ... x Dn correspond to worlds in the modal logic sense. As in modal logic, there is always an 'actual world tuple' cT = (d1 , ... , dn) that determines the interpretation of the syntax ele­ ments .

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-A.CC correspond t.o n + 1ary 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-A.CC we shall use the following notational conventions. For a fixed number of dimensions n, the Cartesian prod­ uct of the sets D1 , ... , Dn is denoted by D. An element (d1 , .. . ,dn) of D is denoted by J, and (d1 , ... , di-1 1 x, di+l· ... , dn) by l1[ijx].

Definition 2.2 An interpretation 8' (D, S'r;) for an n-dimensional M -A.CC language .Cn consists of the Cartesian product D = D1 x ... x Dn of n non-empty carrier sets (domains), and a signatur-e interpretation S'r;.

The signature interprdation assigns successor func­ tions to rde names and n-place relations to concept names. To be more precist:, a role name p is intt:rpreted as a function S'r;(p) : D -+ 2D', and a concept name c as a set S'r;( c) ~ D. The concept name T is interpreted as D and .l as the empty set.

The interpretation of a role ta·m q of dimension i is also a function 8'( q) : D -+ 2D; that is inductively de­ fined as follows. Let p be a role name, q, r be mle terms, and let j be the dimension of q.

S'(p)(d) ~r;(p)(lD,

~((q]r)(d) nxE"(q)(d) ~(r)(l1(jjx]),

~((q)r)(d) UxE~( q )(d) ~- ( r )( l1(j / :r:])'

~((q]+r)(lD ~((q]r)(d) n ~( (q)r)(d).

A satisfiability relation F between an interpretation ~ with actual point J and concept terms and concept equations is defined as follows. Let c be a concept name, e, f be concept tenns, p be a role term of dimension i, and l/J be a concept term or concept equation.

~,lLpc iJJrlE~r;(c)

~,dpc=e iff('Z'!,dpc iff'Z'J,dpe)

~. dp -.e iff not '21, dp e

~, d F e V f iff '21, d F e or '21, d F f

~. dp e 1\ f iff '21, dp e and '21, dp f

~. dp [p]<P iff for all x E 'Z'J(p)(d) : '21, d[ijx] F cP

~. dp (p)c/J iff for some x E 'Z'J(p)(d): '21, d[i/x] F cP

'21, J F [pJ+ <P iff '21, J F [p]<P and '21, J F (p)c/J

An interpretation '21 is a model of a T-Box iff for all actual points J and all equations l/J of the T-Box one has ~,Jp l/J. <l

It should be noted that with respect to this seman­ tics, 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 defini­ tion of models in modal logics where a formula is only required to hold at one point (world) . Only the char­ acteristic axioms of the particular modal system are re­ quired 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 ob­ jects 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 in­ side of concept terms. Since our concept and role terms already have a very complex structure we shall concen­ trate on the concept term level, and leave the treatment ofT-Boxes-with a possibly more flexible definition of a model-as a topic of further research.

The basic reasoning services every KL-ONE system pro­ vides 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 ( snbsumption problem).

Definition 2.3 The concept term e subsumes the con­ cept term f iff, for all interpretations '21 and actual points J, '21, dp f implies '21, dp e.

The concept term e is satisfiable iff there is an inter­ pretation '21 and an actual point J such that '21, J F e. <l

Since e subsumes f iff f 1\ -.e is unsatisfiable, it is suffi­ cient to have an algorithm for the satisfiability problem.

3 The Satisfiability Test

In A.CC 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 deter­ ministic and cycle free . That means no pairs c = d and c = d' with d ::j: d' are in the T-Box, and no chains c1 = dl[c2], ... , Cn = dn[c] are in the T-Box. With this restriction, all defined concepts in a concept. term can be expanded with their definition prior to the subsumpt.ion 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 spec­ ification 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 sat­ isfiability algorithm for concept terms (which is in fact a general theorem prover for the modal logic M-A.CC).

The algorithm we shall present works only for the re­ stricted serial case where no [ ... ]-operators occur in the role terms. The following example demonstrates the ex­ pressive 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 1\ [p]..l . The term [p]..l (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 do­ main 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-A.CC can be used to simulate general concept equations of the form c = T where c is a complex concept term. As mentioned in the introduc­ tion, general concept equation are very hard to handle algorithmically. If M-A.CC terms are assumed to satisfy the seriality restriction concept equations can no longer be expressed.

In the satisfiability algorithm we assume that all con­ cept 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:

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 f: tjJ where f = (/1 , ... , ln) consists of eonstant symbols generated during t.he expan­ sion of the tableau . The label f is the syntactic counter­ part of the 'actual world tuple' (I in an interpretation . That means f : 4> describes tjJ in the context f Here tjJ may be a concept term, a concept equation or a role term with an argument. The expression f: p : a for example means that a is a p-successor of ldim(p). 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-dimen.sional M-A.CC lan­ guage, constraints are built from constant symbols (points), n-tup./es of constant symbols (labels), and role and concept terms. A role constraint is a triple f: p : a consisting of a label ~ a role term p and a point a. A concept constraint is a tuple f: c consisting of a label f and a concept term c. A constraint system is a set of role constraints and concept constraints. <1

The constraint systems that are generated by our satisfiability algorithm will always have a specified ini­ tial label fa. The algorithm calls itself recursively with 'negated' role terms p in constraints. Since we must avoid [ ... ]-operators in the role terms, the rules for build­ ing negation normal form of role terms is slightly modi­ fied :

After building negation normal form, only atomic role names occur negated. Note that [p]..l is an allowed con­ cept term. The intended interpretation of p is simply as complement : ~(p)(d) = Ddim(p) \<J(p)(d). Since negated role terms occur only in a very restricted setting, this does not mean that we introduce general role negation.

The algorithm depends on a function depth that, for a given point in a constraint system, measures its distance from the initial label fa, i.e. it counts with how many atomic steps f : 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 IPI to be the number of occurrences of role names in p. For a constraint set r with initial label lo = (/ol, ... , Ion) we define

• depth(/o;,f)=Ofori= l, ... n.
• depth(~ r) = maxl~i~n depth( I;, r).
• If n = depth(~ f) is already defined, and f : p : b E r is selected by some selection function for b then depth(b, r) = n + IPI · <1

It can be shown that for the constraint systems generated by the satisfiability algorithm, this definition deter­ mines for every point and label in the system a unique depth (i .e., one that is independent of the selection func­ tion). 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 in­ put a restricted serial M-A.CC concept term c in nega­ tion normal form. It then constructs an initial label fa and builds the constraint system {fa : c} . Then it calls the function apply-rules with the singleton set Llo = {{fa : c}}. This function iteratively applies the rules of Figure 1 to the constraint systems already ob­ tained. It returns 'ttnsatisfiable' if the (0)-rule applies, and 'satisfiable' if the (T)-rule applies. <1

A small example shall illustrate how the algorithm works. In the one-dimensional case, the concept terms 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 '&f' stands for the unmodified part of the constraint system under consideration, and '& ~~stands for the other constraint. systems currently not under consideration.

• if not both f: c and f : d are in r. (V) {f: ¢>Vt/J & r} & ~ ---+ {f: ¢>Vt/J}: ¢> & r},{f: ¢>Vt/J}: t/J & r} & ~ if neither f: ¢> nor f: tf; is in r. (()) {f: (p)¢> & r} & ~ ---+ {f: (p)¢>}: p: a, qija] : ¢> & r} & ~ {f: (p]+¢> & r} & ~ ---+ {f: [p]+¢>, f: p: a, qija] : ¢> & r} & ~ iff : p : b, qijb] : ¢> is not in r for some b. Here a is assumed to be a new constant. (Q·) {f: (p]·¢>, & r} & ~ ---+ {f: (p]·¢>, qija] : ¢> & r} & ~ if depth(/, r) + IPI =depth( a, r) = : nand qija]: ¢>fl. rand apply-rules( {{f : q : b I depth(b, r) :S n} U {f: p: a)}}) = 'unsatisfiable' (J_) {f: c,f: -,c & r} & ~ ---+ ~ {f: p: a}: p: a & r} & ~ ---+ ~ {f:-,T&r}&~ ---+ ~ (T) r & ~ ---+ 'satisfiable' if none of the other rules is applicable to r (0) 0 ---+ 'unsatisfiable'

Figure 1: Transformation rules of the satisfiability algorithm for M-A.CC .

[(p)q)c and [p][q)c are equivalent. We prove that. the sec­ ond term subsumes the first by applying the sat.isfiabilit.y algorithm to [(p)q)c t\ -,[pj[q] c.

The initial constraint set for this input term consists of the two constraints

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

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

Now depth(b, r) = 2 = depth(f, 10 ) + l(p)ql. For this reason, we have to make a recursive call of the function apply-rules to determine whether the o· -rule fires for ( 1) and b.

In this recursive call we consider the constraints (3) and (5) together with the new negated role constraint. (7) 10 : [pj+q : b. (The alternative /0 : [p)_i also leads to unsatisfiable.) Now the 0·-rule becomes applicable for (7) and a. In fact, the recursive call of apply-rules with the constraint (3) and the new negated role con­ straint (8) 10 : p : a immediately returns unsatisfiable. Application of the 0· -rule for (7) and a yields the new constraint (9) a: q: b, which dashes with (5) . Thus the first recursive call also yields unsatisfiable.

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

In [2) it is 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 M(c), which depends linearly on the size of the input term c. It should be noted that both properties strongly depend on our restriction that ( ... )-operators are not allowed at the role term level. The fact that labels are of bounded depth plays an important role in the proof of termination .

Theorem 3.4 The satisfiability algorithm described above terminates for all restricted serial M -A.CC concept terms. If it returns unsatisfiable then the input term is in fact unsatisfiable.

A proof can be found in (2] . Unfortunately, we did not succeed in showing the opposite direction of the second statement, 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-A.CC .

The semantics of M-A.CC 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 for­ mulae one gets do not seem to fall into one of the known decidable subclasses of first-order logic. This is in con­ trast to A.CC where concept terms can be translated into formulae of the Godel class. Decidability of the satisfia­ bility problem in M-A.CC is still an open problem.

4 Summary and Open Problems

The present paper is a first. investigation of a new kind of multi-dimensional modal logic. The logic M-A.CC is a combination of modal logics Km, but the combination is of an unusual type. The modal operators of the com­ ponent 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 knowl­ edge 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 sat.isfiability problem for restricted serial M-A.CC terms . If the answer is no, decidabilit.y remains an open question .

More generally, one can ask whether the methods de­ scribed 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­ A.CC terms is decidable?

An adequate representation of modalities such as know, belief, or time require component logics that are stronger than Km; for example S4.3 for knowledge, lin­ ear structures for time etc. More generally, one can ask whether it is possible to modify the satisfiability algo­ rithm such that it can take additional modal axioms into account . A possible way of attacking this prob­ lem could be to translate the modal axiom schemas into properties of the accessibility relations (see [9]). Com­ plex 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 ofT-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)]?