Skip to main content
SpringerLink
Log in

Natural Deduction for Non-Classical Logics

  • Published:
Studia Logica Aims and scope Submit manuscript

Abstract

We present a framework for machine implementation of families of non-classical logics with Kripke-style semantics. We decompose a logic into two interacting parts, each a natural deduction system: a base logic of labelled formulae, and a theory of labels characterizing the properties of the Kripke models. By appropriate combinations we capture both partial and complete fragments of large families of non-classical logics such as modal, relevance, and intuitionistic logics. Our approach is modular and supports uniform proofs of soundness, completeness and proof normalization. We have implemented our work in the Isabelle Logical Framework.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Anderson, A. R., N. D. Belnap, Jr., and J. M. Dunn, Entailment, The Logic of Relevance and Necessity, volume 2, Princeton University Press, Princeton, New Jersey, 1992.

    Google Scholar 

  2. Avron, A., 'Simple consequence relations', Information and Computation 92, 105-139, 1991.

    Google Scholar 

  3. Avron, A., F. Honsell, M. Miculan, and C. Paravano, 'Encoding modal logics in logical frameworks', this issue, 161-208.

  4. Basin, D., S. Matthews, and L. ViganÒ, 'Implementing modal and relevance logics in a logical framework', in L. Carlucci Aiello, J. Doyle, and S. Shapiro, editors, Proceedings of KR'96, 386-397. Morgan Kaufmann Publishers, Inc., San Francisco, California, 1996.

    Google Scholar 

  5. Basin, D., S. Matthews, and L. ViganÒ, 'Labelled propositional modal logics: theory and practice', Journal of Logic and Computation 7(6), 1997.

  6. Belnap, Jr. N. D., 'Display logic', Journal of Philosophical Logic 11, 357-417, 1982.

    Google Scholar 

  7. Bull, R., and K. Segerberg, Basic modal logic, 1-88, volume 2 of Gabbay and Guenthner [19], 1984.

    Google Scholar 

  8. D'Agostino, M., and D. M. Gabbay, 'A generalization of analytic deduction via labelled deductive systems. Part I: basic substructural logics', Journal of Automated Reasoning 13, 243-281, 1994.

    Google Scholar 

  9. DoŠen, K., 'Sequent-systems for modal logic', Journal of Symbolic Logic 50(1), 149-168, 1985.

    Google Scholar 

  10. DoŠen, K., 'Negation as a modal operator', Reports on Mathematical Logic 20, 15-27, 1986.

    Google Scholar 

  11. Dummett, M., 'The philosophical basis of intuitionistic logic', in Truth and other enigmas, 215-247, Harvard University Press, Cambridge, Massachusetts, 1978.

    Google Scholar 

  12. Dunn, J. M., Relevance logic and entailment, 117-224, volume 3 of Gabbay and Guenthner [19], 1986.

    Google Scholar 

  13. Dunn, J. M., 'Star and perp: Two treatments of negation', in J. Tomberlin, editor, Philosophical Perspectives, volume 7, 331-357, Ridgeview, Atascadero, California, 1994.

    Google Scholar 

  14. Dunn, J. M., 'Gaggle theory applied to modal, intuitionistic, and relevance logics', in I. Max and W. Stelzner, editors, Logik und Mathematik (Frege Kolloquium '93), 335-368, de Gruyter, Berlin, 1995.

    Google Scholar 

  15. Dunn, J. M., 'Positive modal logic', Studia Logica 55, 301-317, 1995.

  16. FariÑas Del Cerro, L., and A. Herzig, 'Combining classical and intuitionistic logic', in F. Baader and K. U. Schulz, editors, Frontiers of Combining Systems, 93-102, Kluwer Academic Publishers, Dordrecht, 1996.

    Google Scholar 

  17. Fitting, M., Proof Methods for Modal and Intuitionistic Logics, Kluwer Academic Publishers, Dordrecht, 1983.

    Google Scholar 

  18. Gabbay, D. M. LDS — Labelled Deductive Systems (Volume 1 — Foundations), Clarendon Press, Oxford, 1996.

    Google Scholar 

  19. Gabbay, D. M., and F. Guenthner, editors, Handbook of Philosophical Logic, D. Reidel Publishing Company, Dordrecht, 1983–1986.

    Google Scholar 

  20. Gardner, P., 'A new type theory for representing logics', in A. Voronkov, editor, Proceedings of LPAR'93, LNAI 698, 146-157, Springer, Berlin, 1993.

    Google Scholar 

  21. Gardner, P., 'Equivalences between logics and their representing type theories' Mathematical Structures in Computer Science 5, 323-349, 1995.

    Google Scholar 

  22. Gentzen, G., 'Untersuchungen über das logische Schließen I, II', Mathematische Zeitschrift 39, 176-210, 405–431, 1934–1935. English translation in [23].

    Google Scholar 

  23. Gentzen, G., 'Investigations into logical deduction' in M. Szabo, editor, The collected papers of Gerhard Gentzen, 68-131, North Holland, Amsterdam, 1969.

    Google Scholar 

  24. Girard, J.-Y., 'Linear logic', Theoretical Computer Science 50, 1-102, 1987.

    Google Scholar 

  25. Goldblatt, R., 'Semantical analysis of orthologic', Journal of Philosophical Logic 31, 9-35, 1974.

    Google Scholar 

  26. Harper, R., F. Honsell, and G. Plotkin, 'A framework for defining logics', Journal of the ACM 40(1), 143-184, 1993.

    Google Scholar 

  27. Herzig, A., Raisonnement Automatique en Logique Modale et Algorithmes d'Unification, PhD thesis, Université Paul-Sabatier, Toulouse, 1989.

    Google Scholar 

  28. Honsell, F., and M. Miculan, 'A natural deduction approach to dynamic logics', in S. Berardi and M. Coppo, editors, Proceedings of TYPES'95, LNCS 1158, 165-182, Springer, Berlin, 1996.

    Google Scholar 

  29. Hughes, G., and M. Cresswell, A Companion to Modal Logic, Methuen, London, 1984.

  30. Humberstone, I., 'Interval semantics for tense logic: Some remarks', Journal of Philosophical Logic 8, 171-196, 1979.

    Google Scholar 

  31. JÓnsson, B., and A. Tarski, 'Boolean algebras with operators', American Journal of Mathematics 73–74, 891-939, 127–162, 1951–1952.

    Google Scholar 

  32. Martini, S., and A. Masini, 'A computational interpretation of modal proofs', in H. Wansing, editor, Proof Theory of Modal Logic, 213-241, Kluwer Academic Publishers, Dordrecht, 1996.

    Google Scholar 

  33. Masini, A., '2-sequent calculus: a proof theory of modalities', Annals of Pure and Applied Logic 58, 229-246, 1992.

    Google Scholar 

  34. Nederpelt, R. P., J. H. Geuvers, and R. C. de Vrijer, editors, Selected Papers on Automath, Elsevier, Amsterdam, 1994.

    Google Scholar 

  35. Ohlbach, H. J., A Resolution Calculus for Modal Logics, PhD thesis, Universität Kaiserslautern, Kaiserslautern, Germany, 1988.

    Google Scholar 

  36. Ohlbach, H. J., 'Translation methods for non-classical logics: an overview', Bulletin of the IGPL 1(1), 69-90, 1993.

    Google Scholar 

  37. Orlowska, E., 'Relational interpretation of modal logics', in H. Andréka, J. D. Monk, and I. Németi, editors, Algebraic Logic, North-Holland, Amsterdam, 1991.

    Google Scholar 

  38. Orlowska, E., 'Relational proof system for relevant logics', Journal of Symbolic Logic 57(4), 1425-1440, 1992.

    Google Scholar 

  39. Paulson L., 'The foundation of a generic theorem prover', Journal of Automated Reasoning 5, 363-397, 1989.

    Google Scholar 

  40. Paulson, L., Isabelle: A Generic Theorem Prover, LNCS 828, Springer, Berlin, 1994.

    Google Scholar 

  41. Pfenning, F., 'The practice of logical frameworks', in H. Kirchner, editor, Proceedings of CAAP'96, LNCS 1059, 119-134, Springer, Berlin, 1996.

    Google Scholar 

  42. Prawitz, D., Natural Deduction, a Proof-Theoretical Study, Almqvist and Wiksell, Stockholm, 1965.

    Google Scholar 

  43. Prawitz, D., 'Ideas and results in proof theory', in J. E. Fensted, editor, Proceedings of the 2nd Scandinavian Logic Symposium, 235-307. North-Holland, Amsterdam, 1971.

    Google Scholar 

  44. Restall, G., 'Display logic and gaggle theory', Technical Report TR-ARP-22-95, Australian National University, Dec. 7, 1995.

  45. Restall, G., 'Negation in relevant logics (how I stopped worrying and learned to love the Routley star)', Technical Report TR-ARP-3-95, Australian National University, Feb. 20, 1995.

  46. Routley, R., and R. Meyer, 'The semantics of entailment — II', Journal of Philosophical Logic 1, 53-73, 1972.

    Google Scholar 

  47. Routley, R., V. Plumwood, R. Meyer, and R. Brady, Relevant Logics and their Rivals, Ridgeview, Atascadero, California, 1982.

    Google Scholar 

  48. Russo, A., Modal Logics as Labelled Deductive Systems, PhD thesis, Department of Computing, Imperial College, London, 1996.

    Google Scholar 

  49. Shoenfield, J. R., Mathematical Logic, Addison Wesley, Reading, Massachusetts, 1967.

    Google Scholar 

  50. Simpson, A., The Proof Theory and Semantics of Intuitionistic Modal Logic, PhD thesis, University of Edinburgh, Edinburgh, 1993.

    Google Scholar 

  51. Sundholm, G., Proof theory and meaning, 471-506, volume 3 of Gabbay and Guenthner [19], 1986.

    Google Scholar 

  52. Troelstra, A. S., and H. Schwichtenberg, Basic proof theory, Cambridge University Press, Cambridge, 1996.

    Google Scholar 

  53. van Benthem, J., Correspondence theory, 167-248, volume 2 of Gabbay and Guenthner [19], 1984.

    Google Scholar 

  54. van Benthem, J., Modal Logic and Classical Logic, Bibliopolis, Napoli, 1985.

    Google Scholar 

  55. van Dalen, D., Logic and Structure, Springer, Berlin, 1994.

    Google Scholar 

  56. Viganò, L., A Framework for Non-Classical Logics, PhD thesis, Universität des Saarlandes, Saarbrücken, Germany, 1997.

    Google Scholar 

  57. Wansing, H., 'Sequent calculi for normal modal propositional logics', Journal of Logic and Computation 4(2), 125-142, 1994.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik Universität Freiburg Am Flughafen 17, D-79110, Freiburg, Germany

    David Basin

  2. Max-Planck-Institut für Informatik Im Stadtwald, D-66123, Saarbrücken, Germany

    Seán Matthews & Luca Viganò

Authors
  1. David Basin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Seán Matthews
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Luca Viganò
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

About this article

Cite this article

Basin, D., Matthews, S. & Viganò, L. Natural Deduction for Non-Classical Logics. Studia Logica 60, 119–160 (1998). https://doi.org/10.1023/A:1005003904639

Download citation

  • Issue Date:

  • DOI: https://doi.org/10.1023/A:1005003904639

Keywords

Search

Navigation