{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T04:11:12Z","timestamp":1748751072192,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662488980"},{"type":"electronic","value":"9783662488997"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-48899-7_8","type":"book-chapter","created":{"date-parts":[[2015,11,21]],"date-time":"2015-11-21T03:59:28Z","timestamp":1448078368000},"page":"97-111","source":"Crossref","is-referenced-by-count":0,"title":["Decidability, Introduction Rules and Automata"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Dowek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ying","family":"Jiang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,22]]},"reference":[{"issue":"1","key":"8_CR1","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1145\/363647.363681","volume":"48","author":"D Basin","year":"2001","unstructured":"Basin, D., Ganzinger, H.: Automated complexity analysis based on ordered resolution. J. ACM 48(1), 70\u2013109 (2001)","journal-title":"J. ACM"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/3-540-63141-0_10","volume-title":"Concurrency Theory","author":"A Bouajjani","year":"1997","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: application to model-checking. In: Mazurkiewicz, A.W., Winkowski, J. (eds.) Concurrency Theory. LNCS, vol. 1243, pp. 135\u2013150. Springer, Heidelberg (1997)"},{"key":"8_CR3","unstructured":"Dowek, G., Jiang, Y.: Cut-elimination and the decidability of reachability in alternating pushdown systems (2014). arXiv:1410.8470 [cs.LO]"},{"issue":"3","key":"8_CR4","doi-asserted-by":"publisher","first-page":"795","DOI":"10.2307\/2275431","volume":"57","author":"R Dyckhoff","year":"1992","unstructured":"Dyckhoff, R.: Contraction-free sequent calculi for intuitionistic logic. J. Symb. Log. 57(3), 795\u2013807 (1992)","journal-title":"J. Symb. Log."},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/11780342_19","volume-title":"Logical Approaches to Computational Barriers","author":"R Dyckhoff","year":"2006","unstructured":"Dyckhoff, R., Lengrand, S.: LJQ: a strongly focused calculus for intuitionistic logic. In: Beckmann, A., Berger, U., L\u00f6we, B., Tucker, J.V. (eds.) CiE 2006. LNCS, vol. 3988, pp. 173\u2013185. Springer, Heidelberg (2006)"},{"key":"8_CR6","doi-asserted-by":"publisher","first-page":"1499","DOI":"10.2307\/2695061","volume":"65","author":"R Dyckhoff","year":"2000","unstructured":"Dyckhoff, R., Negri, S.: Admissibility of structural rules for contraction-free systems of intuitionistic logic. J. Symb. Log. 65, 1499\u20131518 (2000)","journal-title":"J. Symb. Log."},{"key":"8_CR7","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1017\/S096012950100336X","volume":"11","author":"J-Y Girard","year":"2001","unstructured":"Girard, J.-Y.: Locus solum. Math. Struct. Comput. Sci. 11, 301\u2013506 (2001)","journal-title":"Math. Struct. Comput. Sci."},{"key":"8_CR8","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":"8_CR9","doi-asserted-by":"crossref","unstructured":"Fr\u00fchwirth, T., Shapiro, E., Vardi, M., Yardeni, E.: Logic programs as types for logic programs. In: Logic in Computer Science, pp. 300\u2013309 (1991)","DOI":"10.1109\/LICS.1991.151654"},{"issue":"3","key":"8_CR10","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1016\/j.ipl.2005.04.007","volume":"95","author":"J Goubault-Larrecq","year":"2005","unstructured":"Goubault-Larrecq, J.: Deciding H $$_1$$ by resolution. Inf. Process. Lett. 95(3), 401\u2013408 (2005)","journal-title":"Inf. Process. Lett."},{"key":"8_CR11","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1093\/logcom\/3.1.63","volume":"3","author":"J Hudelmaier","year":"1993","unstructured":"Hudelmaier, J.: An $$O(n \\log n)$$ -space decision procedure for intuitionistic propositional logic. J. Log. Comput. 3, 63\u201376 (1993)","journal-title":"J. Log. Comput."},{"key":"8_CR12","volume-title":"Introduction to Metamathematics","author":"SC Kleene","year":"1952","unstructured":"Kleene, S.C.: Introduction to Metamathematics. North-Holland, Amsterdam (1952)"},{"issue":"2","key":"8_CR13","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1145\/151261.151265","volume":"40","author":"DA McAllester","year":"1993","unstructured":"McAllester, D.A.: Automatic recognition of tractability in inference relations. J. ACM 40(2), 284\u2013303 (1993)","journal-title":"J. ACM"},{"key":"8_CR14","volume-title":"Natural Deduction","author":"D Prawitz","year":"1965","unstructured":"Prawitz, D.: Natural Deduction. Almqvist & Wiksell, Stockholm (1965)"},{"issue":"94","key":"8_CR15","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1090\/trans2\/094\/02","volume":"2","author":"NN Vorob\u2019ev","year":"1970","unstructured":"Vorob\u2019ev, N.N.: A new algorithm for derivability in the constructive propositional calculus. Am. Math. Soc. Transl. 2(94), 37\u201371 (1970)","journal-title":"Am. Math. Soc. Transl."}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-48899-7_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T13:28:09Z","timestamp":1748698089000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-48899-7_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662488980","9783662488997"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-48899-7_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}