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

摘要

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 first-order 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.