Modal Theorem Proving: An Equational Viewpoint

Yves AUFFRAY Societe des avions M. Dassault 78 quai Marcel Dassault 92210 Saint-Cloud -France

ABSTRACT

We propose a new method for automated theorem pro­ ving in first order modal logic. Essentially, the method consists in a translation of modal logic in­ to a specially designed typed first order logic cal led Path Logic, such that classical modal systems (first order Q, T, 04, S4, SS) can be characteri­ zed by sets of equations. The question of modal theorem proving then amounts to classical theorem proving in some equational theories. Different me­ thods can be. investigated and in this paper we con­ sider Resolution. We may use Resolution with Para­ modulation, or a combination of Resolution and Rewriting techniques. In both cases, known results provide "free of charge" a framework immediately applicable to Path Logic, with completeness theo­ rems. Considering efficiency, the R~writing method seems better and we present here in details its application to Path Logic. In particular we show how it is possible to define a special kind of skolemisation and design a unification algorithm which insures that two clauses will always have a finite set of resolvents.

INTRODUCTION

In the so-called possible worlds semantics for Mo­ dal Logic, modal operators are interpreted as quan tifications over "worlds", constrained by some "accessibility" relation. But in the language of modal logic, worlds are not explicitely named, i.e. there is no syntactic item, such as variables or constants, denoting them. We consider that much of the success of Modal Logic comes from this feature, since the variableless operatorsoand o can be clo­ sely related with current language operators like "necessary", "always", or "I believe that". But from a theorem proving point of view, is this choi­ ce appropriate ? This is not that obvious : just observe the difficulties encountered by different authors who tried to extend Robinson's Resolution method to first order modal theorem proving [Cial­ dea 86] [Abadi Manna 86] [Konolidge 86]. Indeed it is certainly not easy to cope with the dependencies between objects of the discourse domain and worlds, which are in fact specified by a first order modal formula, in a fQrmalism which avoids naming the latter.

*This work has been partially supported by the GRECO-PRC "Programmation"

Patrice ENJALBERT * Laboratoire d'Informatique Oniversite de Caen 14032 Caen Cedex - France

A well-known way of restoring, say, a syntactic status to the worlds and the accessibility relation is to translate modal formulas into a first order classical logic with a binary relation symbol to denote the accessibility relation. This direction has been proposed by several authors in the A.I. field (f.i. [Moore 80]). But it seems that we loose much of the structure of the initially given modal formulas in the process of translation, and this is to be paid in terms of efficiency.

In this paper we propose another method for mo­ dal theorem proving. This method is based on a translation into a first order classical logic, but the target logic is tailored to better fit the structure of modal formulas.

We call this logic Path Logic. It possesses three types A, W and D. Objects of type D are those of the discourse domain. Objects of type-W represent worlds. Concerning A, we can see it as the type of operators on objects of type W. The idea is to cap­ ture the notion of accessibility relation in the following way : "the world w' is accessible from w" will be expressed by the sentence "w' is obtained from w by application of an operator in A". Through our translation in Path Logic, the various systems of modal logic are mapped into equational theories expressing some constraints on the system of opera­ tors. Proposition 1 provides the correspondance for Q, T, Q4, S4 and SS.

The question of modal theorem proving then amounts to classical theorem proving in some equa­ tional theories. Different methods can be investi­ gated and in this paper, we consider Resolution.We may use Resolution with Paramodulation like in [Walther 87], or a combination of Resolution and Rewriting techniques like in [Plotkin 72] and [Fa­ ges 83]. Both these theories provide "free of char­ ge" a framework immediately applicable to Path Logic with completeness theorems (proposition 3). Conside­ ring efficiency, Plotkin-Fages method seems better and we present here in details its application to Path Logic.

In particular, we must face the following problem. The equational theories considered for some modal system (Q4,S4)possess an associative operator, and associative unification in general is known as a difficult question [Fages, Huet 86] [Pecuchet 84]. The difficulty is overcome here by defining a spe­ cial skolemisation ("strong skolemisation"in the pa­ per). A unification algorithm ·based on these results has been defined and proved correct (proposition 5).

Similar approaches are proposed by L. Farinas and A. Herzig [Farinas Herzig 88], and H.J. Ohlbach [Ohlbach 88] from who we have borrowed the state­ ment of the Unique Prefix Property. Compared to these papers, ours is characterized by the syste­ matic developpement of an algebraic-equational point of view. This to our sense gives a cleaner mathematical framework and has the invaluable ad­ vantage of discharging of a great deal of mathe­ matical work.

PATH LOGIC AND THE TRANSLATION OF FIRST ORDER MODAL LOGIC

1.1 Syntax

We consider the language of modal logic built on a signature L consisting of : - a set G of function symbols of any arity - a set P of predicate symbols of any arity with the classical and modal connectives A,v,i, V, 3, <> ,c, and a set V (x, y, z ··· ) · Terms and modal formulas are defined in the usual way.

Given some modal system S among Q, T, Q4, S4, SS L(S) will denote the Path Logic associated with s. As earlier mentionned, L(S) possesses three types A , W, D. Its language is the classical typed first order language built on one of the following signatures LS' according to the modal system S in view. For any term t and type T, we note "t:T" for "t of tvoe T". -

L Q : £ : W, constant ! ! W x A ~ W, function symbol - for which we use Infix notation The set G of L - a function symbol g in G has type Dn --" D in L if g had arity n in L The set P of L-a 8redicate symbol p in P has t ype W x ~n ~{0,1} in LQ if p had arity n in L LT : LQ U { 1 : ~} LQ 4 : LQ U { * : ~ x ~ ---7 ~} - again, we use infix notation LS4 LQ4 U LT LS5 : LS4 U { () -1 : ~ ~ ~}

Let 11 ( {a , S,y, ·.· ,}}a set of variables of type A. V is the set of variables of type D. We have the usual notions of well typed terms and-formulas. Re­ mark that there is no variables of type W, so that the only terms possessing this type are £ and £!a 1 ! .·· !ak' with a. : ~· The reader can fruitfully interpret such objetts as paths in a Kripke struc­ ture, where "transitions" from one world to another would be named by some a .· J

1.2. Semantics

The semantics of modal logic considered in this paper is a semantics with constant domains and ri­ gid function symbols. The restriction to rigid function symbols is inessential and only for sake of simplicity : all results in this paper easily extend to flexible symbols. We shall say that a modal formula is S-satisfiable if it admits a mo­ del which fulfils the requirements on interpreta­ tions for the modal system S.

An interpretation K for L(S) is a classical in­ terpretation, defined-by giving a domain for each type ~· ~ and ~· and, for any symbol in LS a function or predicate with the correct type. Moreover we suppose that K satisfies the following equatio­ nal theory E(S), according to the modal systemS in view

We say that K is an E(S)-interpretation. The no­ tions of truth, validity, satisfiability are defi­ ned in the usual way. We shall say that a formula is L(S)-satisfiable if it admits an E(S)-interpre­ tation.

The idea is the following. Let K be some inter­ pretation and A and W be the domains -for type A and W respectively. W can be considered as a set of worlds and A as a set of operators on W. The sen­ tence "the world w' is accessible from w" is inter­ preted in Path Logic as "there is an operation a in A such that w' = w! a is true inK". The set of equations E(S) is what corresponds in the Path Lo­ gic L(S) to the properties of the accessibility re­ lation for s. For instance reflexivity is expressed by the existence of a neutral element 1 ; transiti­ vity by the existence of an associative operation * on A, such that (A,*) is a semi-group operating on W, or a monoid or ·a group according to whether we are in L(Q4), L(S4) or L(SS).

If the above equations are oriented from left to right, each set E(S) becomes a rewriting system which can be completed into a canonical one, let's call it R(S) (for the notion of canonical rewriting system, see f.i. [Huet, Oppen 80]). If follows that any term t admits a normal form for R(S).

Given any modal system S (among those under con­ sideration) the Path Logic L(S) consists of the above defined first order language on the signature L 5 , together with the equational theory E(S)

1:3. Translation from m~dal logic to. path logic

For any term TI : W and modal formula B, the for­

mula t(n,B) is defined by induction on the structu re of B : t(TI, p(t 1 , ·.· ,tn)) = p (TI, t 1 , ..· ,tn) if p is a predicate symbol t('n, -.B) = -.t(1t, B) t(1t, B 1 D. Bz) = t(1t, B1) D. t(1t, Bz) t(1t, Vx B) = Vx t(1t, B) t(1t, 3x B) = 3x t(1t, B) t(1t, 0 B)= Va t(1t! a, B) ( b.e {", v} )

t(1t, 0 B) = 3a t(1t! a, B)

t(n,B) can be read as "the translation of B with starting point the world denoted by TI~ 1 The transl a tion of B is T(B) = t(£,B)

Proposition I : A modal formula B is S-satisfiable iff T(B) is L(S) satisfiable. Example I : Let G = c 3 x C() p (x) T (G) = 3 a 3 x V S 3 y p (£ ! a ! S! y 1 x)

2 - RESOLUTION -FOR PATH LOGIC

A Path Logic L(S) is a typed first order equatio­ nal theory. We can apply Resolution with Paramodu­ lation : for instance, the techniques presented in [Walther 87] immediately apply, Or we can use a combination of Resolution and Rewriting techni­ ques; and this is what we present now.

2.1 FeEolution in equational theories

We first recall that the equational theories E(S) above are defined by canonical rewriting systems. [Plotking 72],[Fages 83] extend Robinson Resolution Principle to this framework in the following way. Let E be some equational theory and {t 1 , ··· ,tk}a

defined by a canonical rewriting system ~ then = E is decidable and t = Et' iff the normal form oft according toRE is identical to that oft'.

E-resolvant :

Let us call E-resolution the deductive system consisting of one inference rule which, given two clauses c 1 and c 2 allows to infer any E-resolvant of c 1 and c 2 · As usual a refutation is a proof of the empty clause.

Theorem 2 (Plotkin, Fages) :

A clausal formula is E-unsatisfiable iff there exists a refutation of this formula by E-resolu­ tion.

Let us apply this result to Path Logic. We can introduce in the signature LS skolem functions of

the convenient arities and types and associate, in the standard way, with every formula H of L(S) a clausal formula H' equivalent to H with respect to L(S)-satisfiability. Combining this process with the traduction T thanks to proposition I, we can associate with every modal formula B of S a formu­ la B' of L(S) in clausal form such that B' is L(S)­ unsatisfiable iff B is S-unsatisfiable. Then we have :

Proposition 3

Let B any modal formula, S any system among Q, T, Q4, 54, SS, and B' the skolemized of T(B). B is S-unsatisfiable iff we can refute B' by E(S)-reso­ lution.

Example 2 : 55-validity of ()p -+ cOpa

We prove the SS-:unsatisfiability ofF =()p AQC,p Translation : T(F) = 3oc p(c ! oc) 1\ 3(3 'Vy. -,p(c ! (3 ! y.)

Thus, the empty clause is a resolvant of c 1 and c 2

2.2 Sttong skolemisation

We recall some definitions. Given some set T of terms, a COmplete Set of Unifiers (CSU) for T is a set S of unifiers of T such that for any unifier a of T, there is some 'l'" in S such that'(' is more ge­ neral than a : there is some 11 such that O='t ~ -

, In order to automatise the search for refuta­ tions of sets of clauses, it is quite desirable (but not strictly necessary) to be sure that any unifiable family {t 1 , ··· ,tk} of terms admits a fi-

nite CSU. In the empty theory, f.i. E(Q), we know that such sets exist and are in fact reduced to singletons (most general unifiers), and we know algorithms to produce them. It is easy to check that there also exist finite CSU's in the case of E(T), and to exhibit a unification procedure. But in E(Q4), E(S4) or E(SS) we have an associativity axiom for *, and complete sets of unifiers are in general infinite.

Counter example 3 Let E = E(Q4) = {w ! (a *a') = w !a !a', (Cl *a') * a" "' a * (a oto")}. The E-unifiers of {E ! a ! a, E ! a ! a} are e 1 : oc --> a

there is no finite complete set of E-unifiers.

It is possible to enumerate the members of a complete 10~ of unifiers, f. i. using the "narrowing" procedure [fages 83] [Fay 79]. But there is a bet­ ter way on. We can take advantage of the particular structure of the formulas obtained in L(S) by trans lation from S, and perform a skolemisation finer than the standard one, which will ensure the desi­ rable finiteness property. This is what we call strong skolemisation. At the present time it is de­ fined for the modal systems Q, T, Q4, 54, so that they are the only systems under consideration in this section.

Since the process of strong skolemisation is a bit complex, we rather present here the result T"(B) of applying it to the translation T(B) of a modal formula B.

Let B a modal formula in negative normal form (ne­ gation operating on a atomic formulas).

T'(B) = t 1 (£, ¢,B) where, if rr is of type Wand X is a set of D-typed variables, t'(rr,X,B) is-recursi vely defined-by :

Example 4 :

Let G"' c c 3 xOp(x). We have:

T(G) = V aV8 3 x·3y p(£! a ! 8 !y,x) ,and the strongly skolemized form is :

VaV8 p(£ !a !8 !(/) (g(£ !a !8)), g(£ !a !8))

As one can see on this example, the general idea is to replace skolem terms depending ort A-variables (such as f(a,8)), by skolem terms depending on path expressions (like in g(£!a!8)).

Proposition 4

Let B be some modal formula and T'(B) the strong skolemisation of T(B). B is satisfiable inS iff T'(B) is satisfiable in L(S).

Skolemised formulas can then be put into clausal form. The clausal formulas obtained that way, pos­ sess a property which guarantees that terms to be unified admit a finite complete set of unifiers, namely :

Let C be a clause and a : A a variable. For eve­ ry sub-term rr!a: ~ in C, rr does not depend on the particular occurence of a, but uniquely on a. We call this property the Unique Prefix Prope_r ty · (U. P. ~). In particular it follows that if rr!a!a 1 ! ··· !ak:

W is a sub-term of C, a does not occur in rr and a. ~a for all j = I ... k J

For example one can easily check that the formu­ la T'(G) in example 3 satisfies this condition, while the set in the counter-example 3 does not.

Proposition 5 Any set of expressions that satis­ fies the U.P.P. admits a complete set of E(S)-uni­ fiers. There is a procedure that computes such a set of E(S)-unifiers. The substitutions which are computed preserve the U.P.P. on the given expres­ sions.

It follows from proposition 5 and Plotkin-Fages' results that the classical semi-decision procedure for checking unsatisfiability of a set of clauses can be adapted to Path Logics in a straightforward way. By means of the translation T', we obtain a semi-decision procedure for the modal systems un­ der consideration. The algorithm is given in [Auf­ fray, Enjalbert 88] and proved correct in [Auffray 89].

3. EXTENSIONS -DISCUSSION

Extensions

Our method can be extended to deal with logics with several different modalities (or multimodal logics) such as epistemic logic with many agents. If no relation is specified between the modal operators, we just need to consider subtypes of type A corres ponding to the different modal operators, and the characteristic set of equations for each one. We can also deal with relations between modalities specified by axiom schemas like c 1 A~ c 2 A, by

setting some order on the subtypes. Again Walther's techniques immediately apply, and we are studying the extension of Plotkin-Fages ones.

Discussion

I - The Unique Prefix Property constitutes a cha­ racterisation of a subset of the set of formulas of Path Logic in which Modal Logic can be embed­ ded. This feature distinguishes our translation from the "trivial" one ·envolving a binary relation symbol to denote the accessibility relation. We consider that it indicates that translation from modal logic to path logic is a good compromise keeping part ot the structure of modal formulas while adding what is necessary of extra mathema­ tical structure.

Also in the "trivial" translation, properties of the accessibility relation would be expressed by clauses at the same level than the other ones characterizing the problem to be solved. This si­ tuation would be very similar to the treatment of equality which consists in adding a predicate symbol "=" with clauses to express its properties this is known to be the wrong way to do · Further on, the use of Rewriting techniques seems likely to give better efficiency than Paramodulation : see [Plotkin 72] for this discussion.

2 - In this paper we considered Resolution, but other classical theorem proving techniques could be used for Path Logic. Fo instance techniques based on rewriting [Hsiang, Dershowitz 83] could be of interest.

3 - A nice feature of our theory is that the treat­ ment of modalities is finally reduced to unifica­ in an equational theory, Unfortunately it:· is likely that not all modal systems can be delt with that way : consider a system like G where the property of the accessibility relation is of topological nature, or some Temporal Logics with the same characteristic. But nothing prohibits to mix the techniques of this paper with other ones, induc­ tion for example. This remains to be investigated. Also the question of s 5 must be considered.

On the other hand we can ask which semantical properties can be nicely expressed in the language of Path Logic.