{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T13:20:40Z","timestamp":1758979240221},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540735946"},{"type":"electronic","value":"9783540735953"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73595-3_9","type":"book-chapter","created":{"date-parts":[[2007,8,30]],"date-time":"2007-08-30T09:31:33Z","timestamp":1188466293000},"page":"116-131","source":"Crossref","is-referenced-by-count":8,"title":["Bidirectional Decision Procedures for the Intuitionistic Propositional Modal Logic IS4"],"prefix":"10.1007","author":[{"given":"Samuli","family":"Heilala","sequence":"first","affiliation":[]},{"given":"Brigitte","family":"Pientka","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"9_CR1","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1023\/A:1005291931660","volume":"65","author":"G.M. Bierman","year":"2000","unstructured":"Bierman, G.M., de Paiva, V.C.V.: On an intuitionistic modal logic. Studia Logica\u00a065(3), 383\u2013416 (2000)","journal-title":"Studia Logica"},{"key":"9_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/11538363_15","volume-title":"Computer Science Logic","author":"K. Chaudhuri","year":"2005","unstructured":"Chaudhuri, K., Pfenning, F.: Focusing the inverse method for linear logic. In: Ong, L. (ed.) CSL 2005. LNCS, vol.\u00a03634, pp. 200\u2013215. Springer, Heidelberg (2005)"},{"issue":"3","key":"9_CR3","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1145\/382780.382785","volume":"48","author":"R. Davies","year":"2001","unstructured":"Davies, R., Pfenning, F.: A modal analysis of staged computation. Journal of the ACM\u00a048(3), 555\u2013604 (2001)","journal-title":"Journal of the ACM"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Degtyarev, A., Voronkov, A.: The inverse method. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 179\u2013272. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50006-0"},{"key":"9_CR5","unstructured":"Dyckhoff, R., Pinto, L.: A permutation-free sequent calculus for intuitionistic logic. Research Report CS\/96\/9, University of St. Andrews (1996)"},{"issue":"1","key":"9_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1997.2627","volume":"137","author":"M. Fairtlough","year":"1997","unstructured":"Fairtlough, M., Mendler, M.: Propositional lax logic. Information and Computation\u00a0137(1), 1\u201333 (1997)","journal-title":"Information and Computation"},{"issue":"2","key":"9_CR7","first-page":"113","volume":"7","author":"F.B. Fitch","year":"1948","unstructured":"Fitch, F.B.: Intuitionistic modal logic with quantifiers. Portugaliae Mathematica\u00a07(2), 113\u2013118 (1948)","journal-title":"Portugaliae Mathematica"},{"issue":"3","key":"9_CR8","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1017\/S0960129500001328","volume":"1","author":"J.-Y. Girard","year":"1991","unstructured":"Girard, J.-Y.: A new constructive logic: Classical logic. Mathematical Structures in Computer Science\u00a01(3), 255\u2013296 (1991)","journal-title":"Mathematical Structures in Computer Science"},{"key":"9_CR9","volume-title":"Proofs and types","author":"J.-Y. Girard","year":"1989","unstructured":"Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and types. Cambridge University Press, Cambridge (1989)"},{"key":"9_CR10","unstructured":"Heilala, S., Pientka, B.: Bidirectional decision procedures for the intuitionistic propositional modal logic IS4. Technical Report SOCS-TR-2007.2, McGill University (May 2007)"},{"key":"9_CR11","unstructured":"Howe, J.M.: Proof search issues in some non-classical logics. PhD thesis, University of St. Andrews (1998)"},{"issue":"4","key":"9_CR12","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1017\/S0960129501003334","volume":"11","author":"J.M. Howe","year":"2001","unstructured":"Howe, J.M.: Proof search in lax logic. Mathematical Structures in Computer Science\u00a011(4), 573\u2013588 (2001)","journal-title":"Mathematical Structures in Computer Science"},{"key":"9_CR13","unstructured":"Moody, J.: Modal logic as a basis for distributed computation. Technical Report CMU-CS-03-194, Carnegie Mellon University (2003)"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Nanevski, A., Pfenning, F., Pientka, B.: Contextual modal type theory. ACM Transactions on Computational Logic (to appear)","DOI":"10.1145\/1352582.1352591"},{"issue":"4","key":"9_CR15","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1017\/S0960129501003322","volume":"11","author":"F. Pfenning","year":"2001","unstructured":"Pfenning, F., Davies, R.: A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science\u00a011(4), 511\u2013540 (2001)","journal-title":"Mathematical Structures in Computer Science"},{"key":"9_CR16","unstructured":"Prawitz, D.: Natural deduction: A proof-theoretical study. Almqvist & Wiksell (1965)"},{"key":"9_CR17","unstructured":"Raths, T., Otten, J., Kreitz, C.: The ILTP problem library for intuitionistic logic, release v1.1. Journal of Automated Reasoning (to appear)"},{"issue":"4","key":"9_CR18","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1305\/ndjfl\/1093890707","volume":"13","author":"T.W. Satre","year":"1972","unstructured":"Satre, T.W.: Natural deduction rules for modal logics. Notre Dame Journal of Formal Logic\u00a013(4), 461\u2013475 (1972)","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"9_CR19","unstructured":"Simpson, A.K.: The proof theory and semantics of intuitionistic modal logic. PhD thesis, University of Edinburgh (1994)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-21"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73595-3_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T09:53:14Z","timestamp":1619517194000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73595-3_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540735946","9783540735953"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73595-3_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}