Modalities in Knowledge Representation^{1}

Ullrich Hustadt and Andreas Nonnengart

Max-Planck-Institut für Informatik, Im Stadtwald, 66123 Saarbrücken, Germany

ABSTRACT

Standard knowledge representation systems are supposed to be able to represent either common or individual knowledge about the world. In this paper we propose an extension to such knowledge representation systems which, in a uniform manner, allows to express beliefs of multiple agents as well as knowledge, desire, time and in fact any modality which has a first-order predicate logic possible world semantics.

1 Introduction

Since the mid-seventies a variety of knowledge representation systems in the tradition of semantic networks and terminological logics has been proposed. The most famous example is KL-ONE^{3} which first appeared in 1977 in R. J. Brachman’s Ph.D. thesis. Other examples are KRYPTON^{2}, NIKL^{14}, LOOM^{8} and KRIS^{1}.

All these systems can be used to represent common or individual knowledge about the world. Recently, terminological logics have been extended to allow the representation of the knowledge or the beliefs of multiple agents in one knowledge base^{4, 7}.

In this paper, we investigate such an extension which allows not only to represent either knowledge or beliefs of multiple agents but a huge variety of modal operators for multiple agents.

The approach described is implemented in the MOTEL knowledge representation system. MOTEL was developed at the Max-Planck-Institute for Computer Science and is currently used at the University of Saarbrücken^{6}.

2 Syntax and Semantics for Mod-ALC

We assume four disjoint alphabets, the primitive concepts C, the primitive roles R, the set M of modal operator names, and the individual objects O. In particular, there is a distinguished subset A of the individual objects, called the set of agents, containing the special agent all which is supposed to denote the union of all the agents in order to be able to express mutual belief. The tuple (O, A, M, C, R) is called the signature, denoted by Σ.

1To appear in “Proceedings of the 1993 Australian Joint Conference on Artificial Intelligence”

The set of concept terms (or just concepts) and role terms (or just roles) is inductively defined as follows. Every primitive concept is a concept term and every primitive role is a role term. Now assume that C, C_{1}, and C_{2} are concepts, R, R_{1}, and R_{2} are roles, m is a modal operator name, a is an agent’s name. Then C_{1} ⊓ C_{2}, C_{1} ⊔ C_{2}, ¬C, ∀ R.C, ∃ R.C, □_{(m,a)} C, and ◇_{(m,a)} C are concept terms, and R_{1} ⊓ R_{2}, R^{−1}, RC, □_{(m,a)} R and ◇_{(m,a)} R are role terms.

Thus we are now able to describe the sentences of our language Mod-ALC which are divided into terminological sentences and assertional sentences. If C_{1} and C_{2} are concepts and R_{1} and R_{2} are roles then C_{1} ⊑ C_{2}, C_{1} ≡ C_{2}, R_{1} ⊑ R_{2}, R_{1} ≡ R_{2} are terminological sentences. If C is a concept, R is a role, and O, O_{1}, and O_{2} are individual objects then O ∈ C and (O_{1}, O_{2}) ∈ R are assertional sentences. Moreover, if Φ is a terminological (respectively assertional) sentence and if m is a modal operator name and a is an agent’s name then □_{(m,a)} Φ and ◇_{(m,a)} Φ are terminological (respectively assertional) sentences.

So far the syntax of Mod-ALC has been described. Now we have to provide its semantics.

Definition 1 (Σ-Structures) As usual we define a Σ-structure as a pair (D, I) which consists of a domain D and an interpretation function I which maps the individual objects to elements of D, primitive concepts to subsets of D and the primitive roles to subsets of D × D.

Definition 2 (Frames and Interpretations) By a frame F we understand any pair (W, ℜ) where

• W is a non-empty set (of worlds).

• ℜ = ⨄_{m∈M,a∈A} ℜ_{m}^{a} where the ℜ_{m}^{a}’s are binary relation on W, the so-called accessibility relations between worlds.

By a Σ-interpretation ℑ based on F we understand any tuple (D, F, ℑ_{loc}, ϵ) where

• D denotes the common domain of all Σ-structures in the range of ℑ_{loc}.

• ϵ denotes the actual world (the current situation)

• F is a frame

• ℑ_{loc} maps worlds to Σ-structures with common domain D which interpret agents’ names equally.

Definition 3 (Interpretation of Terms) Let ℑ = (D, F, ℑ_{loc}, ϵ) be a Σ-interpretation and let ℑ_{loc}(ϵ) = (D, I). We define the interpretation of terms inductively over their structure:

ℑ(C)  = I(C)
ℑ(R)  = I(R)

if C (R) is a primitive concept (role)

ℑ(C_{1} ⊓ C_{2}) = ℑ(C_{1}) ∩ ℑ(C_{2})

ℑ(C_{1} ⊔ C_{2}) = ℑ(C_{1}) ∪ ℑ(C_{2})
ℑ(¬C)  = D \ ℑ(C)
ℑ(∀ R.C) = {d ∈ D | e ∈ ℑ(C) for all e with (d, e) ∈ ℑ(R)}
ℑ(∃ R.C) = {d ∈ D | e ∈ ℑ(C) for some e with (d, e) ∈ ℑ(R)}
ℑ(□_{(m,a)} C) = {d ∈ D | d ∈ ℑ[χ](C) for all χ with ℜ_{m}^{a}(ϵ, χ)}
ℑ(◇_{(m,a)} C) = {d ∈ D | d ∈ ℑ[χ](C) for some χ with ℜ_{m}^{a}(ϵ, χ)}
ℑ(R_{1} ⊓ R_{2}) = ℑ(R_{1}) ∩ ℑ(R_{2})
ℑ(R^{−1})  = {(x, y) ∈ D × D | (y, x) ∈ ℑ(R)}
ℑ(RC)  = {(x, y) ∈ ℑ(R) | y ∈ ℑ(C)}
ℑ(□_{(m,a)} R) = {(x, y) | (x, y) ∈ ℑ[χ](R) for all χ with ℜ_{m}^{a}(ϵ, χ)}
ℑ(◇_{(m,a)} R) = {(x, y) | (x, y) ∈ ℑ[χ](R) for some χ with ℜ_{m}^{a}(ϵ, χ)}

where ℑ[χ] = (D, F, ℑ_{loc}, χ)

Definition 4 (Satisfiability) Let ℑ = (D, F, ℑ_{loc}, ϵ) be a Σ-interpretation. We define the satisfiability relation ⊧ inductively over the structure of Mod-ALC sentences:

ℑ ⊧ C_{1} ⊑ C_{2} iff ℑ(C_{1}) ⊆ ℑ(C_{2})
ℑ ⊧ C_{1} ≡ C_{2} iff ℑ(C_{1}) = ℑ(C_{2})
ℑ ⊧ R_{1} ⊑ R_{2} iff ℑ(R_{1}) ⊆ ℑ(R_{2})
ℑ ⊧ R_{1} ≡ R_{2} iff ℑ(R_{1}) = ℑ(R_{2})
ℑ ⊧ x ∈ C  iff I(x) ∈ ℑ(C)
ℑ ⊧ (x, y) ∈ R iff (I(x), I(y)) ∈ ℑ(R)
ℑ ⊧ □_{(m,a)} Φ iff ℑ[χ] ⊧ Φ for every χ with ℜ_{m}^{a}(ϵ, χ)
ℑ ⊧ ◇_{(m,a)} Φ iff ℑ[χ] ⊧ Φ for some χ with ℜ_{m}^{a}(ϵ, χ)

Definition 5 Let ℑ be an interpretation and let Φ be a Mod-ALC sentence with ℑ ⊧ Φ. Then we call Φ satisfiable and we call ℑ a model for Φ. If all interpretations are models for Φ then we call Φ a theorem. Any sentence for which no model exists is called unsatisfiable. Thus, Φ is a theorem iff its negation is unsatisfiable.

Let T be a set of Mod-ALC sentences. We say T entails Φ, written T ⊧ Φ, iff every model of T is a model of Φ.

So far we did not consider any special properties of the given modal operators. Typical axiom schemata which reflect such potential additional properties are listed below.

Axiom Schema Property □_{(m,a)} Φ ⇒ ◇_{(m,a)} Φ  ∀x∃y ℜ_{m}^{a}(x, y)

□_{(m,a)} Φ ⇒ Φ  ∀x ℜ_{m}^{a}(x, x)
Φ ⇒ □_{(m,a)} ◇_{(m,a)} Φ  ∀x, y ℜ_{m}^{a}(x, y) ⇒ ℜ_{m}^{a}(y, x)
□_{(m,a)} Φ ⇒ □_{(m,a)} □_{(m,a)} Φ ∀x, y, z ℜ_{m}^{a}(x, y) ∧ ℜ_{m}^{a}(y, z) ⇒ ℜ_{m}^{a}(x, z)
◇_{(m,a)} Φ ⇒ □_{(m,a)} ◇_{(m,a)} Φ ∀x, y, z ℜ_{m}^{a}(x, y) ∧ ℜ_{m}^{a}(x, z) ⇒ ℜ_{m}^{a}(y, z)

Table 1: Properties of the accessibility relation Historically, these properties are called D, T, B, 4, and 5 respectively.

If we consider modal operators for belief, i.e. □_{(believe,a)} and ◇_{(believe,a)}, then 4 and 5 are axioms of introspection. Intuitively, they say that the agent a has complete insight what his own beliefs are concerned. Property T is one of the major characteristics of modal operators for knowledge, i.e. □_{(knows,a)} and ◇_{(knows,a)}, because it enables us to deduce a fact about the real world from an agent’s knowledge about the world.

Definition 6 Let R be a set of properties of the accessibility relation. An interpretation ℑ is called a R-interpretation if the accessibility relation ℜ of the underlying frame F satisfies all properties in R. We say a set of Mod-ALC sentences T entails Φ in all R-interpretations if all R interpretations which are models of T are also models of Φ.

What is remarkable for the properties from above is that they all are first-order properties. Therefore it is not too surprising that a translation of modal terminological and modal assertional axioms into first-order predicate logic can be done very easily.

3 Translating Mod-ALC into Classical Logic

There have been a lot of proposals for correct and complete calculi for nonclassical logics — temporal logics^{13}, epistemic logics^{9}, etc. — and terminological logics^{3, 5}.

Unfortunately, these calculi require implementations for their respective theorem proving system with hardly a chance to apply results and techniques of the traditional work on automated theorem proving. Therefore, we follow the approach of Ohlbach^{12} to eliminate modal operators in a way that we get standard first-order predicate logic formulae that still represent the modal semantics.

In this section we define such a logic morphism that maps Mod-ALC into firstorder predicate logic.

First, we transform all concepts and roles which occur in a given knowledge base into negation normal form, i.e. in a form where no implication or equivalence sign occurs and where all negation signs occur solely in front of the primitive concepts. This can be performed in a straightforward manner as known from classical logic and therefore the technical details are omitted here. In the sequel we assume that any (terminological or assertional) sentence is already in negation normal form.

Now we translate the terminological and assertional sentences into first-order logic formulae using the function [[ ]].

Axiom  Translation
[[ □_{(m,a)}M_{2} … M_{n}Φ ]]_{U} ∀V : ℜ_{m}^{a}(U, V) ⇒ [[ M_{2} … M_{n}Φ ]]_{V}
[[ ◇_{(m,a)}M_{2} … M_{n}Φ ]]_{U} ∃V : ℜ_{m}^{a}(U, V) ∧ [[ M_{2} … M_{n}Φ ]]_{V}
[[ C_{1} ⊑ C_{2} ]]_{U}  ∀ X : [[ C_{1} ]]_{U,X} ⇒ [[ C_{2} ]]_{U,X}
[[ C_{1} ≡ C_{2} ]]_{U}  [[ C_{1} ⊑ C_{2} ]]_{U} ∧ [[ C_{2} ⊑ C_{1} ]]_{U}
[[ R_{1} ⊑ R_{2} ]]_{U}  ∀ X, Y : [[ R_{1} ]]_{U,(X,Y)} ⇒ [[ R_{2} ]]_{U,(X,Y)}

\begin{matrix}[[ R_{1} ≡ R_{2} ]]_{U} & [[ R_{1} ⊑ R_{2} ]]_{U} ∧ [[ R_{2} ⊑ R_{1} ]]_{U} \\ [[ a ∈ A ]]_{U} & [[ A ]]_{U,a} \\ [[ (a, b) ∈ P ]]_{U} & [[ P ]]_{U,(a,b)} \end{matrix}

where the translation of concepts and roles is defined by:

Term  Translation
[[ A_{1} ]]_{U,X}  A_{1}(U, X)
[[ ¬A_{1} ]]_{U,X}  ¬A_{1}(U, X)
[[ C_{1} ⊓ … ⊓ C_{k} ]]_{U,X}  [[ C_{1} ]]_{U,X} ∧ … ∧ [[ C_{k} ]]_{U,X}
[[ C_{1} ⊔ … ⊔ C_{k} ]]_{U,X}  [[ C_{1} ]]_{U,X} ∨ … ∨ [[ C_{k} ]]_{U,X}
[[ ∀ R.C ]]_{U,X}  ∀Y : [[ R ]]_{U,(X,Y)} ⇒ [[ C ]]_{U,Y}
[[ ∃ R.C ]]_{U,X}  ∃Y : [[ R ]]_{U,(X,Y)} ∧ [[ C ]]_{U,Y}
[[ □_{(m,a)} C ]]_{U,X}  ∀V : ℜ_{m}^{a}(U, V) ⇒ [[ C ]]_{V,X}
[[ ◇_{(m,a)} C ]]_{U,X}  ∃V : ℜ_{m}^{a}(U, V) ∧ [[ C ]]_{V,X}
[[ P ]]_{U,(X,Y)}  P (U, X, Y)
[[ R_{1} ⊓ … ⊓ R_{l} ]]_{U,(X,Y)} [[ R_{1} ]]_{U,(X,Y)} ∧ … ∧ [[ R_{l} ]]_{U,(X,Y)}
[[ R^{−1} ]]_{U,(X,Y)} [[ R ]]_{U,(Y,X)}
[[ RC ]]_{U,(X,Y)}  [[ R ]]_{U,(X,Y)} ∧ [[ C ]]_{U,Y}
[[ □_{(m,a)} R ]]_{U,(X,Y)}  ∀V : ℜ_{m}^{a}(U, V) ⇒ [[ R ]]_{V,(X,Y)}
[[ ◇_{(m,a)} R ]]_{U,(X,Y)}  ∃V : ℜ_{m}^{a}(U, V) ∧ [[ R ]]_{V,(X,Y)}

Thus given any Mod-ALC-formula Φ, the result of the above translation, [[ Φ ]]_{ϵ} is a first-order predicate logic formula which can easily be transformed into clause normal form with the help of the well-known standard techniques. The translation of a knowledge base is completed by adding a suitable set K of properties from table 1.

In order to prove that a modal terminological or modal assertional axiom Φ is satisfiable in any model of a knowledge base B, we have to show the unsatisfiability of [[ B ]] ∪ K ∪ [[ ¬Φ ]]_{ϵ}. Evidently, this can be done very easily with the help of any sound and complete theorem proving method for classical first-order predicate logic.

However, if we take a closer look at the results of the translation described above we can see quite a big problem. Already simple knowledge bases result in rather huge clause sets where many of the clauses merely express certain informations about accessibilities and role correlations. But we can exploit a property of the language Mod-ALC which is typical for most modal and terminological logics, namely, each accessibility relation symbol or role symbol R occurs either in the form ∃x R(…, x)∧ Φ(x) or in the form ∀x R(…, x) ⇒ Φ(x). How we can make use of this special syntactical feature is explained in the following section.

4 Functional Simulation of n-ary Predicates

First of all let us define what we mean by a functional simulator.

Definition 7 (Functional Simulators)

Let ℜ be an n-ary relation. A set F_{ℜ} of functions is called a functional simulator for ℜ if for any x_{1}, …, x_{n}

ℜ(x_{1}, …, x_{n}) iff there exists a f ∈ F_{ℜ} with f(x_{1}, …, x_{n−1}) = x_{n}

In particular, if ℜ is total, i.e. for any x_{1} … x_{n−1} there is a x_{n} such that ℜ(x_{1}, …, x_{n}) then each function in F_{ℜ} is total, too.

I.e. a functional simulator for some relation R is a set of functions which is able to take over the responsibilities of R. The following lemma shows that its cardinality does not exceed the cardinality of worlds under consideration.

Lemma 4.1 Let ℜ ⊆ S_{1} × … × S_{n} where each S_{i} denotes a countable sort. Then there exists a countable functional simulator for ℜ. Proof: See^{11}.

What a functional simulator is on the meta-level are the simulator axioms on the object level.

Definition 8 (Simulator Axioms for Total Predicates) According to Definition 7 we call the two axioms

Sim_{1}^{R} = ∀u_{i}, v R(…, u_{i}, …, v) ⇒ ∃f: F_{R} f(…, u_{i}, …) = v
Sim_{2}^{R} = ∀u_{i}∀f: F_{R} R(…, u_{i}, …, f(…, u_{i}, …))

the simulator axioms for the total predicate R. Note that in the case of non-total predicates the definition of Sim_{2}^{R} needs to be changed because in this case we have to be able to deal with partial functions instead of total functions.

The collection of all axioms Sim_{1}^{R}, respectively Sim_{2}^{R}, is called Sim_{1}, respespectively Sim_{2}.

Thus, for any total (serial) accessibility relation or role we can introduce functional simulators. This allows an alternative definition for the translation into firstorder predicate logic as described below.

Definition 9 (An Alternative for [[ Φ ]]_{ϵ}) The alternative for [[ Φ ]]_{ϵ} differs from [[ Φ ]]_{ϵ} merely in the following cases where the associated accessibility relations and role relations are assumed to be total.

\begin{aligned}[[ ◇_{(m,a)}Φ ]]_{U}^{⋆} & = & ∃V: F_{ℜ_{m}^{a}} [[ Φ ]]_{V (U)}^{⋆} \\ [[ ◇_{(m,a)} C ]]_{U,X}^{⋆} & = & ∃V: F_{ℜ_{m}^{a}} [[ C ]]_{V (U),X}^{⋆} \\ [[ ◇_{(m,a)} R ]]_{U,(X,Y)}^{⋆} & = & ∃V: F_{ℜ_{m}^{a}}[[ R ]]_{V (U),(X,Y)}^{⋆} \end{aligned}

Note that although the syntax of the translation suggests a second-order quantification we actually do not go beyond first-order logic.

Lemma 4.2 Let R be a set of formulae which expresses the properties of the underlying accessibility relations. Then

R ⊧ [[ Φ ]]_{ϵ} iff R ∪ {Sim_{2}} ⊧ [[ Φ ]]_{ϵ}^{⋆}

Proof: Can be found in^{11}

We have gained quite a lot already, however, under these preliminaries very interesting simplifications are possible.

Note that the clause form of such a translation does not contain any positive occurrence of a role or accessibility relation symbol. This fact can be exploited in a very interesting manner. Since any role or accessibility relation symbol can only occur in the additional axioms we can examine these independently from the translated formula. Nonnengart^{11} presents extremely good simplifications for various modal logics. So, for instance, the whole theory for the modal logic KD45 (i.e. the accessibility relation is serial, transitive and euclidean) can be simplified to the almost trivial unit clause R(U, V (W)). For those readers familiar with KD45 this might not be too surprising since the class of frames which are characteristic for KD45 are just those frames which consist of a single equivalence class or a world followed by an equivalence class such that this world has access to all the elements in this class. Other examples for suitable simplifications are e.g. the logic KDB (i.e. the accessibility relation is serial and symmetric). The set of theory clauses to be added to the translation of given formula consists just of the two simple unit clauses R(U, X(U)) and R(X(U), U) and nothing else is necessary.

In the following theorem we suppose that we have some simplification Sim which can be applied to a set R of formulae expressing the properties of the accessibility relation such that

R ∪ {Sim_{2}} ⊧ [[ Φ ]]_{ϵ}^{⋆} iff Sim(R) ∪ {Sim_{2}} ⊧ [[ Φ ]]_{ϵ}^{⋆}

Theorem 1 Let Φ be a Mod-ALC sentence and T a set of Mod-ALC sentences. Let R be a set of formulae which express the properties of the underlying accessibility relation. Then

T ⊧_{R} ϕ

iff

⋃_{Ψ∈T} [[ Ψ ]]_{ϵ}^{⋆} ∪ Sim(R) ∪ {Sim_{2}} ⊧ [[ Φ ]]_{ϵ}^{⋆}

iff

[[ Φ ]]_{ϵ}^{⋆} is provable from ⋃_{Ψ∈T} [[ Ψ ]]_{ϵ}^{⋆} ∪ Sim(R) ∪ {Sim_{2}} using some theorem prover which is correct and complete for first-order logic with equality.

5 An Example

Suppose Bob is a car seller and Tim is a customer. Tim tells Bob that he wants to buy a nice car and for some reason he believes that red cars are very nice. Bob has told Tim that he can offer a magenta colored audi. Of course, it is common believe, that magenta is a red color and that the audi is a car. This situation can be represented by the following knowledge base.

□_{(believe,bob)}□_{(believe,tim)} audi colored magenta
□_{(believe,all)}  magenta ∈ red
□_{(believe,all)}  audi ∈ car
□_{(believe,bob)}□_{(believe,tim)} car ⊓ ∃ colored.red ⊑ nice car
□_{(believe,bob)}  □_{(believe,tim)} nice car ⊑ □_{(want,tim)} buy car

From this knowledge base it follows that Bob believes that Tim wants to buy the audi, i.e.

□_{(believe,bob)}(audi ∈ □_{(want,tim)} buy car)

should be provable.

The translation of the knowledge base results in the following clauses:

colored(V, audi, magenta) ⇐ ℜ_{believe}^{bob}(ϵ, U) ∧ ℜ_{believe}^{tim}(U, V)  (1)
red(U, magenta) ⇐ ℜ_{believe}^{all}(ϵ, U)  (2)
car(U, audi) ⇐ ℜ_{believe}^{all}(ϵ, U)  (3)
nice car(V, X) ⇐ ℜ_{believe}^{bob}(ϵ, U) ∧ ℜ_{believe}^{tim}(U, V) ∧
colored(V, X, Y) ∧ red(V, Y) ∧
car(V, X)  (4)
buy car(V, X) ⇐ ℜ_{believe}^{bob}(ϵ, U) ∧ ℜ_{want}^{tim}(U, V) ∧
nice car(f_{believe}^{tim}(U), X)  (5)

We assume both consistency and full introspection for the agents’ beliefs. In this case we are allowed to simplify the theory clauses for the modal operator to^{11}:

ℜ_{believe}^{X}(U, Y_{believe}^{X}(V)) ⇐  (6)

where X ranges over the set of agents (i.e. Bob and Tim). The special agent all is therefore a KD45-operator as well, which ranges over all agents, thus:

ℜ_{believe}^{all}(U, Y_{believe}^{X}(V)) ⇐  (7)

For the want-operator, however, we do not assume anything in particular, merely consistency of what is wanted:

ℜ_{want}^{X}(U, Y_{want}^{X}(U)) ⇐  (8)

Finally, we get as the negated theorem:

⇐ buy car(h_{want}^{tim}(g_{believe}^{bob}(ϵ)), audi)  (9)

Because all axioms are Horn clauses, we can even use PROLOG to prove our theorem. The linear derivation of the goal is:

⇐ buy car(h_{want}^{tim}(g_{believe}^{bob}(ϵ)), audi)

⇐ ℜ_{believe}^{bob}(ϵ, U) ∧ ℜ_{want}^{tim}(U, h_{want}^{tim}(g_{believe}^{bob}(ϵ))) ∧ nice car(f_{believe}^{tim}(U), audi)

using axiom 5

⇐ nice car(f_{believe}^{tim}(g_{believe}^{bob}(ϵ)), audi)

using axioms 6 and 8

⇐ ℜ_{believe}^{bob}(ϵ, U) ∧ ℜ_{believe}^{tim}(U, f_{believe}^{tim}(g_{believe}^{bob}(ϵ))) ∧

colored(f_{believe}^{tim}(g_{believe}^{bob}(ϵ)), audi, Y) ∧ red(f_{believe}^{tim}(g_{believe}^{bob}(ϵ)), Y) ∧

car(f_{believe}^{tim}(g_{believe}^{bob}(ϵ)), audi)

using axiom 4

⇐ colored(f_{believe}^{tim}(g_{believe}^{bob}(ϵ)), audi, Y) ∧ red(f_{believe}^{tim}(g_{believe}^{bob}(ϵ)), Y) ∧

car(f_{believe}^{tim}(g_{believe}^{bob}(ϵ)), audi)

using axioms 6 twice

⇐ ℜ_{believe}^{bob}(ϵ, U) ∧ ℜ_{believe}^{tim}(U, f_{believe}^{tim}(g_{believe}^{bob}(ϵ)))∧

red(f_{believe}^{tim}(g_{believe}^{bob}(ϵ)), magenta) ∧ car(f_{believe}^{tim}(g_{believe}^{bob}(ϵ)), audi)

using axiom 1

⇐ red(f_{believe}^{tim}(g_{believe}^{bob}(ϵ)), magenta) ∧ car(f_{believe}^{tim}(g_{believe}^{bob}(ϵ)), audi)

using axioms 6 twice

⇐ ℜ_{believe}^{all}(ϵ, f_{believe}^{tim}(g_{believe}^{bob}(ϵ))) ∧ car(f_{believe}^{tim}(g_{believe}^{bob}(ϵ)), audi)

using axiom 2

⇐ car(f_{believe}^{tim}(g_{believe}^{bob}(ϵ)), audi)

using axiom 7

⇐ ℜ_{believe}^{all}(ϵ, f_{believe}^{tim}(g_{believe}^{bob}(ϵ)))

using axiom 3 success

using axiom 7

6 Conclusion and Further Work

We presented an approach which allows to reason within modal terminological logics by utilizing an appropriate translation technique into first-order predicate logic. The main idea behind this method is the functional simulation of accessibility relations and roles by suitable sets of functions. This turns out to have two main advantages: it decreases the size and the number of clauses and it allows significant simplifications on the set of theory clauses.

A necessary condition for the method proposed here to work is that the accessibility relation properties have to be first-order predicate logic definable. Unfortunately, not all modal logics have a first-order describable frame property.

Until now, we have only worked out the optimization for those modalities which have a simple possible world semantics. If the interaction of multiple modalities requires the more complex neighbourhood semantics, we have to rely on the straightforward translation which will result in a rather large number of clauses. Looking for optimizations for this case is part of future work. Besides, the extension of the system by number restrictions is one of the major future goals.

References

1. F. Baader and B. Hollunder. KRIS: Knowledge Representation and Inference System — System Description —. Technical Memo DFKI-TM-90-03, Deutsches Forschungszentrum für Künstliche Intelligenz, 1990.

2. R. J. Brachman, V. P. Gilbert, and H. J. Levesque. An Essential Hybrid Reasoning System: Knowledge and Symbol Level Accounts of krypton. In Proceedings of the Ninth International Joint Conference on Artificial Intelligence, pages 532–539, Los Angeles, California, 1985.

3. R. J. Brachman and J. G. Schmolze. An Overview of the klone Knowledge Representation System. Cognitive Science, 9(2):171–216, 1985.

4. F. M. Donini, M. Lenzerini, D. Nardi, A. Schaerf, and W. Nutt. Adding Epistemic Operators to Concept Languages. In B. Nebel, C. Rich, and W. Swartout, editors, Proceedings of the Third International Conference on Principles of Knowledge Representation and Reasoning, pages 342–353, San Mateo, CA, 1992. Morgan Kaufmann.

5. B. Hollunder and W. Nutt. Subsumption Algorithms for Concept Languages. Research Report DFKI-RR-90-04, Deutsches Forschungszentrum für Künstliche Intelligenz, 1990.

6. U. Hustadt, A. Nonnengart, R. Schmidt, and J. Timm. MOTEL User Manual. Internal report MPI-I-92-236, Max-Planck-Institute for Computer Science, June 1992.

7. A. Kobsa. Towards Inferences in BGP-MS: Combining Modal Logic and Partition Hierarchies for User Modeling (Preliminary Report). Bericht WIS-2, Projekt BGP-MS, Universität Konstanz Informationswissenschaft, Postfach 5560, 7750 Konstanz, Juni 1992. Proceedings of the Third International Workshop on User Modeling, Schloss Dagstuhl, Germany, Aug. 10–13, 1992.

8. R. M. MacGregor. Inside the LOOM Description Classifier. SIGART Bulletin, 2(3):88–92, 1991. Special Issue on Implemented Knowledge Representation and Reasoning Systems.

9. R. C. Moore. Autoepistemic Logic. In Ph. Smets, E. H. Mamdani, D. Dubois, and H. Prade, editors, Non-Standard Logics for Automated Reasoning. Academic Press, London, 1988.

10. J. Mylopoulos and M. Brodie, editors. Readings in Artificial Intelligence and Databases. Morgan Kaufmann, San Mateo, CA, 1989.

11. A. Nonnengart. First-Order Modal Logic Theorem Proving and Standard PRO-LOG. Internal report MPI-I-92-228, Max-Planck-Institute for Computer Science, July 1992.

12. H. J. Ohlbach. A Resolution Calculus for Modal Logics. PhD thesis, Universität Kaiserslautern, October 1988.

13. N. Rescher and A. Urquhart. Temporal Logic. Springer, Berlin, 1971.

14. J. G. Schmolze. The Language and Semantics of nikl. Technical Report 89–4, Department of Computer Science, Tufts University, Medford, MA, 1989.