Abstract
There exist valuable methods for theorem proving in non classical logics based on translation from these logics into first-order classical logic (abbreviated henceforth FOL). The key notion in these approaches istranslation from aSource Logic (henceforth abbreviated SL) to aTarget Logic (henceforth abbreviated TL). These methods are concerned with the problem offinding a proof in TL by translating a formula in SL, but they do not address the very important problem ofpresenting proofs in SL via a backward translation. We propose a framework for presenting proofs in SL based on a partial backward translation of proofs obtained in a familiar TL: Order-Sorted Predicate Logic. The proposed backward translation transfers some formulasF TL belonging to the proof in TL into formulasF SL , such that the formulasF SL either (a) belong to a corresponding deduction in SL (in the best case) or, (b) are semantically related in some precise way, to formulas in the corresponding deduction in SL (in the worst case). The formulasF TL andF SL can obviously be considered aslemmas of their respective proofs. Therefore the transfer of lemmas of TL gives at least a skeleton of the corresponding proof in SL. Since the formulas of a proof “keep trace” of the strategy used to obtain the proof, clearly the framework can also help in solving another fundamental and difficult problem:the transfer of strategies from classical to non classical logics. We show how to apply the proposed framework, at least to S5, S4(p), K, T, K4. Two conjectures are stated and we propose sufficient (and in general satisfactory) conditions in order to obtain formulas in the proof in SL. Two particular cases of the conjectures are proved to be theorems. Three examples are treated in full detail. The main lines of future research are given.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Y. Auffray, P. Enjalbert andJ-J. Hebrard,Strategies for modal resolution: result and problems,Journal of Automated Reasoning 6 (1990), pp. 1–38.
M. Abadi andZ. Manna,Modal theorem proving, inProc. CADE 8, LNCS 230, Springer-Verlag 1986.
J. Barwise andS. Feferman (eds.),Model Theoretical Logics, Springer-Verlag 1985.
J. Barwise,Model theoretical logics: background and aims, inModel Theoretical Logics, J. Barwise and S. Feferman (eds.), Springer-Verlag 1985, pp. 3 – 23.
T. Boy de la Tour, R. Caferra andG. Chaminade,Some tools for an Inference Laboratory (ATINF),CADE-9, LNCS 310, Springer-Verlag 1988, pp. 744 – 745.
R. Caferra, M. Herment andN. Zabel,User-oriented theorem proving with the ATINF graphic proof editor,Proc. of FAIR'91, LNAI 535, Springer-Verlag 1991 pp. 2 – 10.
R. Caferra andS. Demri,Cooperation between dierct method and translation method in non-classical logics: some results in Propositional S5. Submitted.
A, R. Cavalli andL. Farinas del Cerro,A decision method for linear temporal logic, inCADE 7, LNCS 170, R. E. Shostak (ed.) Springer-Verlag 1984, pp. 113 – 127.
M. C. Chan,The recursive resolution method for mosal logics New Generation Computing 5 (1987), pp. 155–183.
F. B. Chellas,Modal Logic, Cambridge University Press 1980.
P. Enjalbert andL. Fariñas del Cerro,Modal resolution in clausal form Theoretical Computer Science 65 (1989), pp. 1–33.
L. Fariñas del Cerro,Un principe de résolution modale,R.A.I.R.O. Informatique théorique 18 no 2 (1984).
L. Fariñas del Cerro,Resolution modal logics, inLogics and Models of Concurrent Systems, K. R. Apt (ed.), Springer-Verlag 1985.
L. Fariñas del Cerro andA. Herzig,Automated quantified modal logic inMachine learning, Metareasoning and Logics, P. Bradzdil and K. Konolige (eds), Kluwer Academic Publishers, Dordrecht/Boston/London 1989.
R. Feys,Modal Logic, edited by J. Dopp,Collection Logique Mathématique Serie B., E. Wauwelaerts, Gauhier-Villars, Paris 1965.
M. C. Fitting,Proof Methods for Modal and Intuitionistic Logics D. Reidel Publ. Co., Dordrecht 1983.
M. C. Fitting,First-Order Logic and Automated Theorem Proving, Springer-Verlag 1990.
R. I. Goldblatt,First-Order definability in modal logic Journal of Symbolic Logic 40 (1975), Number 1, March, pp. 35–40.
A. Herzig,Raisonnement automatique en logique modale et algorithmes d'unification, Thèse, Université Paul-Sabatier de Toulouse, July 1989.
K. Konolige,A Deduction model of Belief, Pitman 1986.
J. Meseguer,General logics, inProc. of Logic Colloquium'87, H-D. Ebbinghaus et al. (eds.), North-Holland 1989.
H.-J. Ohlbach,Context Logic, FB Informatik Univ. Kaiserslautern, 1989.
E. Orłowska,Resolution systems and their applications I Fundamenta Informaticae 3 (1979), pp. 235–268.
E. Orłowska,Resolution systems and their applications II Fundamenta Informaticae 3 (1980), pp. 333–362.
J. H. Schmerl,Transfer theorems and their applications to logics, inModel Theoretical Logics, J. Barwise and S. Feferman (eds.), Springer-Verlag 1985, pp. 177 – 209.
R. M. Smullyan,First-Order Logic, Springer-Verlag 1968.
M. Schmidt-Schauss,Computational aspects of an order-sorted logic with term declarations, Thesis, FB Informatic Univ. Kaiserslautern, 1988.
P. B. Thislewaite, M. A. McRobbie andR. K. Meyer,Automated Theorem Proving in Non-Classical Logics, Pitman 1988.
J. van Benthem,Correspondence theory inHandbook of Philosophical Logic D. Gabbay and F. Guenthner (eds.) Vol. II. D. Reidel Publ. Co., Dordrecht 1984, pp. 167–247.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Caferra, R., Demri, S. & Herment, M. A framework for the transfer of proofs, lemmas and strategies from classical to non classical logics. Stud Logica 52, 197–232 (1993). https://doi.org/10.1007/BF01058389
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF01058389