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.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
A. Avron. Simple Consequence Relations. Information and Computation, 92:105–139, 1991.
T. Boy de la Tour, R. Caferra, and G. Chaminade. Some tools for an Inference Laboratory (ATINF). In CADE-9, pages 744–745. Springer-Verlag, LNCS 310, 1988.
R. Caferra and S. Demri. Semantic entailment in non classical logics based on proofs found in classical logic, 1992. Extended version to appear.
R. Caferra, S. Demri, and M. Herment. Logic morphisms as a framework for the backward transfer of lemmas and strategies in some modal and epistemic logics. In AAAI-9, pages 421–426. AAAI, MIT Press, July 1991.
R. Caferra, M. Herment, and N. Zabel. User-oriented theorem proving with the ATINF graphic proof editor. In FAIR' 91, pages 2–10. Springer-Verlag, LNAI 535, 1991.
H. D. Ebbinghaus. Extended logics: the general framework. In J. Barwise and Feferman S., editors, Model theoretic logics, pages 25–76. Springer-Verlag, 1985.
M. C. Fitting. Proof methods for modal and intuitionistic logics. D. Reidel Publishing Co., 1983.
A. Herzig. Raisonnement automatique en logique modale et algorithmes d'unification. PhD thesis, Université Paul Sabatier, Toulouse, July 1989.
K. Konolige. A deduction model of belief. Pitman, 1986.
C.R. Mann. Equivalence of deduction in proof theory and free cartesian closed categories. Journal of Symbolic Logic, 39:380–381, 1974.
J. Meseguer. General logic. In H-D Ebbinghaus, editor, Logic Colloquium '87, pages 275–330. North-Holland, 1987.
C. Morgan. Methods for automated theorem proving in non classical logics. IEEE Transactions on Computers, 25(8):852–862, August 1976.
H.J. Ohlbach. A resolution calculus for modal logics. PhD thesis, FB Informatik Univ. of Kaiserslautern, 1988.
H.J. Ohlbach. Context Logic. Technical report, FB Informatik Univ. of Kaiserlautern, 1989.
E. Orlowska. Resolution systems and their applications I. Fundamenta Informaticae, 3:253–268, 1979.
E. Orlowska. Resolution systems and their applications II. Fundamenta Informaticae, 3:333–362, 1980.
D. Scott. Completeness and axiomatizability in many-valued logic. In L. Henkin et al., editor, Tarski Symposium, pages 411–35, 1974.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Caferra, R., Demri, S. (1992). Semantic entailment in non classical logics based on proofs found in classical logic. In: Kapur, D. (eds) Automated Deduction—CADE-11. CADE 1992. Lecture Notes in Computer Science, vol 607. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55602-8_179
Download citation
DOI: https://doi.org/10.1007/3-540-55602-8_179
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55602-2
Online ISBN: 978-3-540-47252-0
eBook Packages: Springer Book Archive