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

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.