Ricardo Caferra, Stephane Demri, Michel Herment
There exist methods in automated theorem proving for non-classical logics based on translation of logics from a (non-classical) source logic (abbreviated henceforth SL) into a (classical) target logic (abbreviated henceforth TL). These valuable methods do not address the important practical problem of presenting proofs in SL. We propose a framework applicable at least to S4(p), K, T, K4 for presenting proofs of theorems of these logics found in a familiar TL: Order-Sorted Predicate Logic (abbreviated henceforth OSPL). The method backward translates lemmas in a deduction (in TL) either (a) into lemmas in a corresponding deduction in SL (in the best case), or (b) into formulas semantically related to lemmas in a corresponding deduction (in the worst case). As a natural consequence we bring to the fore the fact that this framework can also be used to help in solving another important and very difficult problem: the transfer of strategies from one logic to another. One conjecture -with corresponding theorem which is a particular case of it- is stated. When (b) above holds we give sufficient (and in general satisfactory) conditions in order to obtain the lemmas in SL. Two examples are treated in full detail : the well known problem of the "wise man puzzle" and another one which shows how our method can be used to transfer strategies. No additional theoretical result is given in this direction, but it is clear from the example how the proposed framework can help to transfer strategies.