{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:29:47Z","timestamp":1725456587733},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540633884"},{"type":"electronic","value":"9783540695301"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/bfb0014564","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T09:17:33Z","timestamp":1132737453000},"page":"491-514","source":"Crossref","is-referenced-by-count":0,"title":["Extending a logical framework with a modal connective for validity"],"prefix":"10.1007","author":[{"given":"Se\u00e1n","family":"Matthews","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"20_CR1","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1016\/0890-5401(91)90023-U","volume":"92","author":"A. Avron","year":"1991","unstructured":"A. Avron. Simple consequence relations. Inform. and Comput., 92:105\u2013139, 1991.","journal-title":"Inform. and Comput."},{"key":"20_CR2","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1007\/BF00245294","volume":"9","author":"A. Avron","year":"1992","unstructured":"A. Avron, F. Honsell, I. Mason, and R. Pollack. Using typed lambda calculus to implement formal systems on a machine. J. Auto. Reas., 9:309\u2013352, 1992.","journal-title":"J. Auto. Reas."},{"key":"20_CR3","unstructured":"A. Avron, F. Honsell, M. Miculan, and C. Paravano. Encoding modal logics in logical frameworks. Studia Logica, (to appear)."},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"H. P. Barendregt. Lambda calculi with types. In S. Abramsky, D. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2. Oxford University Press, 1992.","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"key":"20_CR5","volume-title":"Proc. KR'96","author":"D. Basin","year":"1996","unstructured":"D. Basin, S. Matthews, and L. Viganb. Implementing modal and relevance logics in a logical framework. In C. Aiello et al., editors, Proc. KR'96. Morgan-Kaufmann, California, 1996."},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"D. Basin, S. Matthews, and L. Viganb. Labelled propositional modal logics: theory and practice. J. Logic Computat., (to appear).","DOI":"10.1093\/logcom\/7.6.685"},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"I. Cervesato and F. Pfenning. A linear logical framework. In 11th Ann. Symp. Logic in Comp. Sci. IEEE Computer Society Press, I996.","DOI":"10.1109\/LICS.1996.561339"},{"key":"20_CR8","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511621192","volume-title":"Modal Logic","author":"B. Chellas","year":"1980","unstructured":"B. Chellas. Modal Logic. Cambridge University Press, New York, 1980."},{"key":"20_CR9","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/BF00156914","volume":"1","author":"K. Dosen","year":"1992","unstructured":"K. Dosen. Modal logic as metalogic. J. Logic, Language and Information, 1:173\u2013201, 1992.","journal-title":"J. Logic, Language and Information"},{"key":"20_CR10","volume-title":"Proc. LADE-9","author":"A. Felty","year":"1988","unstructured":"A. Felty and D. Miller. Specifying theorem provers in a higher-order logic programming language. In E. Lusk and R. Overbeek, editors, Proc. LADE-9. Springer, Berlin, 1988."},{"key":"20_CR11","first-page":"179","volume":"39","author":"G. Gentzen","year":"1934","unstructured":"G. Gentzen. Untersuchen \u00fcber das logische Schliessen. Math. Z., 39:179\u2013210, 405\u2013431, 1934.","journal-title":"Math. Z."},{"key":"20_CR12","volume-title":"Proof Theory and Logical Complexity","author":"J.-Y. Girard","year":"1987","unstructured":"J.-Y. Girard. Proof Theory and Logical Complexity. Bibliopolis, Naples, 1987."},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"I. Hacking. What is logic? J. Philosophy, 76(6), 1979.","DOI":"10.2307\/2025471"},{"key":"20_CR14","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. J. Assoc. Comput. Mach., 40:143\u2013184, 1993.","journal-title":"J. Assoc. Comput. Mach."},{"key":"20_CR15","volume-title":"Introduction to Modal Logic","author":"G. Hughes","year":"1972","unstructured":"G. Hughes and M. Cresswell. Introduction to Modal Logic. Routledge, London, 1972."},{"key":"20_CR16","volume-title":"Introduction to Metamathematics","author":"S. C. Kleene","year":"1952","unstructured":"S. C. Kleene. Introduction to Metamathematics. North-Holland, Amsterdam, 1952."},{"key":"20_CR17","unstructured":"S. Matthews. Logical frameworks for relevance and linear logics. Unpublished."},{"key":"20_CR18","volume-title":"Handbook of Theoretical Computer Science","author":"J. C. Mitchell","year":"1990","unstructured":"J. C. Mitchell. Type systems for programming languages. In J. Van Leeuwen, editor, Handbook of Theoretical Computer Science. Elsevier, Amsterdam, 1990."},{"key":"20_CR19","volume-title":"Selected papers on Automath","author":"R. P. Nederpelt","year":"1994","unstructured":"R. P. Nederpelt et al., editors. Selected papers on Automath. Elsevier, Amsterdam, 1994."},{"key":"20_CR20","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/BF00248324","volume":"5","author":"L. C. Paulson","year":"1989","unstructured":"L. C. Paulson. The foundation of a generic theorem prover. J. Auto. Reas., 5:363\u2013397, 1989.","journal-title":"J. Auto. Reas."},{"key":"20_CR21","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"L. C. Paulson","year":"1994","unstructured":"L. C. Paulson. Isabelle: A Generic Theorem Prover. Springer, Berlin, 1994."},{"key":"20_CR22","doi-asserted-by":"crossref","unstructured":"F. Pfenning. Logic programming in the LF logical framework. In G. Huet and G. Plotkin, editors, Logical Frameworks. Cambridge University Press, 1991.","DOI":"10.1017\/CBO9780511569807.008"},{"key":"20_CR23","volume-title":"Natural Deduction","author":"D. Prawitz","year":"1965","unstructured":"D. Prawitz. Natural Deduction. Almqvist and Wiksell, Stockholm, 1965."},{"key":"20_CR24","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1016\/S0049-237X(08)70849-8","volume-title":"Proc. Second Scandinavian Logic Symp.","author":"D. Prawitz","year":"1971","unstructured":"D. Prawitz. Ideas and results in proof theory. In J. E. Fensted, editor, Proc. Second Scandinavian Logic Symp., pages 235\u2013307. North-Holland, Amsterdam, 1971."},{"key":"20_CR25","unstructured":"A. K. Simpson. Kripke semantics for a logical framework. In Proc. Workshop on Types for Proofs and Programs, B\u00e5stad, 1992. Available from http:\/\/www.dcs.ed.ac.uk\/home\/als\/."}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computer Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0014564","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,1]],"date-time":"2024-02-01T02:24:26Z","timestamp":1706754266000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0014564"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540633884","9783540695301"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/bfb0014564","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}