Semantic entailment in non classical logics based on proofs found in classical logic

Abstract

A particular way of relating logics, specially useful in the framework of automated theorem proving is proposed. From the definition of the semantics of a logic (called source logic and abbreviated henceforth SL) in another logic (called target logic and abbreviated henceforth TL or TLS), we translate formulas of SL into TL using known techniques. Then we show how to partially translate proofs found in TL into SL. More precisely, the main theoretical result of the paper is a theorem establishing that for a class of non-classical logics — taking first-order sorted logic with equality as target logic — given a formula f in SL, it is possible from a proof P of f (obtained in TL) to backward translate into SL some (sometimes all) formulas in P. This set of backward translated formulas are proved to be semantically related each other and to define a partial consequence relation in SL. We get therefore an entailment sequence for f in SL. Our approach is applicable to source logics either without “computationally interesting” proof systems or without proof systems at all. One running example is fully treated. We compare the results of our method with the ones of a specialized tableaux-based theorem prover for the logic S4(p). Some hints of future work are given.