Cooperation between Direct Method and Translation Method in

Preparing to load PDF file. please wait...

0 of 0
100%
Cooperation between Direct Method and Translation Method in

Transcript Of Cooperation between Direct Method and Translation Method in

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

Ricardo Caferra

Stephane Demri

L I F I A - I M A G , 46 Av. Felix Viallet, 38031 Grenoble Cedex, France

Abstract
The aim of this work is to combine advantageously the two existing approaches for theorem proving in non classical logics: proving in the considered non classical logic (called here the direct approach) and proving in classical logic by way of translation -called here the translation approach. Some results in propositional S5 show evidence of the relevance of this approach. We assume a translation from S5 into first-order logic and then we define a partial inverse formula translation from firstorder classical logic into S5. Semantic relations are proved to hold between the backward translated formulas. We answer positively (for S5) to one conjecture stated in a previous work by the authors. An Interpolation Theorem stating a property stronger than refutational completeness is also proved. A plausible conjecture stronger than the Interpolation Theorem is proposed. These results are interpreted in the framework of a slight variant of an existing resolution calculus for S5. We illustrate our method on a simple example. Future work includes applications of the approach to other modal logics.
1 Introduction
The interest in non classical logics is now unanimously accepted in Artificial Intelligence and in Computer Science. Concerning the way to mechanize them, there are two approaches: • the direct approach: it consists of building (or using existing) specific p r o o f 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. [Thislewaite et al., 1988; Ohlbach, 1988]. The direct approach naturally arose the first. Relating logics is a technique that has been used in pure logical studies: in correspon-

dence theory and in definability theory. It has been also used in automated deduction for non classical logics as an alternative to implement specific calculi for each non classical logic and it is the theoretical foundations of the second approach. Historically the innovative work of E. Orlowska introduced the notion of resolutioninterpret ability of a logic i n t o another -see [Orlowska, 1980J. M o r e recently A. Herzig and H - J . O l h b a c h (see [ H e m e , 1989; Ohlbach, 1988] and a related work by M. Chan [Chan, 1987]) emphasized the idea of logic morphism, 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 m o d a l 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 logics, with the help of inverse translations. So, it becomes possible to add the advantage of the efficiency of theorem provers for classical logics with that of presenting results (in the present case p a r t i a l proofs) in the source logic. A computer system implementing this hybrid approach 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 translation approach and the direct one is possible we shall define a partial backward translation from classical firstorder logic (from now on abbreviated FOL) into propositional 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

74 Automated Reasoning

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 propositional 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 deciding S5-satisfiability is only1 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 theorem on partially ordered sets of S5-formulas. Section 4 states a result similar to the "consequence finding theorem" [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 continue this work.

2 Preliminaries

We assume familiarity with the syntax and semantics of propositional S5. The standard definitions of satisfiability and validity will be used -see [Hughes and Cresswell, 1968]. The set of well-formed S5-formulas will be noted MFor. We now recall one normal form for the S5-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.

D e f i n i t i o n : A S5-formula is said to be in conjunctive

normal form iff it is a conjunction of formulas of the

form:

where

C and the Di's are clauses and the Cj's are conjunctions

of clauses. Each conjunct is called a S5-clausc.

Fact 1 Every S5-formula is equivalent to a formula in conjunctive normal form.
2.1 Translation into First-Order Formulas

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

Caferra and Demri 75

76 Automated Reasoning

Caferra and Demri 77

P r o o f (sketch): The (constructive) proof is tedious. It is based on the format of c, on the refutational completeness 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 combines them. Q.E.D.

Figure 1: Refutation with classical resolution

So, we cannot build an interpolant between any two formulas f and g by using the system RS5. The alternative syntactic interpolation lemma presented in [Czermak, 1973] cannot be adapted to RS5 -see also the related semantic interpolation lemma given in [Gabbay, 1972]. Conject ure 1 can be seen as an intermediate plausible 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 finding in research of automated theorem proving for classical 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'.

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 applicable so we get the following sequence of semantic entailments. Each formula of the sequence logically entails the next one.
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 interpolant 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
W i t h 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 theorem concerning consequence finding in S5 using a vari-

78 Automated Reasoning

Figure 2: Refutation with the proof system RS5

ant 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 p a r t i a l l y answer to a second one -see [Caferra et a i , 1993].
The inherent limitations of our work are threefold. The expressive power of propositional logic S5 is obviously limited. The extension of our results to first-order S5 is not straightforward because there is neither Interpolation Lemma for first-order S5 [Fine, 1979], nor reasonable normal form for all the quantificational S5formulas. We have shown that RS5 is incomplete for consequence-finding. Finally it should be mentioned that the computation of S5 normal forms remains expensive.
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 difficulties and to consider other proof systems -tableaux, matings.

References

[Caferra and D e m r i , 1992] R. Cafer ra and S. D e m r i . Semantic entailment in non classical logics based on proofs found in classical logic. In C A D E - 1 1 , pages 385-399. Springer-Verlag, L N A I 607, June 1992.
[Caferra and D e m r i , 1993] R. Caferra and S Demri. Cooperation of direct and translation methods in propositional S5 (long version), 1993. Forthcoming.

[Caferra tt a i , 1993] R. Caferra, S. Demri, and M. Herment. A framework for the transfer of proofs and strategies from classical to non classical logics. Studia Logica, 52(2), 1993.

[Chan, 1987] M. C. Chan. method for modal logics. ing, 5:155-183, 1987.

The recursive resolution New Generation Comput-

[Chellas, 1980] F. B. Chellas. Modal Logic. Cambridge University Press, 1980.

[Corcoran and Weaver, 1969] J.

Corco-

ran and G. Weaver. Logical consequence in modal

logic: natural deduction in S5. Notre Dame Journal

of Formal Logic, X(4):370-384, October 1969.

[Czermak, 1973] J. Czermak. Interpolation theorem for some modal logics. In Rose and Sheperdson, editors, Logic Colloquium 75, pages 382-393. North-Holland Publishing Company, 1973.

[Enjalbert and Farinas del Cerro, 1989] P. Enjalbert and L Farinas del Cerro. M o d a l resolution in clausal form. Theoretical Computer Science, 65:1-33, 1989.

[Fine, 1979] K. Fine. Failures of the interpolation lemma in quantified modal logic. Journal of Symbolic Logic, 44(2):201-206, June 1979.

[Fitting, 1983] M. C. F i t t i n g . Proof methods f o r modal and tntuitionistic logics. D. Reidel Publishing Co., 1983.

[Gabbay, 1972] D. M. Gabbay. Craig's interpolation theorem for modal logics. In Conference in Mathem a t i c a l Logic, London "70, pages 111-127. SpringerVerlag, L N M 255, 1972.

[Herzig, 1989] A. H e r z i g . R a i s o n n e m e n t automatique en logique modale et algorithmes d 'unification. P h D thesis, Universite P. Sabatier, Toulouse, 1989.

[Hughes and Cress well, 1968] G. E. Hughes and M. J. Cresswell. An introduction to modal logic. Methuen and Co., 1968.

[inoue, 1991] K. Inoue. Consequence-finding based on ordered linear resolution. In I J C A I - 1 2 , Sidney, pages 158-164, August 1991.

[Ladner, 1977] R. E. Ladner. The computational complexity of provability in systems of modal propositional logic. S I A M J. Comp., 6(3):467-480, September 1977.

[Lee, 1967] R. C. Lee. A completeness theorem and a computer program for finding theorems derivable for given axioms. PhD thesis, University of California, Berkeley, 1967.

[Miura, 1983] S. M i u r a . Embedding of modal predicate logics into lower predicate calculus I. Rassegna Internazionale Di Logica, 28:94-105, 1983.

[Moore, 1985] R. C. Moore. Semantical considerations on nonmonotonic logic. Artificial Intelligence, 25:7594, 1985.

[Ohlbach, 1988] J.H. Ohlbach. A resolution calculus for modal logics. In C A D E - 9 , pages 500-516. SpringerVerlag, LNCS 310, 1988.

[Orlowska, 1980] E. Orlowska. Resolution systems and their applications I I . Fundamenta Informaticae, 3:333-362, 1980.

[Scott, 1974] D.Scott. Completeness and axiomatizability in many-valued logic. In L. Henkin et al., editor, Tarskt Symposium, pages 411-435, 1974.

[Thislewaite et a i , 1988] P. B. Thislewaite, M. A. McRobbie, and R. K. Meyer. Automated theoremproving in non-classical logics. P i t m a n , 1988.

Caferra and Demri 79
LogicLogicsTranslationApproachProofs