First-Order Modal Logic Theorem Proving and Functional Simulation

1 Introduction

Today's calculi for modal logics can be divid.ed into two main groups. The first group is concerned with the ex­ tension 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 appropri­ ately extended and [Wallen, 1987] in which the connec­ tion 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 expo­ nentially bigger than the original ones.

Based on Wallen's ideas, Hans Jiirgen Ohlbach and others ([Ohlbach, 1989; Ohlbach, 1991; Auffray and En­ jalbert , 1992; Farinas del Cerro and Herzig, 1988]) de­ veloped 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 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 respec­ tive advantages and to avoid their disadvantages if pos­ sible. To be more precise, it consists of both, a rela­ tional translation which does not result in an exponential growth in the number of clauses and a functional trans­ lation 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 seman­ tics. 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 ex­ emplified 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 famil­ iar 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 S'M we understand a tuple ((W, ~), S'loc, r, ¢)where W is a non-empty set of worlds and ~ is a binary accessibility relation between worlds, Tis one of these worlds (the actual world), <Pis a variable assignment and S'1oc 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 respec­ tive signature structures are all identical. Thus, if we refer to some domain 1J 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 inter­ pretation ~M = ((W, !R), ~Joe, T, ¢) is said to satisfy a formula() if~M FM (), where FM is recursively defined as follows:

where ~M[x] differs from ~M only with respect to the new current world X and j {P) denotes the function {pred­ icate) associated with f (P) by the signature structure ~Joe ( r) .

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 re­ spective accessibility relations. The most common ac­ cessibility relation properties are reflexivity, symmetry, transitivity, euclidity, seriality, directedness and linear­ ity. 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 t 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 ac­ tually a term representing a world).

The following definition describes the formula mor­ phism L () J w which accepts a modal logic formula () and a term w (which denotes a world) and results in a first­ order predicate logic formula. It can be viewed as a di­ rect translation from the satisfiability definition 2.1 into classical logic.

Definition 2.2 (The Formula Morphism L()Jw)

The remaining cases are treated by the usual homomor­ phic extension. The initial call for the translation of an arbitrary formula () then simply is L () J, .

This translation indeed behaves as desired . We for­ mulize 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 com­ plete, i.e. a modal logic formula () is satisfiable if and only if L()J, 1\ 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 R1 , R2 ... such that each of the R; denotes a (partially)Junctional 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 re­ sponsible 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 sub­ relations 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 (pro­ vided 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 apply­ function.

The following section provides with a formal defini­ tion 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 overS x T.

Then define for any pairs (x,y) and (u,v) inS x T : (x,y) ~ (u,v) iffx = u .

Obviously ~ denotes an equivalence relation. It is thus possible to introduce equivalence classes []~ by:

Both [(x, y)]/ ~'>$ and Rf ~'>$ are denumerable, therefore there exist surjective mappings 0 : Nat - Rf ~'>$ and 6, :Nat- O(i). Then define!;= {t5~:(j) IkE Nat}. We call FR = {/; I j EN at} a functional simulator of R on S x T. An element s E S is called normal w.r.t . R if there exists at E T such that (s, t) E R.

Now, given a denumerable binary relation Rover SxT and a functional simulator FR of R we know by construc­ tion that

• FR denotes a denumerable set of partial functions from S toT
• If u is normal w.r.t. R then for any f E FR f is defined on u and R(u, f(u)) holds.
• If R is left-total, then FR consists of total functions and for any ueS and any fEFR: R(u,f(u)) holds.
• For any u E S and any v E T : if R( u, v) then there exists an f E FR such that f( u) = v

3.2 Application to the Relational Translation

In the sequel we assume that the modal logic formu­ lae 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 trans­ formed into an equivalent one which is in negation nor­ mal form.

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

Definition 3.2 (The Formula Morphism l41J!) Let 41 be a modal logic formula in negation normal form.

In any other case l41J: behaves as l41Ju·

The notation u:f is used for readability instead of apply(/, u) . It is shorter and reflects the order of the 0-operators in the original formula. Thus, for instance, the formula 00 P gets translated into 3f: FR 3g: FR P'(t:g:f) where bracketing to the left is assumed.

According to the functional simulator properties de­ scribed above we define the two simulator axioms Sim1 and Sim2 as:

and

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 Sim1 and Sim2 are added to the clause set. But Sim1 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 theo­ rem shows this simulator axiom Sim1 is in fact superflu­ ous and thus merely the unit clause from Sim2 has to be added to the clause set.

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

where Axioms denotes the correspondence axioms for the modal logic M and FPL denotes the usual predicate logic satisfiablity relation.

Proof: From Theorem 2.3 we know that

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

simply because under the assumption that FR is a func­ tional simulator of R (i.e. the simulator axioms hold), the two formulae l41 J, and l41 J~ are logically equivalent. Re­ mains to be shown that Sim1 is in fact superfluous. Writ­ ten in clause form Sim1 gets: -.R( u, v) 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 Sim1 needs to be applied only from left to right. However, as a simple induction shows, no term of the form a1: . . . :an produced by the translation contains a universally quantified FR-variable and thus, no application of the Sim1 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 ex­ ponential 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 them­ selves 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 Sim2. Nevertheless, we can do even bet­ ter.

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 remark­ able, 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 con­ siderable 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 accessi­ bility relation properties, i.e. via Axioms and Sim2.

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

In the following application to some well known modal logics we will make use of this fact. For historical rea­ sons 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 symme­ try, 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 Sim2 . 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 Sim2 and the symmetry clause which is R(u::z:, u). Thus, a single unit clause for KD (namely R(u, u::z:)) and two unit clauses for KDB (namely R(u, u::z:) and R(u::z:, 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 Sim2 is infi­ nite. Nevertheless, its elements have a common struc­ ture which is R( u, u::z:1 ... ::z:n) where n ~ 0 for S4 and n ~ 1 for KD4. It is thus very easy to find an alter­ native clause set which generates exactly the same set, namely the two-literal clause ...,R(u,v) V R(u,v::z:) plus R( u, u) for S4 and R( u, u::z:) for KD4. The overall effect of this translation is therefore that at least the transitiv­ ity 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::z:1 ... ::z:n, u:y1 ... :ym) 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 £:y1 ... :ym for suitable instantiations of the y; we get R( u, v) for S5, R(u, v::z:) for KD45 and R(u::z:, v:y) for KD5. These unit clauses for S5 and KD45 even subsume Sim2 and hence their respective theories are determined by a sin­ gle unit clause. R(u:x,v:y) does not subsume R(u,u::z:), nevertheless it can be used for a simplification getting R(t, t::z:) (since all other cases are in fact subsumed by R( u::z:, 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 com­ mon predecessor in R also have a common successor in R. The clause set generated by this formula and Sim2 is infinite. However, the special structure of translated formulae allows to take the simple unit clause

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 appli­ cations of R(u:x, u:y:f(u, u:x, u:y)). In fact, this unit clause nicely reflects our intention what the directed­ property 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

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 !R. Hence, the simple unit clause from Sim2 (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 Sim2 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:

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 char­ acterized 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 Defini­ tions 2.1 and 2.2.

If we want to take varying domains into account a fur­ ther predicate has to be introduced, namely one which expresses existence of domain elements in given worlds. Thus the relational translation changes to

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 FE be a functional simulator for E, the formula morphism changes to:

where Lcl'J![xju:y] means that every x in lcl'J! gets re­ placed 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 FE.

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

Note that again the translation from above produces for­ mulae 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) A R( u, v) ~ E( v, x) and E( u, u:x ). This results m

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 do­ mains in the logic KD but also for KT, KD4 and S4. For the logics KD5 and KD45 we can get even simpler ax­ ioms 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 FR and y over FE) which states that every domain element (denoted by v:y) is known to any world apart from the initial world t . For t itself we still have the unit clause E(u ,u:x) which can thus be simplified to E(t,t: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 FE and x belongs to FR and for KD5 and KD45 we get the two simple unit clauses E(t, t:x) and E(u, v:x:y) with the FE element x and the FR element y.

In the non-serial case we are again not allowed to ig­ nore 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 FR-variable x is indeed defined on u. This evidently has to be done for any of the above sim­ plifications. 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 OF and Op where OF is responsible for the future and Op for the past respec­ tively. 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: RF(u, v) # Rp(v, u) for any two worlds (time instants) u and v. This leads to the following "time-theory":

Because of the equivalence between RF(u , v) and Rp( v, u) , it is not really necessary to consider both pred­ icates, i.e. we can for instance, replace any occurrence of Rp in the translated formula as well as in the theory axioms by RF provided the arguments are reversed. We thus get the theory axioms (where R is taken as a short­ form for RF):

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

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 R­ literals 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 formuliza­ tion of the Belief of Agents since it incorporates consis­ tency 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 struc­ ture, we would automatically have that also each agent considers his own and the other's agent's beliefs as con­ sistent with positive and negative introspection. If we do not want this, we have to assure that the KD45 proper­ ties 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 Xa in FRa

where u ranges over the worlds of the whole universe and Xa belongs to the functional simulator of Ra (agent a's belief relation). Thus the respective agent's theory of belief is then given by

i.e. the KD45 axiom holds only for those worlds which are accecssible for agent a. For all other worlds we still have Na(u) => Ra(u, u:xa) 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: Wa(u) => Na(u) (because of seriality).

Note that this technique also allows to express mu­ tual 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:xa) (for all agents a) will do for this purpose.

For more details on this issue the reader is again re­ ferred 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 stan­ dard 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 sim­ ple 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 the­ ories) 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 gen­ eral 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 lat­ ter 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 ef­ ficient 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 accessi­ bility relation properties. Part of our future work will be to examine more properties and property combinations which might be useful and/or interesting.