The traditional description logics can be used for representing common and individual knowledge about the world (domain of application). Recently description logics have been extended to allow the representation of the knowledge and the beliefs of multiple agents in one knowledge base [3,11]. In MOTEL we formulate knowledge and belief as additional modal operators.

We are using [1] as a base
language.
That is,
we assume three disjoint alphabets,
the set of * concept names* * C*,
the set of * role names* * R*, and
the set of individual objects * O*.
The set of * concept terms* (or just * concepts*) and
* role terms* (or just * roles*) is inductively defined as
follows. Every concept name is a concept term and every role
name is a role term. Now assume that ` C`, ` D` are concepts,
and ` R`, ` S` are roles. Then
` and([C,D])`, ` not(C)`, ` some(R,C)`,
` atleast(n,R)`, ` atmost(n,R)`
are concept terms, and
` and([R,S])`, ` inverse(R)`, ` restrict(R,C)` are role terms.
The sentences of
are divided into * terminological sentences* and
* assertional sentences*.
If ` C` and ` D` are concepts and ` R` and ` S` are roles then
` defprimconcept(C,D)` and
` defprimrole(R,S)` are terminological
sentences.
If ` C` is a concept, ` R` is a role, and ` a`, ` b` are
individual objects
then ` assert_ind(a,C)` and ` assert_ind(a,b,R)`
are assertional sentences.
As in [1] we do not allow terminological cycles.

For the extended language Mod- we assume in addition that
we have an alphabet
* M* of * modal operator names*. Also, there is a distinguished
subset * A* of the individual objects, called the set of *
agents*.
We have a distinguished concept name `* all*' denoting
the set of all agents with which we express mutual belief.
The set of concepts and the set of roles of Mod- contains
all the concepts and roles of its sublanguage and in
addition it contains the
concepts ` b(m,a,C)`, ` d(m,a,C)`, ` bc(m,C,D)`, and
` dc(m,C,D)`. A * modal context* is a list of modal operators
of the form ` b(m,a)`, ` d(m,a)`, ` bc(m,C)`, and
` dc(m,C)`. If ` L` is a modal context,
` C` and ` D` are concepts and ` R` and ` S` are roles then
` defprimconcept(L,C,D)` and
` defprimrole(L,R,S)` are terminological
sentences in Mod-.
If ` C` is a concept, ` R` is a role, and ` a`, ` b` are
individual objects
then ` assert_ind(L,a,C)` and ` assert_ind(L,a,b,R)`
are assertional sentences in Mod-.

We use a translational approach to provide the usual inference mechanisms, i.e. solving the consistency, the subsumption, the instantiation and the realization problem. Obviously, knowledge bases can be translated into first-order logic theories. There are also well-known relational translation methods for modal logics. In [8] (also available as we have developed an improved translation method for Mod- which provides an elegant translation of knowledge bases into first-order logic theories. In a prototypical implementation, the MOTEL system, we use a Prolog-based system with loop-checking as inference machine.