Cooperation between Direct Method and Translation Method in Non Classical Logics: Some Results in Propositional S5

1 Introduction

The interest in non classical logics is now unanimously accepted in Artificial Intelligence and in Computer Sci­ ence. Concerning the way to mechanize them, there are two approaches:

• the direct approach: it consists of building (or us­ ing existing) specific proof systems for these logics (see for ex. [Fitting, 1983; Enjalbert and Farinas del Cerro, 1989])
• the translation approach: a problem expressed in a non classical logic (from now on called source logic) is translated into classical logic (from now on called target logic) . The problem is therefore solved in the target logic (see for ex. [Ohlbach, 1988]) .

Each approach has good defenders -see for ex. [Thisle­ waite et a/. , 1988; Ohlbach, 1988]. The direct approach naturally arose the first . Relating logics is a technique that has been used in pure logical studies: in correspondence theory and in definability theory. It has been also used in automated deduction for non classical log­ ics as an alternative to implement specific calculi for each non classical logic and it is the theoretical founda­ tions of the second approach. Historically the innovative work of E. Orlowska introduced the notion of resolution­ interr.retability of a logic into another -see [Orlowska, 1980 . More recently A. Herzig and H-J . Olhbach (see [Herzi~, 1989; Ohlbach, 1988] and a related work by M. Chan lChan, 1987]) emphasized the idea of logic mor­ phism, which is implicitly used in the previous work of E. Orlowska. Their works in which unification plays a central role were applied to several classes of modal and temporal logics.

The two approaches have drawbacks -and obviously advantages. The direct approach needs the construction of new theorem provers whereas the translation approach generates proofs from which the relation with the initial problem is difficult to grasp. In this paper we contend that the two approaches are not mutually exclusive but can be profitably combined. We propose to build from the proofs obtained after translation, partial (possibly total) proofs in the specific systems for non classical log­ ics, with the help of inverse translations. So, it becomes possible to add the advantage of the efficiency of theo­ rem provers for classical logics with that of presenting results (in the present case partial proofs) in the source logic. A computer system implementing this hybrid ap­ proach would allow the user to formalize his problem in his favorite logic and to get a reasonable solution in the same logic.

We do not consider in this work neither the problems inherent to the translation approach such as the nature of the classical logic into which the translation is done (first-order logic, fragment of second-order logic ... ), nor the theoretical limits of translation ( definability) or the choice of proof systems for non classical logics -tableaux,

resolution, matings and so on.

In order to show how cooperation between the trans­ lation approach and the direct one is possible we shall define a partial backward translation from classical first­ order logic (from now on abbreviated FOL) into propo­ sitional logic S5. Semantic relations hold between the backward formulas and we shall show that some S5clauses that logically entail some backward translated

formulas, can be derived in a variant of the resolution system RS5 [Enjalbert and Farinas del Cerro, 1989]. In that way we shall answer positively (for S5) to one of the conjectures stated in [Caferra et al., 1993]. Actually, we shall study how the proofs in FOL can be useful to build proofs in S5 with resolution methods.

There are different reasons to consider S5. S5 propo­ sitional formulas have a reasonable normal form -S5clauses in [Enjalbert and Farinas del Cerro, 1989]. It can be used as a model of autoepistemic reasoning [Moore, 1985]. Moreover the translation from S5 into FOL we shall use, is quite simple. Finally the problem of decid­ ing S5-satisfiability is only 1 NP-complete [Ladner, 1977].

The paper is structured as follows. The next section recalls the features for S5 we shall work on. In section 3 the inverse formula translation is defined and different semantic results are presented to state the main theo­ rem on partially ordered sets of 55-formulas. Section 4 states a result similar to the "consequence finding theo­ rem" [Lee, 1967] for the inverse formula translation in a variant of RS5. We also propose a plausible conjecture related to this theorem. In section 5, a simple example is fully treated. Finally we propose different ways to con­ tinue this work.

2 Preliminaries

We assume familiarity with the syntax and semantics of propositional S5. The standard definitions of satisfia­ bility and validity will be used -see [Hughes and Cress­ well, 1968]. The set of well-formed 55-formulas will be noted MFor. We now recall one normal form for the 55-formulas [Enjalbert and Farinas del Cerro, 1989]. In the sequel, by the term 'clause' (resp. 'literal') we shall mean a clause (resp. literal) in the classical logic.

Definition: A 55-formula is said to be in conjunctive normal form iff it is a conjunction of formulas of the form: C V DDt V ... V DDN V OCt V ... V OCR where C and the D; 's are clauses and the C; 's are conjunctions of clauses. Each conjunct is called a S5-clause. 6.

Fact 1 Every S5-formula is equivalent to a formula in conjunctive normal form.

2.1 Translation into First-Order Formulas

The proposed translation is standard (see for ex. [Chel­ las, 1980; Miura, 1983]) and it preserves validity. The translation is based on the naive one where the binary predicate R for the accessibility relation is deleted. If F denotes a 55-formula then T(F) denotes its translation. We use an auxiliary function Tr with the profile: Term x MFor-+ FOLFor -through all this paper 'term' will mean 'first-order term'. The constant 'aw' stands for "actual world" and T(F) = Tr(aw, F) .

1. Tr(t, P) = P(t) for P propositional variable
2. Tr(t, ft\g) = Tr(t, f)t\Tr(t, g)
3. Tr(t, -,f) = --.Tr(t, f)
4. Tr(t, Of) = Vx' Tr(x', f), x' is a new variable symbol
5. Tr(t, Of) = 3x" Tr(x", f), x" is a new variable symbol

Fact 2 A formula f is S5-valid iff T (!) is FOL-valid.

1 The satisfiability problem for usual logics such as 84 has a higher complexity

Notation: A first-order literal will be noted either Q(l) or sP(l), with s E {A, --.} (A the empty string), P a predicate symbol, l a list of terms and Q a predicate symbol preceded by one element of {A, --.}.

2.2 A Resolution Proof System

We recall the rules of the elegant resolution system RS5 defined in [Enjalbert and Farinas del Cerro, 1989]. D, D', C and C' denote clauses, E a conjunction of clauses and the symbol',' is a conjunctive operator.

DO-rule

RS5 is a V<!-riant of the system RT [Enjalbert and Far­ inas del Cerro, 1989] for the logic Ton which the special form of the 55-clauses has been taken into account. Ev­ ery modal formula without nesting of modal operators is 55-satisfiable iff it is T-satisfiable. RS5 is sound and complete for the refutation [Enjalbert and Farinas del Cerro, 1989].

3 Partial Inverse Formula Translation

The proposed partial inverse translation transforms FOL-formulas into 55-formulas. It applies to the set of first-order clauses that are deduced from the translation of 55-formulas. We shall note 'RFoL the operator giving the set of all the resolvents of two clauses and similarly :F FOL for the factorization rule. The symbol t-Re~FOL denotes the derivation operator for classical resolution.

3.1 Definitions

LetS= {Ct, ... ,CN} be a set of 55-clauses. We note TC; the FOL-formula T(C;) and TC: the skolemized (in the usual sense) form of TC; . Only Skolem con­ stants (noted a;) are introduced. TC: has the following form : Kt(aw) V ... V KN(aw) V Ll{x.) V ... V L~(l)(x.) V ... V Lk(xK) V ... V L'l<:(K)(xK) V ((Mf, 1 (a.) V ... V M m(l,l)( )) (Ml ( ) Mm(l ,u(l))( ))) 1,1 a1 t\ ··· t\ l,u(l) a1 V ··· V l,u(l) a1 V ... v ((Mt, 1 (aL)V ... V MZ:P' 1 )(aL)) t\ ... t\ (Ml ,u(L)(aL)v ... V M.Z:~ti)(L))(aL))) where the a;'s are constants and the x;'s are variables. So from the formula TC: we get n;=l u(k) clauses.

Definition: Let S be a set of 55-clauses equivalent to the S5-formula F. We note S' the set of clauses generated from S. Every clause c such that S' 1-RuFOL cis called a F-clause. !:::.

A clause c is a /-clause (generic term) if there is a S5-formula /' such that c is a /'-clause with the above definition. By definition we restrict the application of the backward translation only to the £-clauses. Every £- clause c has the form: K1(aw)V ... V KN(aw) V LHz1)V ... VL~( 1 )(zl)V ... V Li-(zK)V ... V Lr;jK)(zK)VMf{ai) V ... V M~( 1 )(al) V ... V Mf(aL)V .. . VM'f:(L)(aL). Informally if <P is the inverse translation, then t/J(c) = K1 V ... V KNV O(L~ V ... V L~( 1 ))V ... V D(L{' V ... V Lr;jK>) V O(Mf V ... V M~( 1 )) V ... VO(Ml V ... V MZ'(L)). We now define formally the partial inverse formula translation.

Backward translation for clauses

The principle of the backward translation is to gather the literals that have some modal context in common. In the particular case of S5, a modal context is simply a variable, or a constant. For other logics such as S4 a normal form for the clauses must be found -see [Caferra and Demri , 1992]. Indeed, the inverse partial formula translation is basically defined for clauses and then for the conjunction of clauses. We first define auxiliary func­ tions.

• generate-op( t) := if t is a variable then 0 else 0

· f3(C) := aw% C is a term%

We extend f3 to literals, clauses and sets of clauses.

Definition of </J: Let D be a £-clause L1 V ... V Ln . We define a partition with the literals of D, i.e., we define the set of classes { C;, 1 $ i $ k}. Moreover the classes satisfy the following properties. For 1 $ j $ k,

1. For all P,Q E C;, tQ = tP % L; = s;PL;(tL') %

2. For all P E Cj and Q fl. Cj, tQ ::/; tP

It can be easily checked that the decomposition in classes is unique. The definition of t/J(D) uses a function a mapping a class S to a S5-formula: ,

a({/1, .. . ,/p}) :=% S = {/I. ... ,lp}, I;= s;P;(c;)%

if c1 = aw then s1P1 V ... V spPp else generateop(cl).V{s;P; I s;P;(c;) E S}

<P(D) = a(C1) v ... V a(CA:) ·

Backward translation for conjunctions of clauses The partial inverse formula translation is extended to conjunctions of clauses. To do so, superclasses are de­ fined in so for as sets of classes. In order to compute <P( C 1 1\ ... 1\ C N) the partition { cf , .. . ,ci'} is associated to each clause C; and so is t(i,j) for each class c{. The point is now to compute superclasses considered as subsets of the set { c{, for 1 $ i $ N, 1 $ j $ us}. A superclass {c{f, ... ,c{~} satisfies the following properties :

1. for 1 $ a < b $ n, ia ::/; i6

2. for 1 $a$ b $ n, tia,ja = t 16 ·i 6 and til,jl ::/; aw By definition t/J'(SC)=generate-op(t< 11 .i 1 >)./\ {t/J(fJ(c{;)), 1 $ k $ n}.

t/J(C11\ ... I\CN) = V { t:({c;;, 1 $j $ N }), 1$ i1 $ u1, ... , 1$ iN$ UN} and t:({c1, ... ,cr}) :=%the c;'s are classes % if { ClJ ... , cr} does not contain any superclass then a( c1) 1\ ... 1\ a( c1) then let { sc1, ... , BCA:} be the su­ perclasses contained in { ClJ ... , c,} %they are disjoint% a(ci) 1\ ... 1\ a(cr)[sc1- t/J'(scl), ... , sq - <P'(sck)}.

For N = 1, we obtain the restricted definition for the clauses. Moreover if no superclass can be found in t/J(C1/\ ... 1\CN) then f:ss 4J(C11\ ... I\CN) <:? t/J(C1)/\ .. . At/J(CN) ·

Ezample: A= Q(z) V R(z) V M(a) V P(a); B = P'(aw) V M'(a) (the only variable is 'x') <P(A) = D(Q V R) V O(M V P) t/J(A 1\ B)= (D(QV R)AP')V(O(QV R)AOM')v(O(MV P) 1\ P') V O((M V P) 1\ M') In A, the class {Q(x), R(x)} has been considered as the superclass { {P(a), M(a)}, {M'(a)}} in A 1\ B .

The detailed proof of the next lemma as well as the other omitted proofs of this paper can be found in [Ca­ ferra and Demri, 1993].

Lemma 1 Let a and b be two /-clauses. It is decidable whether F=ss t/J(a 1\ b) ¢:} t/J(a) 1\ <P(b) and </J(a 1\ b) f=s 5 <P( a) 1\ <P( b) holds.

This lemma can be extended for n clauses. Further­ more, the equivalence holds iff the different clauses do not share any Skolem constants.

3.2 Partially Ordered Sets of 55-formulas

The next lemma states that if the resolution or the fac­ torization rules are used then there exist semantic re­ lations in S5 between the backward translation of the corresponding clauses.

Lemma 2 Let a, b and c be /-clauses. If b E :F FOL {a) then </J(a) F=ss <!J(b). If c E 'RFoL(a,b) then </J(a 1\ b) F=ss t/J(c).

The next proposition answers positively (for proposi­ tional S5) to conjecture 1 in [Caferra et a/., 1993]: the formula f entails the inverse translation off-clauses.

Proposition 1 Let f be a S5-formula equivalent to the set S of S5-clauses. Let S' be the set of clauses ob­ tained from the translation of S. For all /-clause c, if S' 1-Re·FOL c then/ F=ss t/J(c). .

Proof: The proof can be obtained by using the results about induced model in [Miura, 1983]. Let SB = (W, R, m) be a substructure of the S5-model (W, R, m, w) . In [Miura, 1983], it is shown that an induction translation W can be defined for S5 such that Vu E W (SB, u) f:ss f iff W(SB)(aw - u) ~FOL Tr(f, aw) . In the terminology used in [Miura, 1983], (W(SB), u) is an induced FOL­ model.

Let I= (W, R, m, w0 ) be a S5-model such that I f:s5 f (SB = (W, R, m)) . We therefore get that W(SB)(aw - wo) = fJol FFOL T(f) . We note fJol + Sko a model with the interpretation of Skolem constants (the Axiom of Choice is used here) such that lJol + Sko FFOL T(f) and lfol + Sko FFOL S'. Since the resolution is sound, if S' 1-RuFOL c then ljol + Sko FFOL c.

We know that the clause c has the format:

P1(aw)V ... V Pn(aw)VQHzt)V ... VQi 1 (zt)V ... VQ~(zl)V ... V Q~a(za) V RHat) V ... V Ri 1 (al) V ... V R1(at) V ... V R';fJ ( ap) where the z; 's are variables and the a; 's are (Skolem) constants.

We get Ijol FFOL (Pl(aw)V ... VPn(aw)) V (Vz1QHzl)V

... V Q1t(zl)) V ... V (Vza Q~(zl) V ... V Q~a(za)) V (3ytRl<Yt) V ... V Rit(Yt)) V ... V (3ypR~(yp) V ... V R{;" (yp )).

There exists a S5-clause c' such that 'T(c') is equal to the above formula modulo the renaming of variables. So by using the equivalence relation of the beginning of this proof, we get I F=ss c'. Q.E.D.

From the properties previously stated, we can build from a deduction in FOL, partially ordered sets of 55formulas semantically related to each other.

Theorem 1 Let U be a set of S5-clauses equivalent to f. We note S' the set of clauses obtained from U by using the translation 'T, the introduction of Skolem functions and the clausal transformation. Let {It, ... , lm) be a de­ duction from S' by resolution and factorization . Then there exists a partially ordered set -p. o.s.- (S, I) such that (conditions SC)

• S is a finite set of S5-formulas with/, 1/>{lm) E S and I is a partial order on S
• If(/ I g) then/ F=ss g
• f is minimal in {S, I) and 4>(1m) is maximal in {S, I)
• The non oriented graph {S, I) connects f and <P(lm)

Proof: By induction on the number of steps s used to deduce lm .

Base Case : lm E S' (s = 0)

Proposition 1 states that f F=ss 1/>{lm). The p.o.s. ( {f, 4>(1m)} , {(f, 1/>(lm))}) satisfies SC -this p.o.s. trivially satisfies the conditions.

Induction Step

Let {It, ... , lm) be a deduction such that lm has been de­ duced in s+ 1 steps.

Case 1 (lm E F(l; )): There exists, by the induction hypothesis, ( S;, /;) satisfying the semantic conditions with 1; . We consider the p.o.s. (S; U {1/>{lm)}, I; U {(4>(1;),1/>{lm))}. It can be easily shown that this struc­ ture satisfies SC for lm -see Lemma 2.

Case 2 (lm E 'R(l;, 1~:)) : There exists (by the induction hypothesis) a p.o.s. (S;, /;) (resp. (S~:, /~:)) satisfying SC for 1; -resp. 1~:. We consider the p.o.s. (S~ US~: U {1/>(l;)AI/>{1~:),1/>(1; t\1~:) , 1/>{lm)}, f; U/1: U {(1/>(l;JAI/>(1~:), 4>(1;)), (4>(1;) "4>(1~:), 4>(1~:)), (4>(1; "1~:),4>(1;) "4>(1~:)), (4>(1; t\ 1~:), 1/>{lm))}) . It can be easily shown that this p.o.s. satisfies SC for lm -see Lemma 1, 2. Q.E.D.

In the fourth condition the backward translation gen­ erates 55-formulas related semantically with the initial formula f. In Corollary 1 we shall present a stronger result .

The relationship between backward translated formu­ las should be compared with the definition of conse­ quence relation as a partial ordering on well-formed for­ mulas in [Scott, 1974].

The partial order may be total so that there exists a sequence (/o, ... , /u) such that for 0 ~ i ~ u - 1, /; f:ss /i+t where /o = f and /u = 1/>{lm)· The fol­ lowing corollary states a sufficient condition to get such a sequence.

Corollary 1 (Sequence of Semantic Entailments) If the hypothesis {if I; E 'RFoL (l;, 1~:) then F=ss 4>(1; t\ lk) <=> 1/>(l;)AI/>(1~:)) is added to Theorem 1 then there exists a sequence (/o, ... , /u) such that for 0 ~ i ~ u- 1, /; f:ss /i+t where /o = /and fu = 1/>{lm)·

The sequence built with the proof of Theorem 1 is not necessarily minimal . Its length may be reduced as well as the size of formulas . The condition f:ss 4>(1; t\ 1~:) <=> 4>( 1;) t\ 4>( 1~:) is decidable -Lemma 1.

4 Modal Consequence Finding and In­ terpolation

In Section 3, it has been shown that semantic relations hold between the initial 55-formula and the backward translation of clauses obtained with classical resolution. We shall show that in a variant of the resolution system RS5 -called RS5'- a partial "consequence finding the­ orem" similar to the one in [Lee, 1967] can be found. For a set of 55-clauses S, all the 55-clauses with a given format that are logical consequences of S admit an in­ terpolant S5-clause derivable from S in RS5'. U nfortu­ nately it cannot be extended to all the S5-clauses -see the counterexample in this section. A plausible result would be to connect syntactic and semantic properties about the backward translated formulas as it was mentioned in [Caferra et al. , 1993]. At that time, we ignored the re­ sult in [Lee, 1967] for the classical logic but we consider that a similar result in the systems for the non-classical logics would be a skilled criterion to compare different proof systems.

We shall ~all 0'-rule the following rule c~~~'> . We call RS5' the system (RS5\{0-rule})U{O'-rule}. In RS5', the 0-rule is a derived inference rule and the 0'­ rule is sound so RS5' is sound and complete.

The following theorem gives conditions to ensure the existence of an interpolant clause in the system RS5'. Theorem 3 can be seen as a partial modal equivalent of the so called "consequence finding theorem" . The consequence finding problem is stated in [Inoue, 1991]:

"Given a set of formulas T and a resolution procedure P, for any logical consequence D of T , can P derive a logical consequence C of T such that C subsumes D" ?

The rroblem for classical logic has been solved in [Lee, 1967:

Theorem 2 {Consequence Finding) Given a set S of clauses, if a clause C is a logical consequence of S, then for some n ~ 0, there exists a clause 'P E R:', such that T implies C.

The above theorem can be seen as an "extended com­ pleteness theorem for resolution" , i.e., not only refuta­ tional completeness. The following theorem provides conditions to ensure the existence of an interpolant clause in the system RS5'.

Theorem 3 (Interpolation) Let S be a set of S5-clauses. Let c be a S5-clause with the format dVO(ct)V ... VO(cn) where d and the c; 's are clauses. If S F=ss c then there exists a S5-clause c' such that S 1-RSS' c' and c' f:ss c.

The set S can contain any kind of 55-clauses.

2 Rn is the n 1 h resolution operator

Proof( sketch): The (constructive) proof is tedious. It is based on the format of c, on the refutational complete­ ness of RS5 and on the proofs of the completeness of the system RT [Enjalbert and Farinas del Cerro, 1989]. Two base cases are distinguished and the general case com­ bines them. Q.E.D.

Corollary 2 {Lemma Discovery) Let S be a set of S5clauses equivalent to f For all /-clause c such that t/J(c) has the format of Theorem 9, there exists css such that S 1-Rss' css and css F=ss 1/J{c).

We believe this result can be extended to every f-clause with RS5, but we were not able to completely prove the property stated in the following conjecture.

Conjecture 1 Let S be a set of S5-clauses equivalent to f and c be a /-clause. Then there exists a S5-clause c' such that S 1-Rss c' and c' F=ss 1/J(c).

If S is unsatisfiable then the information given by the Interpolation Theorem is too weak 3 . However, if S is minimally unsatisfiable, Corollary 2 and Conjecture 1 can be relevant for any proper subset of S.

Moreover RS5 is not strongly complete , i.e., if S F=ss c then S 1-Rss c. Obviously, ifS = {D{PVQ),O..., Q} then S F=ss OP and S lfRss OP -butS 1-Rss 0(-,Q 1\ P) . The natural deduction system in [Corcoran and Weaver, 1969] can be mentioned as an example of strongly com­ plete system, with S5-formulas instead of S5-clauses.

Furthermore Theorem 3 cannot be generalized to all the S5-clauses: the following counterexample proves this. IfS = {QVOP, DR} then S F=ss QVO(PI\R) but there is no S5-clause c,s such that S 1-RS5 c,s and c,s F=ss Q v O(P 1\ R) .

So, we cannot build an interpolant between any two formulas f and g by using the system RS5. The alter­ native syntactic interpolation lemma presented in [Cz­ ermak, 1973] cannot be adapted to RS5 -see also the related semantic interpolation lemma given in (Gabbay, 1972]. Conjecture 1 can be seen as an intermediate plau­ sible result between Theorem 3 and the modal equivalent of the Lee's Theorem. Furthermore we conjecture that Proposition 2 can be extended to RS5. We believe that in spite of the relative lack of interest of consequence find­ ing in research of automated theorem proving for classi­ cal logics, results about modal consequence finding could generate applications for Artificial Intelligence. That is why we propose the following result with the hope that a modal equivalent may exist for the system RS5 -or RS5'.

Proposition 2 Let S be a minimally unsatisfiable set of propositional clauses. Let c be a non tautological clause (# .i). There exists a clause d {# .i) such that S 1-Reo PC d and d FPC c iff Varprop{c) ~ Varprop{Sf.

In the case of unsatisfiability, this is stronger than Theorem 3. We conjecture this proposition has a modal equivalent.

5 Example

3 Empty cla.use a.s interpolant

4 Varprop give.s the .set of propo.sitional variable.s

We illustrate on a simple example the results of the pre­ vious sections. We consider the valid S5-formula f = {D(A ~ OB) 1\ D(C ~ OD)) ~((A v C)~ O(B v D)) . From a proof in FOL, we construct a partially ordered set of S5-formulas with ..., f as a minimal element and we present a deduction in RS5 that enables us to apply with f, Corollary 1 and Conjecture 1. The set of S5-clauses S = {A V C, 0-,B, D...,D, OB V o...,A, o...,c V OD} is equivalent to ..., f. The translation of S into FOL gener­ ates the set of clauses {A(aw)VC(aw), -,B(xl), -,D(x2), B(at) V ...,A{xa), ...,C(x4) V D(a2)} .

From the proof in Figure 1, Lemma 2 and Theorem 1 we get a p.o.s. of S5-clauses ; its construction is based on Theorem 1. Moreover in this case Corollary 1 is ap­ plicable so we get the following sequence of semantic en­ tailments. Each formula of the sequence logically entails the next one.

1. ..., f 2. {AVC)/\ {0-,B) /\0-,D/\ {OBVD...,A)/\(D...,CVOD) 3. (A V C) 1\ 0-,D 1\ (D...,C V OD) 1\ 0-,A 4. 0-,D 1\ {D...,C v OD) 1\ C 5. 0-,D/\OD 6 . .l

The properties of the previous sections allow us to built other p.o.s. of S5-formulas. Furthermore we present a refutation in RS5 -Figure 2. From Conjecture 1, every backward translation of a clause in FOL admits an in­ terpolant in RS5. The proof in Figure 2 contains all the required interpolants that are the backward translations themselves but it is not always the case.

6 Conclusion and FUture Work

With respect to the aims stated in Section 1, it has been shown that from a standard translation of S5-formulas into first-order logic it is possible to define a partial inverse formula translation having interesting semantic properties -Theorem 1, Corollary 1. The properties of the inverse translation have been used to prove a theo­ rem concerning consequence finding in S5 using a variant of the resolution system RS5 -Corollary 2. Corollary 2 can be used as a syntactic criterion to guide proofs in RS5'. We also answer positively to one conjecture and partially answer to a second one -see [Caferra et al., 1993J.

The inherent limitations of our work are threefold. The expreSsive power of propositional logic S5 is obvi­ ously limited. The extension of our results to first-order S5 is not straightforward because there is neither In­ terpolation Lemma for first-order S5 [Fine, 1979], nor reasonable normal form for all the quantificational 55formulas. We have shown that RS5 is incomplete for consequence-finding. Finally it should be mentioned that the computation of S5 normal forms remains ex­ penstve.

The main lines of future work are to prove Conjecture 1 of Section 4, to extend the present results to other modal logics (K, S4 ... ) with expectable increasing dif­ ficulties and to consider other proof systems -tableaux, matings.