{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T22:47:32Z","timestamp":1762296452018,"version":"3.43.0"},"reference-count":57,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Studia Logica"],"published-print":{"date-parts":[[1998,1]]},"DOI":"10.1023\/a:1005003904639","type":"journal-article","created":{"date-parts":[[2002,12,21]],"date-time":"2002-12-21T15:31:12Z","timestamp":1040484672000},"page":"119-160","source":"Crossref","is-referenced-by-count":28,"title":["Natural Deduction for Non-Classical Logics"],"prefix":"10.1007","volume":"60","author":[{"given":"David","family":"Basin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Se\u00e1n","family":"Matthews","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luca","family":"Vigan\u00f2","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"155409_CR1","volume-title":"Entailment, The Logic of Relevance and Necessity","author":"A. R. Anderson","year":"1992","unstructured":"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."},{"key":"155409_CR2","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1016\/0890-5401(91)90023-U","volume":"92","author":"A. Avron","year":"1991","unstructured":"Avron, A., 'Simple consequence relations', Information and Computation 92, 105-139, 1991.","journal-title":"Information and Computation"},{"key":"155409_CR3","unstructured":"Avron, A., F. Honsell, M. Miculan, and C. Paravano, 'Encoding modal logics in logical frameworks', this issue, 161-208."},{"key":"155409_CR4","first-page":"386","volume-title":"Proceedings of KR'96","author":"D. Basin","year":"1996","unstructured":"Basin, D., S. Matthews, and L. Vigan\u00d2, '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."},{"key":"155409_CR5","doi-asserted-by":"crossref","unstructured":"Basin, D., S. Matthews, and L. Vigan\u00d2, 'Labelled propositional modal logics: theory and practice', Journal of Logic and Computation 7(6), 1997.","DOI":"10.1093\/logcom\/7.6.685"},{"key":"155409_CR6","first-page":"357","volume":"11","author":"N. D. Belnap Jr.","year":"1982","unstructured":"Belnap, Jr. N. D., 'Display logic', Journal of Philosophical Logic 11, 357-417, 1982.","journal-title":"Journal of Philosophical Logic"},{"key":"155409_CR7","first-page":"1","volume-title":"Handbook of Philosophical Logic","author":"R. Bull","year":"1984","unstructured":"Bull, R., and K. Segerberg, Basic modal logic, 1-88, volume 2 of Gabbay and Guenthner [19], 1984."},{"key":"155409_CR8","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1007\/BF00881958","volume":"13","author":"M. D'Agostino","year":"1994","unstructured":"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.","journal-title":"Journal of Automated Reasoning"},{"issue":"1","key":"155409_CR9","doi-asserted-by":"crossref","first-page":"149","DOI":"10.2307\/2273797","volume":"50","author":"K. Do\u0160en","year":"1985","unstructured":"Do\u0160en, K., 'Sequent-systems for modal logic', Journal of Symbolic Logic 50(1), 149-168, 1985.","journal-title":"Journal of Symbolic Logic"},{"key":"155409_CR10","first-page":"15","volume":"20","author":"K. Do\u0160en","year":"1986","unstructured":"Do\u0160en, K., 'Negation as a modal operator', Reports on Mathematical Logic 20, 15-27, 1986.","journal-title":"Reports on Mathematical Logic"},{"key":"155409_CR11","first-page":"215","volume-title":"Truth and other enigmas","author":"M. Dummett","year":"1978","unstructured":"Dummett, M., 'The philosophical basis of intuitionistic logic', in Truth and other enigmas, 215-247, Harvard University Press, Cambridge, Massachusetts, 1978."},{"key":"155409_CR12","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/978-94-009-5203-4_3","volume-title":"Handbook of Philosophical Logic","author":"J. M. Dunn","year":"1986","unstructured":"Dunn, J. M., Relevance logic and entailment, 117-224, volume 3 of Gabbay and Guenthner [19], 1986."},{"key":"155409_CR13","first-page":"331","volume-title":"Philosophical Perspectives","author":"J. M. Dunn","year":"1994","unstructured":"Dunn, J. M., 'Star and perp: Two treatments of negation', in J. Tomberlin, editor, Philosophical Perspectives, volume 7, 331-357, Ridgeview, Atascadero, California, 1994."},{"key":"155409_CR14","first-page":"335","volume-title":"Logik und Mathematik (Frege Kolloquium '93)","author":"J. M. Dunn","year":"1995","unstructured":"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."},{"key":"155409_CR15","doi-asserted-by":"crossref","unstructured":"Dunn, J. M., 'Positive modal logic', Studia Logica 55, 301-317, 1995.","DOI":"10.1007\/BF01061239"},{"key":"155409_CR16","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/978-94-009-0349-4_4","volume-title":"Frontiers of Combining Systems","author":"L. Fari\u00d1as Del Cerro","year":"1996","unstructured":"Fari\u00d1as 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."},{"key":"155409_CR17","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-2794-5","volume-title":"Proof Methods for Modal and Intuitionistic Logics","author":"M. Fitting","year":"1983","unstructured":"Fitting, M., Proof Methods for Modal and Intuitionistic Logics, Kluwer Academic Publishers, Dordrecht, 1983."},{"key":"155409_CR18","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198538332.001.0001","volume-title":"LDS \u2014 Labelled Deductive Systems (Volume 1 \u2014 Foundations)","author":"D. M. Gabbay","year":"1996","unstructured":"Gabbay, D. M.\nLDS \u2014 Labelled Deductive Systems (Volume 1 \u2014 Foundations), Clarendon Press, Oxford, 1996."},{"volume-title":"Handbook of Philosophical Logic","year":"1983","key":"155409_CR19","unstructured":"Gabbay, D. M., and F. Guenthner, editors, Handbook of Philosophical Logic, D. Reidel Publishing Company, Dordrecht, 1983\u20131986."},{"key":"155409_CR20","series-title":"LNAI","first-page":"146","volume-title":"Proceedings of LPAR'93","author":"P. Gardner","year":"1993","unstructured":"Gardner, P., 'A new type theory for representing logics', in A. Voronkov, editor, Proceedings of LPAR'93, LNAI 698, 146-157, Springer, Berlin, 1993."},{"key":"155409_CR21","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1017\/S0960129500000785","volume":"5","author":"P. Gardner","year":"1995","unstructured":"Gardner, P., 'Equivalences between logics and their representing type theories' Mathematical Structures in Computer Science 5, 323-349, 1995.","journal-title":"Mathematical Structures in Computer Science"},{"key":"155409_CR22","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1934","unstructured":"Gentzen, G., 'Untersuchungen \u00fcber das logische Schlie\u00dfen I, II', Mathematische Zeitschrift 39, 176-210, 405\u2013431, 1934\u20131935. English translation in [23].","journal-title":"Mathematische Zeitschrift"},{"key":"155409_CR23","first-page":"68","volume-title":"The collected papers of Gerhard Gentzen","author":"G. Gentzen","year":"1969","unstructured":"Gentzen, G., 'Investigations into logical deduction' in M. Szabo, editor, The collected papers of Gerhard Gentzen, 68-131, North Holland, Amsterdam, 1969."},{"key":"155409_CR24","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.-Y. Girard","year":"1987","unstructured":"Girard, J.-Y., 'Linear logic', Theoretical Computer Science 50, 1-102, 1987.","journal-title":"Theoretical Computer Science"},{"key":"155409_CR25","first-page":"9","volume":"31","author":"R. Goldblatt","year":"1974","unstructured":"Goldblatt, R., 'Semantical analysis of orthologic', Journal of Philosophical Logic 31, 9-35, 1974.","journal-title":"Journal of Philosophical Logic"},{"issue":"1","key":"155409_CR26","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"Harper, R., F. Honsell, and G. Plotkin, 'A framework for defining logics', Journal of the ACM 40(1), 143-184, 1993.","journal-title":"Journal of the ACM"},{"key":"155409_CR27","volume-title":"Raisonnement Automatique en Logique Modale et Algorithmes d'Unification","author":"A. Herzig","year":"1989","unstructured":"Herzig, A., Raisonnement Automatique en Logique Modale et Algorithmes d'Unification, PhD thesis, Universit\u00e9 Paul-Sabatier, Toulouse, 1989."},{"key":"155409_CR28","series-title":"LNCS","first-page":"165","volume-title":"Proceedings of TYPES'95","author":"F. Honsell","year":"1996","unstructured":"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."},{"key":"155409_CR29","unstructured":"Hughes, G., and M. Cresswell, A Companion to Modal Logic, Methuen, London, 1984."},{"key":"155409_CR30","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/BF00258426","volume":"8","author":"I. Humberstone","year":"1979","unstructured":"Humberstone, I., 'Interval semantics for tense logic: Some remarks', Journal of Philosophical Logic 8, 171-196, 1979.","journal-title":"Journal of Philosophical Logic"},{"key":"155409_CR31","doi-asserted-by":"crossref","first-page":"891","DOI":"10.2307\/2372123","volume":"73\u201374","author":"B. J\u00d3nsson","year":"1951","unstructured":"J\u00d3nsson, B., and A. Tarski, 'Boolean algebras with operators', American Journal of Mathematics 73\u201374, 891-939, 127\u2013162, 1951\u20131952.","journal-title":"American Journal of Mathematics"},{"key":"155409_CR32","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/978-94-017-2798-3_12","volume-title":"Proof Theory of Modal Logic","author":"S. Martini","year":"1996","unstructured":"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."},{"key":"155409_CR33","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1016\/0168-0072(92)90029-Y","volume":"58","author":"A. Masini","year":"1992","unstructured":"Masini, A., '2-sequent calculus: a proof theory of modalities', Annals of Pure and Applied Logic 58, 229-246, 1992.","journal-title":"Annals of Pure and Applied Logic"},{"volume-title":"Selected Papers on Automath","year":"1994","key":"155409_CR34","unstructured":"Nederpelt, R. P., J. H. Geuvers, and R. C. de Vrijer, editors, Selected Papers on Automath, Elsevier, Amsterdam, 1994."},{"key":"155409_CR35","volume-title":"A Resolution Calculus for Modal Logics","author":"H. J. Ohlbach","year":"1988","unstructured":"Ohlbach, H. J., A Resolution Calculus for Modal Logics, PhD thesis, Universit\u00e4t Kaiserslautern, Kaiserslautern, Germany, 1988."},{"issue":"1","key":"155409_CR36","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1093\/jigpal\/1.1.69","volume":"1","author":"H. J. Ohlbach","year":"1993","unstructured":"Ohlbach, H. J., 'Translation methods for non-classical logics: an overview', Bulletin of the IGPL 1(1), 69-90, 1993.","journal-title":"Bulletin of the IGPL"},{"key":"155409_CR37","volume-title":"Algebraic Logic","author":"E. Orlowska","year":"1991","unstructured":"Orlowska, E., 'Relational interpretation of modal logics', in H. Andr\u00e9ka, J. D. Monk, and I. N\u00e9meti, editors, Algebraic Logic, North-Holland, Amsterdam, 1991."},{"issue":"4","key":"155409_CR38","doi-asserted-by":"crossref","first-page":"1425","DOI":"10.2307\/2275375","volume":"57","author":"E. Orlowska","year":"1992","unstructured":"Orlowska, E., 'Relational proof system for relevant logics', Journal of Symbolic Logic 57(4), 1425-1440, 1992.","journal-title":"Journal of Symbolic Logic"},{"key":"155409_CR39","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/BF00248324","volume":"5","author":"L. Paulson","year":"1989","unstructured":"Paulson L., 'The foundation of a generic theorem prover', Journal of Automated Reasoning 5, 363-397, 1989.","journal-title":"Journal of Automated Reasoning"},{"key":"155409_CR40","series-title":"LNCS","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"L. Paulson","year":"1994","unstructured":"Paulson, L., Isabelle: A Generic Theorem Prover, LNCS 828, Springer, Berlin, 1994."},{"key":"155409_CR41","series-title":"LNCS","first-page":"119","volume-title":"Proceedings of CAAP'96","author":"F. Pfenning","year":"1996","unstructured":"Pfenning, F., 'The practice of logical frameworks', in H. Kirchner, editor, Proceedings of CAAP'96, LNCS 1059, 119-134, Springer, Berlin, 1996."},{"key":"155409_CR42","volume-title":"Natural Deduction, a Proof-Theoretical Study","author":"D. Prawitz","year":"1965","unstructured":"Prawitz, D., Natural Deduction, a Proof-Theoretical Study, Almqvist and Wiksell, Stockholm, 1965."},{"key":"155409_CR43","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1016\/S0049-237X(08)70849-8","volume-title":"Proceedings of the 2nd Scandinavian Logic Symposium","author":"D. Prawitz","year":"1971","unstructured":"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."},{"key":"155409_CR44","unstructured":"Restall, G., 'Display logic and gaggle theory', Technical Report TR-ARP-22-95, Australian National University, Dec. 7, 1995."},{"key":"155409_CR45","unstructured":"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."},{"key":"155409_CR46","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/BF00649991","volume":"1","author":"R. Routley","year":"1972","unstructured":"Routley, R., and R. Meyer, 'The semantics of entailment \u2014 II', Journal of Philosophical Logic 1, 53-73, 1972.","journal-title":"Journal of Philosophical Logic"},{"key":"155409_CR47","volume-title":"Relevant Logics and their Rivals","author":"R. Routley","year":"1982","unstructured":"Routley, R., V. Plumwood, R. Meyer, and R. Brady, Relevant Logics and their Rivals, Ridgeview, Atascadero, California, 1982."},{"key":"155409_CR48","volume-title":"Modal Logics as Labelled Deductive Systems","author":"A. Russo","year":"1996","unstructured":"Russo, A., Modal Logics as Labelled Deductive Systems, PhD thesis, Department of Computing, Imperial College, London, 1996."},{"key":"155409_CR49","volume-title":"Mathematical Logic","author":"J. R. Shoenfield","year":"1967","unstructured":"Shoenfield, J. R., Mathematical Logic, Addison Wesley, Reading, Massachusetts, 1967."},{"key":"155409_CR50","volume-title":"The Proof Theory and Semantics of Intuitionistic Modal Logic","author":"A. Simpson","year":"1993","unstructured":"Simpson, A., The Proof Theory and Semantics of Intuitionistic Modal Logic, PhD thesis, University of Edinburgh, Edinburgh, 1993."},{"key":"155409_CR51","doi-asserted-by":"crossref","first-page":"471","DOI":"10.1007\/978-94-009-5203-4_8","volume-title":"Handbook of Philosophical Logic","author":"G. Sundholm","year":"1986","unstructured":"Sundholm, G., Proof theory and meaning, 471-506, volume 3 of Gabbay and Guenthner [19], 1986."},{"key":"155409_CR52","volume-title":"Basic proof theory","author":"A. S. Troelstra","year":"1996","unstructured":"Troelstra, A. S., and H. Schwichtenberg, Basic proof theory, Cambridge University Press, Cambridge, 1996."},{"key":"155409_CR53","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/978-94-009-6259-0_4","volume-title":"Handbook of Philosophical Logic","author":"J. van Benthem","year":"1984","unstructured":"van Benthem, J., Correspondence theory, 167-248, volume 2 of Gabbay and Guenthner [19], 1984."},{"key":"155409_CR54","volume-title":"Modal Logic and Classical Logic","author":"J. van Benthem","year":"1985","unstructured":"van Benthem, J., Modal Logic and Classical Logic, Bibliopolis, Napoli, 1985."},{"key":"155409_CR55","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-02962-6","volume-title":"Logic and Structure","author":"D. van Dalen","year":"1994","unstructured":"van Dalen, D., Logic and Structure, Springer, Berlin, 1994."},{"key":"155409_CR56","volume-title":"A Framework for Non-Classical Logics","author":"L. Vigan\u00f2","year":"1997","unstructured":"Vigan\u00f2, L., A Framework for Non-Classical Logics, PhD thesis, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany, 1997."},{"issue":"2","key":"155409_CR57","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1093\/logcom\/4.2.125","volume":"4","author":"H. Wansing","year":"1994","unstructured":"Wansing, H., 'Sequent calculi for normal modal propositional logics', Journal of Logic and Computation 4(2), 125-142, 1994.","journal-title":"Journal of Logic and Computation"}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005003904639.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1005003904639\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005003904639.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,8]],"date-time":"2025-08-08T05:16:25Z","timestamp":1754630185000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1005003904639"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,1]]},"references-count":57,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1998,1]]}},"alternative-id":["155409"],"URL":"https:\/\/doi.org\/10.1023\/a:1005003904639","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"type":"print","value":"0039-3215"},{"type":"electronic","value":"1572-8730"}],"subject":[],"published":{"date-parts":[[1998,1]]}}}