{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:24:35Z","timestamp":1761611075604,"version":"3.43.0"},"reference-count":33,"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:1005060022386","type":"journal-article","created":{"date-parts":[[2002,12,21]],"date-time":"2002-12-21T15:31:12Z","timestamp":1040484672000},"page":"161-208","source":"Crossref","is-referenced-by-count":20,"title":["Encoding Modal Logics in Logical Frameworks"],"prefix":"10.1007","volume":"60","author":[{"given":"Arnon","family":"Avron","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Furio","family":"Honsell","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marino","family":"Miculan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cristian","family":"Paravano","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"155412_CR1","unstructured":"Abramsky, S., D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, Oxford University Press, 1992."},{"key":"155412_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', Infor. Comp. 92, 105-139, Jan. 1991.","journal-title":"Infor. Comp."},{"key":"155412_CR3","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1007\/BF00245294","volume":"9","author":"A. Avron","year":"1992","unstructured":"Avron, A., F. Honsell, I. A. Mason, and R. Pollack, 'Using Typed Lambda Calculus to implement formal systems on a machine', J. Automated Reasoning 9, 309-354, 1992.","journal-title":"J. Automated Reasoning"},{"key":"155412_CR4","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1007\/BF00264250","volume":"21","author":"H. Barringer","year":"1984","unstructured":"Barringer, H., J. H. Cheng, and C. B. Jones, 'A logic covering undefiness in program proofs' Acta Informatica 21, 251-269, 1984.","journal-title":"Acta Informatica"},{"key":"155412_CR5","unstructured":"Basin, D., S. Matthews, and L. Vigan\u00d2, 'A modular presentation of modal logics in a logical framework', this volume, 119-160."},{"key":"155412_CR6","unstructured":"Coen, M., Interactive Program Derivation, PhD thesis, University of Cambridge, 1992."},{"key":"155412_CR7","first-page":"95","volume":"76","author":"T. Coquand","year":"1988","unstructured":"Coquand, T., and G. Huet, 'The calculus of constructions', Information and Control 76, 95-120, 1988.","journal-title":"Information and Control"},{"key":"155412_CR8","volume-title":"The Coq Proof Assistant Reference Manual \u2014 Version 5.10","author":"C. Cornes","year":"1995","unstructured":"Cornes, C., J. Courant, J.-C. Fill\u00c2tre, G. Huet, P. Manoury, C. Mu\u00d1oz, C. Murthy, C. Parent, C. Paulin-Mohring, A. Sa\u00cfbi, and B. Werner, The Coq Proof Assistant Reference Manual \u2014 Version 5.10, INRIA, Rocquencourt, July 1995. Available at ftp:\/\/ftp.inria.fr\/INRIA\/coq\/V5.10\/doc\/Reference-Manual.dvi.Z."},{"key":"155412_CR9","doi-asserted-by":"crossref","unstructured":"Fitting, M., Proof Methods for Modal and Intuitionistic Logic, volume 109 of Synthese Library, Reidel, 1983.","DOI":"10.1007\/978-94-017-2794-5"},{"key":"155412_CR10","doi-asserted-by":"crossref","unstructured":"Fitting, M., 'Tableaus for many-valued modal logic', Studia Logica 55, 63-87, 1995.","DOI":"10.1007\/BF01053032"},{"key":"155412_CR11","unstructured":"Fitting, M., '|eanT\nAP revisited' (unpublished notes, Mar. 1997). Available at ftp:\/\/gillet3.lehman.cuny.edu\/pub\/fitting\/leantap.ps.gz"},{"key":"155412_CR12","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1017\/S0960129500000785","volume":"5","author":"P. Gardner","year":"1995","unstructured":"Gardner, P., 'Equivalence between logics and their representing type theories', Mathematical Structures in Computer Science 5, 323-349, 1995.","journal-title":"Mathematical Structures in Computer Science"},{"key":"155412_CR13","doi-asserted-by":"crossref","unstructured":"Gentzen, G., 'Investigations into logical deduction', in M. Szabo, editor, The collected papers of Gerhard Gentzen, 68-131, North Holland, 1969.","DOI":"10.1016\/S0049-237X(08)70822-X"},{"key":"155412_CR14","doi-asserted-by":"crossref","unstructured":"Harel, D., 'Dynamic logic', in D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, volume II, 497-604, Reidel, 1984.","DOI":"10.1007\/978-94-009-6259-0_10"},{"issue":"1","key":"155412_CR15","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 ACM 40(1), 143-184, Jan. 1993.","journal-title":"Journal of ACM"},{"key":"155412_CR16","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M. Hennessy","year":"1985","unstructured":"Hennessy, M., and R. Milner, 'Algebraic laws for nondeterminism and concurrency', Journal of ACM 32, 137-162, 1985.","journal-title":"Journal of ACM"},{"key":"155412_CR17","doi-asserted-by":"crossref","unstructured":"Honsell, F., and M. Miculan, 'A natural deduction approach to dynamic logics', in S. Berardi and M. Coppo, editors, Proc. of TYPES'95, LNCS number 1158, 165-182, Turin, Mar. 1995, Springer-Verlag, 1996. A preliminar version has been communicated to the TYPES'94 Annual Workshop, B\u00e5stad, July 1994.","DOI":"10.1007\/3-540-61780-9_69"},{"key":"155412_CR18","unstructured":"Hughes, G. E., and M. J. Cresswell, A companion to Modal Logic, Methuen, 1984."},{"key":"155412_CR19","unstructured":"Luo, Z., R. Pollack, and P. Taylor, How to use LEGO (A Preliminary User's Manual), Department of Computer Science, University of Edinburgh, Oct. 1989."},{"key":"155412_CR20","unstructured":"Martin-L\u00d6f, P., 'On the meaning of the logical constants and the justifications of the logic laws', Technical Report 2, Scuola di Specializzazione in Logica Matematica, Dipartimento di Matematica, Universit\u00e0 di Sicna, 1985."},{"key":"155412_CR21","unstructured":"Martini, S, and A. Masini, 'A computational interpretation of modal proofs', in H. Wansing, editor, Proof theory of Modal Logics, Kluwer, 1994."},{"key":"155412_CR22","unstructured":"Merz, S., 'Mechanizing TLA in Isabelle', in R. Rodo\u0161ek, editor, Workshop on Verification in New Orientations, 54-74, Maribor, July 1995. Univ. of Maribor."},{"key":"155412_CR23","unstructured":"Miculan, M., 'The expressive power of structural operational semantics with explicit assumptions', in H. Barendregt and T. Nipkow, editors, Proceedings of TYPES'93, LNCS number 806, 292-320, Springer-Verlag, 1994."},{"key":"155412_CR24","volume-title":"Encoding Logical Theories of Programs","author":"M. Miculan","year":"1997","unstructured":"Miculan, M., Encoding Logical Theories of Programs, PhD thesis, Dipartimento di Informatica, Universit\u00e0 di Pisa, Italy, Mar. 1997."},{"key":"155412_CR25","unstructured":"Nordstr\u00d6m, B., K. Petersson, and J. M. Smith, 'Martin-L\u00f6f's type theory', in Abramsky et al, [1]."},{"key":"155412_CR26","doi-asserted-by":"crossref","unstructured":"Pfenning, F., and H.-C. Wong, 'On a modal \u03bb-calculus for S4', in Proc. MFPS'95, 1995.","DOI":"10.1016\/S1571-0661(04)00028-3"},{"key":"155412_CR27","volume-title":"Natural Deduction","author":"D. Prawitz","year":"1965","unstructured":"Prawitz, D., Natural Deduction, Almqvist & Wiksell, Stockholm, 1965."},{"issue":"4","key":"155412_CR28","doi-asserted-by":"crossref","first-page":"1284","DOI":"10.2307\/2274279","volume":"49","author":"P. Schroeder-Heister","year":"1984","unstructured":"Schroeder-Heister, P., 'A natural extension of natural deduction', J. Symbolic Logic 49(4), 1284-1300, 1984.","journal-title":"J. Symbolic Logic"},{"key":"155412_CR29","unstructured":"Simpson, A., The Proof Theory and Semantics of Intuitionistic Modal Logic, PhD thesis, University of Edinburgh, 1993."},{"key":"155412_CR30","doi-asserted-by":"crossref","unstructured":"Stirling, C., 'Modal and Temporal Logics', in Abramsky et al. [1], 477-563.","DOI":"10.1093\/oso\/9780198537618.003.0005"},{"key":"155412_CR31","series-title":"Monographs in philosophical logic and formal linguistics","volume-title":"Modal logic and classical logic","author":"J. van Benthem","year":"1983","unstructured":"van Benthem, J., Modal logic and classical logic, volume 3 of Monographs in philosophical logic and formal linguistics, Bibliopolis, Napoli, 1983."},{"key":"155412_CR32","unstructured":"Wallen, L. A., Automated Proof Search in Non-Classical Logics, MIT Press, 1990."},{"key":"155412_CR33","unstructured":"Werner, B., Une th\u00e9orie des constructions inductives, PhD thesis, Univ. Paris 7, 1994."}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005060022386.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1005060022386\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005060022386.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,8]],"date-time":"2025-08-08T05:26:20Z","timestamp":1754630780000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1005060022386"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,1]]},"references-count":33,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1998,1]]}},"alternative-id":["155412"],"URL":"https:\/\/doi.org\/10.1023\/a:1005060022386","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"type":"print","value":"0039-3215"},{"type":"electronic","value":"1572-8730"}],"subject":[],"published":{"date-parts":[[1998,1]]}}}