First-Order Modal Logic Theorem Proving and Functional Simulation

Andreas Nonnengart

Max-Planck-Institute for Computer Science Im Stadtwald, 6600 Saarbrücken, Germany

Email: nonnenga@mpi-sb.mpg.de Tel.: (+49) 681 302 5369 Fax: (+49) 681 302 5401

Abstract

We propose a translation approach from modal logics to first-order predicate logic which combines advantages from both, the (standard) relational translation and the (rather compact) functional translation method and avoids many of their respective disadvantages (exponential growth versus equality handling). In particular in the application to serial modal logics it allows considerable simplifications such that often even a simple unit clause suffices in order to express the accessibility relation properties. Although we restrict the approach here to firstorder modal logic theorem proving it has been shown to be of wider interest, as e.g. sorted logic or terminological logic.

1 Introduction

Today’s calculi for modal logics can be divided into two main groups. The first group is concerned with the extension of already existing calculi for classical logic by suitable additional inference rules. Typical examples can be found in [Fitting, 1983] where the well known tableau calculus and the sequent calculus are appropriately extended and [Wallen, 1987] in which the connection method is utilized for reasoning within modal logics.

The other group tries to exploit the experience and progress made in the development of classical predicate logic calculi and defines a translation morphism from modal logics to classical logic such that calculi which are known to be efficient can be utilized. The simplest one of those certainly is the so-called relational translation method ([Moore, 1980]) which makes the implicit model semantics explicit in the translation. Its disadvantage lies in the size of the resulting formulae which get exponentially bigger than the original ones.

Based on Wallen’s ideas, Hans Jürgen Ohlbach and others ([Ohlbach, 1989; Ohlbach, 1991; Auffray and Enjalbert, 1992; Fariñas del Cerro and Herzig, 1988]) developed the functional translation approach which avoids exponential growth of the translated formulae.

Here the number of clauses and literals inside clauses is exactly as big as if the modal operators would have been ignored (although, of course, literals get bigger by the addition of extra arguments). The disadvantage of this approach lies in the handling of the modal theory (as e.g. reflexivity, transitivity, symmetry, directedness) which gets encoded by certain equations and thus requires a rather strong equality handling mechanism. However, some of these properties and their combinations allow for the definition of suitable theory unification procedures, although finding such an algorithm is indeed a non-trivial task.

The approach proposed in this paper can be viewed as a mixture between the relational and the functional translation method. It is tried to combine their respective advantages and to avoid their disadvantages if possible. To be more precise, it consists of both, a relational translation which does not result in an exponential growth in the number of clauses and a functional translation which does not require that the modal theory has to be described by (more or less untractable) equations.

This paper is organized as follows: Section 2 is a brief repetition of the modal logic syntax and model semantics. In addition it describes the relational translation formally. Section 3 is concerned with the definition of what we call a functional simulator and its application to the result of a relational translation. This result gives rise to some considerable simplifications which are exemplified in section 4. How this result can be extended to varying domains and multiple modalities is shown in section 4.6 and 4.7. Finally, in section 5, we summarize the effect of the approach.

2 Modal Logics

It is out of the scope of this paper to give an overview over modal logics in general. The reader not familiar with modal logics is referred to [Chellas, 1980] and [Hughes and Cresswell, 1968].

Nevertheless, at least the notions of interpretations and satisfiability have to be repeated briefly, since they will be needed in later sections.

By a modal logic interpretation ℑ_{M} we understand a tuple ((W, ℜ), ℑ_{loc}, τ, ϕ) where W is a non-empty set of worlds and ℜ is a binary accessibility relation between worlds, τ is one of these worlds (the actual world), ϕ is a variable assignment and ℑ_{loc} is a mapping from worlds to signature structures which consist of a domain and interpretations for the given function and predicate symbols.

For convenience let us start with a constant domain structure, i.e. we assume that the domains of the respective signature structures are all identical. Thus, if we refer to some domain D we mean the domain common to all signature structures. The case of varying domains will be handled in section 4.6. Definition 2.1 (Satisfiability) A modal logic interpretation ℑ_{M} = ((W, ℜ), ℑ_{loc}, τ, ϕ) is said to satisfy a formula Φ if ℑ_{M} ⊧_{M} Φ, where ⊧_{M} is recursively defined as follows:

ℑ_{M}(x)  = ϕ(x)
ℑ_{M}(f(…, t_{i}, …))  = f̂(…, ℑ_{M}(t_{i}), …)
ℑ_{M} ⊧_{M} P (…, t_{i}, …) iff P̂(…, ℑ_{M}(t_{i}), …)
ℑ_{M} ⊧_{M} □Φ  iff ℑ_{M}[χ] ⊧_{M} Φ for every

world χ with ℜ(τ, χ)

ℑ_{M} ⊧_{M} ◇Φ  iff ℑ_{M}[χ] ⊧_{M} Φ for some

world χ with ℜ(τ, χ)

where ℑ_{M}[χ] differs from ℑ_{M} only with respect to the new current world χ and f̂ (P̂) denotes the function (predicate) associated with f (P) by the signature structure ℑ_{loc}(τ). The cases for the logical connectives and quantifiers are just as in classical first-order predicate logic and are therefore omitted here.

The various modal logics known from the literature mainly differ in the properties associated with the respective accessibility relations. The most common accessibility relation properties are reflexivity, symmetry, transitivity, euclidity, seriality, directedness and linearity. All of these properties but one (linearity) will be handled in this paper.

2.1 Relational Translation The idea behind relational translation is to make the implicit semantical parts of modal logic explicit in the predicate logic variant of the given modal logic formula. Hence we assume a new sort W distinct from the domain sort D, a new constant ι which is supposed to represent the actual (or current) world, a relation symbol R which denotes the accessibility relation and, for every function and every predicate symbol f (P respectively) a new function symbol f′ (predicate symbol P′) which accepts one more argument than f (P), namely a world (or actually a term representing a world).

The following definition describes the formula morphism ⌊Φ⌋_{w} which accepts a modal logic formula Φ and a term w (which denotes a world) and results in a firstorder predicate logic formula. It can be viewed as a direct translation from the satisfiability definition 2.1 into classical logic. Definition 2.2 (The Formula Morphism ⌊Φ⌋_{w})

\begin{aligned}⌊x⌋_{w} & = & x \\ ⌊f(…, t_{i}, …)⌋_{w} & = & f′(w, …, ⌊t_{i}⌋_{w}, …) \\ ⌊P (…, t_{i}, …)⌋_{w} & = & P′(w, …, ⌊t_{n}⌋_{w}, …) \\ ⌊□Φ⌋_{w} & = & ∀v: W R(w, v) ⇒ ⌊Φ⌋_{v} \\ ⌊◇Φ⌋_{w} & = & ∃v: W R(w, v) ∧ ⌊Φ⌋_{v} \end{aligned}

The remaining cases are treated by the usual homomorphic extension. The initial call for the translation of an arbitrary formula Φ then simply is ⌊Φ⌋_{ι}.

This translation indeed behaves as desired. We formulize this by the theorem below. For a proof see e.g. [Moore, 1980; Ohlbach, 1989; Nonnengart, 1992]).

Theorem 2.3 Relational translation is sound and complete, i.e. a modal logic formula Φ is satisfiable if and only if ⌊Φ⌋_{ι} ∧ Axioms is (predicate logic) satisfiable, where Axioms denotes those formulae which stem from the additional properties of the accessibility relation of the modal logic under consideration (i.e. the accessibility relation properties).

The big disadvantage of this relational translation lies in the exponential growth of the resulting formulae such that already fairly simple theorems can hardly be proved because of the enormous search space. In the following section we therefore introduce an alternative translation method which has its origin in the functional translation approach, but is rather a mixture between functional and relational translation.

3 Functional Simulation

Given a binary predicate R it is possible to split R into predicates R_{1}, R_{2} … such that each of the R_{i} denotes a (partially) functional relation. Intuitively this can be done as follows: arrange the pairs which belong to R in a two-dimensional array such that every column is responsible for R-pairs with identical first element. Having completed this procedure the resulting field contains all element pairs of R and each row of this field represents a subrelation of R which is evidently (partially) functional by construction. Thus, instead of (or additionally to) reasoning with R we can reason with the respective subrelations from the above construction. Note that it is not really necessary to consider the so generated elements as relations (or partial functions). Since by construction there are no more of them than denumerably many (provided R is denumerable) we can equally consider a new sort of the same cardinality and a new function symbol which is supposed to denote something like the applyfunction.

The following section provides with a formal definition of such functional simulators and some of its most important properties.

3.1 Functional Simulators Definition 3.1 (Functional Simulators) Let S and T be two non-empty denumerable sets and let R be a non-empty binary relation over S × T. Then define for any pairs (x, y) and (u, v) in S × T: (x, y) ≈ (u, v) iff x = u. Obviously ≈ denotes an equivalence relation. It is thus possible to introduce equivalence classes [ ]_{≈} by:

[(x, y)]/_{≈} = {(u, v) ∈ R | (x, y) ≈ (u, v)}

and

R/_{≈} = {[(x, y)]/_{≈} | (x, y) ∈ R}

Both [(x, y)]/_{≈} and R/_{≈} are denumerable, therefore there exist surjective mappings θ : Nat → R/_{≈} and δ_{i} : Nat → θ(i). Then define f_{j} = {δ_{k}(j) | k ∈ Nat}. We call F_{R} = {f_{j} | j ∈Nat} a functional simulator of R on S × T. An element s ∈ S is called normal w.r.t. R if there exists a t ∈ T such that (s, t) ∈ R.

Now, given a denumerable binary relation R over S×T and a functional simulator F_{R} of R we know by construction that

• F_{R} denotes a denumerable set of partial functions from S to T

• If u is normal w.r.t. R then for any f ∈ F_{R} f is defined on u and R(u, f(u)) holds.

• If R is left-total, then F_{R} consists of total functions and for any u∈S and any f ∈F_{R}: R(u, f(u)) holds.

• For any u ∈ S and any v ∈ T: if R(u, v) then there exists an f ∈F_{R} such that f(u) = v

3.2 Application to the Relational Translation In the sequel we assume that the modal logic formulae are already transformed into negation normal form, i.e. all implications and equivalences are removed and the negation signs occur solely in front of the atoms. Evidently, any modal logic formula can easily be transformed into an equivalent one which is in negation normal form.

For convenience we also assume in the sequel that we are dealing with serial modal logics unless otherwise stated. The case of non-serial modal logics will be broached in section 4.5.

Definition 3.2 (The Formula Morphism ⌊Φ⌋_{u}^{⋆}) Let Φ be a modal logic formula in negation normal form.

⌊◇Φ⌋_{u}^{⋆} = ∃f: F_{R} ⌊Φ⌋_{u:f}^{⋆}

In any other case ⌊Φ⌋_{u}^{⋆} behaves as ⌊Φ⌋_{u}.

The notation u:f is used for readability instead of apply(f, u). It is shorter and reflects the order of the ◇-operators in the original formula. Thus, for instance, the formula ◇◇P gets translated into ∃f: F_{R} ∃g: F_{R} P′(ι:g:f) where bracketing to the left is assumed.

According to the functional simulator properties described above we define the two simulator axioms Sim_{1} and Sim_{2} as:

Sim_{1} = ∀u, v: W R(u, v) ⇒ ∃x: F_{R} u:x = v

and Sim_{2} = ∀u: W ∀x: F_{R} R(u, u:x)

What has been gained so far? It is not too hard to see that the new formula morphism behaves as desired provided the two simulator axioms Sim_{1} and Sim_{2} are added to the clause set. But Sim_{1} introduces an equality and one might expect that equations devour all that has been gained so far.

Fortunately it is not that bad. As the following theorem shows this simulator axiom Sim_{1} is in fact superfluous and thus merely the unit clause from Sim_{2} has to be added to the clause set.

Theorem 3.3 Let M be a (serial) modal logic and let Φ be a M-formula. Then

⊧_{M} Φ iff Axioms ∧ Sim_{2} ⊧_{PL} ⌊Φ⌋_{ι}^{⋆}

where Axioms denotes the correspondence axioms for the modal logic M and ⊧_{PL} denotes the usual predicate logic satisfiablity relation. Proof: From Theorem 2.3 we know that

⊧_{M} Φ iff Axioms ⊧_{PL} ⌊Φ⌋_{ι}

Thus, and because of the fact that for any R there exists a suitable functional simulator, we obviously have that

⊧_{M} Φ iff Axioms ∧ Sim_{1} ∧ Sim_{2} ⊧_{PL} ⌊Φ⌋_{ι}^{⋆}

simply because under the assumption that F_{R} is a functional simulator of R (i.e. the simulator axioms hold), the two formulae ⌊Φ⌋_{ι} and ⌊Φ⌋_{ι}^{⋆} are logically equivalent. Remains to be shown that Sim_{1} is in fact superfluous. Written in clause form Sim_{1} gets: ¬R(u, v) ∨ u:f(u, v) = v where the symbol f is new to the whole clause set. As it is known from the area of equality reasoning, it is never necessary to paramodulate into or from variables. Therefore the equality from Sim_{1} needs to be applied only from left to right. However, as a simple induction shows, no term of the form α_{1}: …:α_{n} produced by the translation contains a universally quantified F_{R}-variable and thus, no application of the Sim_{1} equation from left to right is possible. Since the one direction is not possible and the other direction is not necessary we can simply forget about the whole clause and we are done.

We have gained quite a lot already: there is no exponential growth in the number of clauses any more (in fact, the number of clauses generated is exactly as big as if we entirely ignored the modal operators as can be shown by a simple induction; although the clauses themselves might get bigger of course) and the price to be paid is merely the addition of a simple unit clause, namely R(u, u:x) from Sim_{2}. Nevertheless, we can do even better.

Another fairly easy induction shows that the result of the translation of some arbitrary modal logic formula does not contain any positive R-literals. This is remarkable, for it allows to examine the theory clauses which stem from the properties of the underlying accessibility relation independently of the clauses produced by the translation. And this indeed leads to some further considerable simplifications.

4 Simplifications

The main idea behind the following simplifications is as follows: since we know that the translation of modal logic formulae into predicate logic produces clauses which do not contain any positive R-literals, the only possibility where we can have positive R-literals is via the accessibility relation properties, i.e. via Axioms and Sim_{2}.

Call a clause positive in R if it contains no negative R-literal and consider the set of clauses which are positive in R and which are derivable from Axioms and Sim_{2} by finitely many resolution steps. We call this set generated from Axioms and Sim_{2} then. Now it is not very hard to see that the set generated from Axioms and Sim_{2} suffices as the modal logic theory since any negative Rliteral which occurs in Axioms can only be resolved with the help of Axioms itself (and R(u, u:x) of course). This means that any clauses which generate the same set will do for our purposes as well. For more details see [Nonnengart, 1992].

In the following application to some well known modal logics we will make use of this fact. For historical reasons we name the various modal logics with the help of abbreviations for the respective accessibility relation properties. Hence D is used for seriality, B for symmetry, 4 for transitivity, 5 for euclidity, S4 for reflexivity plus transitivity and S5 for reflexivity plus euclidity.

4.1 The Logics KD and KDB Note that seriality is already covered by Sim_{2}. For KD there exists merely a single unit clause anyway and we are already done. For KDB a further unit clause can be derived between Sim_{2} and the symmetry clause which is R(u:x, u). Thus, a single unit clause for KD (namely R(u, u:x)) and two unit clauses for KDB (namely R(u, u:x) and R(u:x, u)) suffice for the description of the respective modal logic theory.

4.2 The Logics KD4 and S4 Here the set generated by Axioms and Sim_{2} is infinite. Nevertheless, its elements have a common structure which is R(u, u:x_{1} …:x_{n}) where n ≥ 0 for S4 and n ≥ 1 for KD4. It is thus very easy to find an alternative clause set which generates exactly the same set, namely the two-literal clause ¬R(u, v) ∨ R(u, v:x) plus R(u, u) for S4 and R(u, u:x) for KD4. The overall effect of this translation is therefore that at least the transitivity clause gets simplified.

4.3 The Logics KD5, KD45, and S5 For these logics the generated set consists of the clauses of the form R(u:x_{1} …:x_{n}, u:y_{1} …:y_{m}) where n, m ≥ 0 for S5, n ≥ 0 and m ≥ 1 for KD45, and n, m ≥ 1 for KD5. Again it would be very easy to find a suitable clause set which generates the same clauses and which is simpler than the original theory. However, we can do even better if we exploit a useful result known from the modal logic literature, namely that we are allowed to consider only worlds which are accessible from the initial world by finitly many R-steps. Thus, if we instantiate the u from above with ι and have in mind that any world whatsoever can be described in the form ι:y_{1} …:y_{m} for suitable instantiations of the y_{i} we get R(u, v) for S5, R(u, v:x) for KD45 and R(u:x, v:y) for KD5. These unit clauses for S5 and KD45 even subsume Sim_{2} and hence their respective theories are determined by a single unit clause. R(u:x, v:y) does not subsume R(u, u:x), nevertheless it can be used for a simplification getting R(ι, ι:x) (since all other cases are in fact subsumed by R(u:x, v:y). Note that these simplified versions nicely reflect Segerberg’s discovery ([Segerberg, 1971]) that S5 is characterized by the universal accessibility relation (a non-degenerate cluster; therefore R(u, v) for all worlds u, v) and that KD5 and KD45 are characterized by a single world followed by a non-degenerated cluster with the only difference that in the latter the single world has access to any world in the following cluster whereas in KD5 this is not necessarily the case. Hence, the theories for S5 and KD45 are described by a single unit clause respectively whereas the theory for KD5 requires two simple unit clauses.

4.4 Other Interesting Properties

R is called directed if any two worlds which have a common predecessor in R also have a common successor in R. The clause set generated by this formula and Sim_{2} is infinite. However, the special structure of translated formulae allows to take the simple unit clause

R(u:x, u:y:f(u, u:x, u:y))

as a substitute for the directedness axiom. This can be proved by showing that the application of any other generated unit clause can be replaced by several applications of R(u:x, u:y:f(u, u:x, u:y)). In fact, this unit clause nicely reflects our intention what the directedproperty is concerned for it states that for any two worlds u:x and u:y (which are both accessible from u) there is a world u:y:f(u, u:x, u:y) which can be accessed by u:x.

R is called dense if no world has a unique successor in R (different to this very world). By a similar argument to the above this property can be simplified to

R(u:g(u, u:x), u:x)

which states that for any u and any u:x accessible from u there is a world u:g(u, u:x) between u and u:x; just as we expected.

4.5 Non-Serial Modal Logics

In non-serial modal logics we are not any more allowed to assume that each world is normal with respect to the accessibility relation ℜ. Hence, the simple unit clause from Sim_{2} (which is R(u, u:x)) is not valid anymore since it might happen that x is not defined on u. Therefore, assume a new unary predicate N(u) which is supposed to denote “normality”. The simulator axiom Sim_{2} thus has to be changed to N(u) ⇒ R(u, u:x). Moreover, the information that certain worlds are normal has to be reflected in the formula morphism which becomes:

⌊◇Φ⌋_{u}^{⋆} = N(u) ∧ ∃f: F_{R} ⌊Φ⌋_{u:f}^{⋆}

Unfortunately, some of the nice results we got for serial modal logics are lost this way. So, for instance, we get again an exponential growth in the number of clauses after translation. Nevertheless, the simplifications from above still work provided some N-literals are added at appropriate places in the simplified clauses.

As an example consider the logic K45 which is characterized by either a single unconnected worlds or a frame as we know it already from KD45. Analogous to the argument for KD45 we get the theory clause R(u, v:x), ¬N(v), i.e. the successors of every normal world can be accessed by any world.

Again, the reader interested in more details is referred to [Nonnengart, 1992].

4.6 Varying Domains Recall that we assumed constant domains in the Definitions 2.1 and 2.2. If we want to take varying domains into account a further predicate has to be introduced, namely one which expresses existence of domain elements in given worlds. Thus the relational translation changes to

\begin{aligned}⌊∀x: D Φ⌋_{u} & = & ∀x: D E(u, x) ⇒ ⌊Φ⌋_{u} \\ ⌊∃x: D Φ⌋_{u} & = & ∃x: D E(u, x) ∧ ⌊Φ⌋_{u} \end{aligned}

where the predicate symbol E denotes “existence”. The other cases remain as in Definition 2.2. The idea is now to functionally simulate this E-predicate just as we did for the R-predicate before. Hence, let F_{E} be a functional simulator for E, the formula morphism changes to:

⌊∃x: D Φ⌋_{u}^{⋆} = ∃y: F_{E} ⌊Φ⌋_{u}^{⋆}[x/u:y]

where ⌊Φ⌋_{u}^{⋆}[x/u:y] means that every x in ⌊Φ⌋_{u}^{⋆} gets replaced by u:y. Note that we asume that no domain is empty and therefore each world is normal with respect to E. If there are no extra properties given for E then the theory is simply reflected by the simulator axiom E(u, u:x) where the x now ranges over F_{E}.

Usually, however, one is not really interested in arbitrary varying domains. Often one considers either increasing or decreasing domains, i.e. either nothing gets lost or no elements get newly generated. The axiom for increasing domains is

∀u, v: W ∀x: D E(u, x) ∧ R(u, v) ⇒ E(v, x)

Note that again the translation from above produces formulae whose clause normal forms do not contain any positive E-literals. We therefore look for a suitable simplification by examining the clauses generated by E(u, x) ∧ R(u, v) ⇒ E(v, x) and E(u, u:x). This results in

E(u, x) ⇒ E(u:v, x)

which states that if x exists in world u then it exists in any world accessible by u as well. Interestingly this theory clause is not only characteristic for increasing domains in the logic KD but also for KT, KD4 and S4. For the logics KD5 and KD45 we can get even simpler axioms because of their simple characteristic frames which guarantee identical domains everywhere but possibly for the actual world. This fact can easily be represented by the unit clause E(u:x, v:y) (where x ranges over F_{R} and y over F_{E}) which states that every domain element (denoted by v:y) is known to any world apart from the initial world ι. For ι itself we still have the unit clause E(u, u:x) which can thus be simplified to E(ι, ι:x).

Decreasing domains can be worked out in a similar manner. We omit here the technical details and just provide the result of the possible simplifications. For the logics KD, KT, KD4 and S4 we get the theory clauses E(u, u:y) and E(u:x, z) ⇒ E(u, z) where y ranges over F_{E} and x belongs to F_{R} and for KD5 and KD45 we get the two simple unit clauses E(ι, ι:x) and E(u, v:x:y) with the F_{E} element x and the F_{R} element y.

In the non-serial case we are again not allowed to ignore the “normality”-property. So, for instance, we get the clause N(u) ⇒ E(u:x, v:y) for K45 and K5, i.e. we have to assure that the F_{R}-variable x is indeed defined on u. This evidently has to be done for any of the above simplifications. We omit details here; the interested reader is referred to [Nonnengart, 1992].

4.7 Multiple Modalities

4.7.1 A Simple Temporal Logic

Consider two KD4-modalities □_{F} and □_{P} where □_{F} is responsible for the future and □_{P} for the past respectively. Moreover assume that there is only one thing said about their connection, namely that the associated accessibility relations (i.e. the “later”- and the “earlier”- relation) are converse. Thus we have as a theory axiom: R_{F} (u, v) ⇔ R_{P} (v, u) for any two worlds (time instants) u and v. This leads to the following “time-theory”:

R_{F} (u, u:x_{F})
R_{P} (u, u:x_{P})
R_{F} (u, v) ∧ R_{F} (v, w) ⇒ R_{F} (u, w)
R_{F} (u, v) ⇔ R_{P} (v, u)

Because of the equivalence between R_{F} (u, v) and R_{P} (v, u), it is not really necessary to consider both predicates, i.e. we can for instance, replace any occurrence of R_{P} in the translated formula as well as in the theory axioms by R_{F} provided the arguments are reversed. We thus get the theory axioms (where R is taken as a shortform for R_{F}):

R(u, u:x_{F})
R(u:x_{P} , u)
R(u, v) ∧ R(v, w) ⇒ R(u, w)

With this we can now start our simplification process which finally results in:

R(u, u:x_{F})
R(u:x_{P} , u)
R(u, v) ⇒ R(u, v:x_{F})
R(u, v) ⇒ R(u:x_{P} , v)

Whether or not these theory axioms should be prefered to those from above is not merely a matter of taste. It is indeed the case that the search space gets smaller in the simplified case because the positive R-literal of the transitivity axiom can unify with arbitrary negative Rliterals from the translated formula of the theory axioms whereas the latter theory clauses do restrict this.

4.7.2 Multiple Agents

The logic KD45 seems appropriate for the formulization of the Belief of Agents since it incorporates consistency of beliefs (seriality axiom) as well as positive and negative introspection (transitivity and euclidity axiom respectively).

Now assume a set of agents where each agent’s belief obeys the KD45 properties. A first idea would be to add the KD45 theory clause to the clause set for each of these agents. However, since this would mean that the KD45 properties hold over the whole world structure, we would automatically have that also each agent considers his own and the other’s agent’s beliefs as consistent with positive and negative introspection. If we do not want this, we have to assure that the KD45 properties only hold in the worlds which are accessible for the respective agents. This can be done with the help of a new predicate W which, given an agent and a world tells us whether this world is accessible for the agent or not. Formally: for all agents a and all x_{a} in F_{R_{a}}

\begin{matrix}W_{a}(ι) \\ W_{a}(u) ⇒ W_{a}(u:x_{a}) \end{matrix}

where u ranges over the worlds of the whole universe and x_{a} belongs to the functional simulator of R_{a} (agent a’s belief relation). Thus the respective agent’s theory of belief is then given by

W_{a}(u) ∧ W_{a}(v) ⇒ R_{a}(u, v:x_{a})

i.e. the KD45 axiom holds only for those worlds which are accecssible for agent a. For all other worlds we still have N_{a}(u) ⇒ R_{a}(u, u:x_{a}) which states that nothing else is assumed for the agent’s beliefs. Finally, we have to provide the correspondences between W and N which is simply given by: W_{a}(u) ⇒ N_{a}(u) (because of seriality).

Note that this technique also allows to express mutual beliefs of many agents. To this end, we introduce a mutual belief accessibility relation RMB which evidently must obey the KD45 properties as well (since each of the agents does). Thus the simple unit clause RMB(u, v:x_{a}) (for all agents a) will do for this purpose.

For more details on this issue the reader is again referred to [Nonnengart, 1992].

5 Summary

We proposed a translation method from modal logic into first-order predicate logic which allows a considerable simplification of the accessibility relation theory. This approach is some sort of a mixture between the standard relational translation approach and the functional translation method proposed by Ohlbach and others. It shows to behave particularly nice in the application to serial modal logics. So, e.g., the background theories for the modal logics KD, KD5, KD45, and S5 get so simple that even a direct incorporation into the translation morphism becomes possible.

A comparison between this approach and the fully functional translation might be interesting at this stage. For the logic KD both methods are identical as can easily be checked. For S5, KD45 and KD5 the mixed approach evidently works better (even if somebody is able to find some suitable theory unification algorithm for these theories) because of the simple background theory described by a single unit clause respectively. What the logics KDB, KD4 and S4 are concerned, we do not have a general answer yet. We have to distinguish between theorem provers which do allow the definition of arbitrary theory unification algorithms and those which don’t. In the latter case a rather strong equality handling mechanism is necessary for the functional translation approach and this might cause troubles for the prover. In the former case the functional translation approach will be more efficient in general. Nevertheless, we can think of some easy control strategy for the mixed approach in which resolution steps between non-R-literals are allowed only if the R-literals in the resolvent can be eliminated by the theory clauses. We did not yet implement this, however, there is some strong evidence that such a control strategy makes the mixed approach behave only slightly worse (in the worst case) compared to full functional translation. This method (as it stands now) can only be applied to modal logics which have first-order describable accessibility relation properties. Part of our future work will be to examine more properties and property combinations which might be useful and/or interesting.

References

[Auffray and Enjalbert, 1992] Yves Auffray and Patrice Enjalbert. Modal theorem proving: An equational viewpoint. Journal of Logic and Computation, 2(3):247 – 295, 1992.

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

[Fariñas del Cerro and Herzig, 1988] Luis Fariñas del Cerro and Andreas Herzig. Quantified modal logic and unification theory. Rapport LSI 293, Languages et Systèmes Informatique, Université Paul Sabatier, Toulouse, 1988.

[Fitting, 1983] Melvin Fitting. Proof Methods for Modal and Intuitionistic Logics. Reidel, 1983.

[Hughes and Cresswell, 1968] G. Hughes and M. Cresswell. An Introduction to Modal Logic. Menthuen, London, 1968.

[Kripke, 1962] Saul Kripke. Semantical considerations on modal logics. In Proceedings of a Colloquium on Modal and Many Valued Logics, Helsinki, 1962. Acta Philosophica Fennica, no 16.

[Kripke, 1963] Saul Kripke. Semantical analysis of modal logic: normal propositional calculi. Zeitschrift für Mathematische Logic und Grundlagen der Mathematik, 9, 1963.

[Moore, 1980] R. Moore. Reasoning About Knowledge and Action. PhD thesis, MIT, Cambridge, 1980. [Nonnengart, 1992] Andreas Nonnengart. First-order modal logic theorem proving and standard PROLOG. Technical Report MPI-I-92-228, Max-Planck-Institute for Computer Science, Saarbrücken, Germany, July 1992.

[Ohlbach, 1989] Hans Jürgen Ohlbach. A Resolution Calculus for Modal Logics. PhD thesis, University of Kaiserslautern, Germany, 1989.

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

[Segerberg, 1971] Krister Segerberg. An essay in classical modal logic. Technical Report 13, University of Uppsala, Filosofiska Studier, 1971. Volume 1-3. [Wallen, 1987] Lincoln A. Wallen. Matrix proof methods for modal logics. In Proceedings of the 10th IJCAI, 1987.