{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T15:34:23Z","timestamp":1725982463999},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319942049"},{"type":"electronic","value":"9783319942056"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-94205-6_28","type":"book-chapter","created":{"date-parts":[[2018,6,29]],"date-time":"2018-06-29T12:22:50Z","timestamp":1530274970000},"page":"422-438","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Constructive Decision via Redundancy-Free Proof-Search"],"prefix":"10.1007","author":[{"given":"Dominique","family":"Larchey-Wendling","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,6,30]]},"reference":[{"key":"28_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2015.06.019","volume":"597","author":"K Bimb\u00f3","year":"2015","unstructured":"Bimb\u00f3, K.: The decidability of the intensional fragment of classical linear logic. Theoret. Comput. Sci. 597, 1\u201317 (2015)","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"28_CR2","doi-asserted-by":"publisher","first-page":"214","DOI":"10.2178\/jsl.7801150","volume":"78","author":"K Bimb\u00f3","year":"2013","unstructured":"Bimb\u00f3, K., Dunn, J.M.: On the decidability of implicational ticket entailment. J. Symb. Log. 78(1), 214\u2013236 (2013)","journal-title":"J. Symb. Log."},{"key":"28_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/BFb0013465","volume-title":"Category Theory and Computer Science","author":"T Coquand","year":"1991","unstructured":"Coquand, T.: A direct proof of the intuitionistic Ramsey theorem. In: Pitt, D.H., Curien, P.-L., Abramsky, S., Pitts, A.M., Poign\u00e9, A., Rydeheard, D.E. (eds.) CTCS 1991. LNCS, vol. 530, pp. 164\u2013172. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/BFb0013465"},{"key":"28_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/BFb0021089","volume-title":"Constructivity in Computer Science","author":"T Coquand","year":"1992","unstructured":"Coquand, T.: Constructive topology and combinatorics. In: Myers, J.P., O\u2019Donnell, M.J. (eds.) Constructivity in CS 1991. LNCS, vol. 613, pp. 159\u2013164. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/BFb0021089"},{"key":"28_CR5","series-title":"Notre Dame mathematical lectures","volume-title":"A Theory of Formal Deductibility","author":"HB Curry","year":"1957","unstructured":"Curry, H.B.: A Theory of Formal Deductibility. Notre Dame mathematical lectures. University of Notre Dame, Dame (1957)"},{"key":"28_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/978-3-319-66902-1_21","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"JE Dawson","year":"2017","unstructured":"Dawson, J.E., Gor\u00e9, R.: Issues in machine-checking the decidability of implicational ticket entailment. In: Schmidt, R.A., Nalon, C. (eds.) TABLEAUX 2017. LNCS, vol. 10501, pp. 347\u2013363. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66902-1_21"},{"issue":"1","key":"28_CR7","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/j.jcss.2012.04.002","volume":"79","author":"S Demri","year":"2012","unstructured":"Demri, S., Jurdzi\u0144ski, M., Lachish, O., Lazi\u0107, R.: The covering and boundedness problems for branching vector addition systems. J. Comput. System Sci. 79(1), 23\u201338 (2012)","journal-title":"J. Comput. System Sci."},{"key":"28_CR8","doi-asserted-by":"crossref","unstructured":"Figueira, D., Figueira, S., Schmitz, S., Schnoebelen, P.: Ackermannian and primitive-recursive bounds with Dickson\u2019s lemma. In: LICS 2011, pp. 269\u2013278 (2011)","DOI":"10.1109\/LICS.2011.39"},{"key":"28_CR9","unstructured":"Figueira, D., Lazic, R., Leroux, J., Mazowiecki, F., Sutre, G.: Polynomial-space completeness of reachability for succinct branching VASS in dimension one. In: ICALP 2017, LIPIcs, vol. 80, pp. 119:1\u201314. Schloss Dagstuhl (2017)"},{"key":"28_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/3-540-48167-2_7","volume-title":"Types for Proofs and Programs","author":"D Fridlender","year":"1999","unstructured":"Fridlender, D.: An interpretation of the fan theorem in type theory. In: Altenkirch, T., Reus, B., Naraschewski, W. (eds.) TYPES 1998. LNCS, vol. 1657, pp. 93\u2013105. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48167-2_7"},{"issue":"6","key":"28_CR11","doi-asserted-by":"publisher","first-page":"1033","DOI":"10.1017\/S0960129505004858","volume":"15","author":"D Galmiche","year":"2005","unstructured":"Galmiche, D., M\u00e9ry, D., Pym, D.: The semantics of BI and resource tableaux. Math. Struct. Comput. Sci. 15(6), 1033\u20131088 (2005)","journal-title":"Math. Struct. Comput. Sci."},{"key":"28_CR12","doi-asserted-by":"publisher","first-page":"324","DOI":"10.2307\/2964568","volume":"24","author":"S Kripke","year":"1959","unstructured":"Kripke, S.: The problem of entailment (abstract). J. Symb. Log. 24, 324 (1959)","journal-title":"J. Symb. Log."},{"key":"28_CR13","unstructured":"Larchey-Wendling, D.: A mechanized inductive proof of Kruskal\u2019s tree theorem (2015). http:\/\/www.loria.fr\/~larchey\/Kruskal"},{"key":"28_CR14","unstructured":"Larchey-Wendling, D.: A constructive mechanization of Kripke-Curry\u2019s method for the decidability of implicational relevance logic (2018). https:\/\/github.com\/DmxLarchey\/Relevant-decidability"},{"key":"28_CR15","series-title":"Synthese Library (Studies in Epistemology, Logic, Methodology, and Philosophy of Science)","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/978-94-010-0526-5_9","volume-title":"Logic, Meaning and Computation","author":"RK Meyer","year":"2001","unstructured":"Meyer, R.K.: Improved decision procedures for pure relevant logic. In: Anderson, C.A., Zel\u00ebny, M. (eds.) Logic, Meaning and Computation. Synthese Library (Studies in Epistemology, Logic, Methodology, and Philosophy of Science), pp. 191\u2013217. Springer, Dordrecht (2001). https:\/\/doi.org\/10.1007\/978-94-010-0526-5_9"},{"issue":"3","key":"28_CR16","doi-asserted-by":"publisher","first-page":"568","DOI":"10.1017\/S0960129512000412","volume":"23","author":"V Padovani","year":"2013","unstructured":"Padovani, V.: Ticket entailment is decidable. Math. Struct. Comput. Sci. 23(3), 568\u2013607 (2013)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"1","key":"28_CR17","doi-asserted-by":"publisher","first-page":"9","DOI":"10.3166\/jancl.15.9-23","volume":"15","author":"J Riche","year":"2005","unstructured":"Riche, J.: Decision procedure of some relevant logics: a constructive perspective. J. Appl. Non-Class. Log. 15(1), 9\u201323 (2005)","journal-title":"J. Appl. Non-Class. Log."},{"key":"28_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/10703163_16","volume-title":"Computer Science Logic","author":"J Riche","year":"1999","unstructured":"Riche, J., Meyer, R.K.: Kripke, Belnap, Urquhart and relevant decidability and complexity. In: Gottlob, G., Grandjean, E., Seyr, K. (eds.) CSL 1998. LNCS, vol. 1584, pp. 224\u2013240. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/10703163_16"},{"issue":"2","key":"28_CR19","doi-asserted-by":"publisher","first-page":"641","DOI":"10.1017\/jsl.2015.7","volume":"81","author":"S Schmitz","year":"2016","unstructured":"Schmitz, S.: Implicational relevance logic is 2-ExpTime-complete. J. Symb. Log. 81(2), 641\u2013661 (2016)","journal-title":"J. Symb. Log."},{"issue":"1","key":"28_CR20","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1145\/2893582.2893585","volume":"3","author":"S Schmitz","year":"2016","unstructured":"Schmitz, S.: The complexity of reachability in vector addition systems. ACM SIGLOG News 3(1), 4\u201321 (2016)","journal-title":"ACM SIGLOG News"},{"issue":"12","key":"28_CR21","first-page":"2086","volume":"11","author":"H Schwichtenberg","year":"2005","unstructured":"Schwichtenberg, H.: A direct proof of the equivalence between Brouwer\u2019s Fan theorem and K\u00f6nig\u2019s lemma with a uniqueness hypothesis. J. UCS 11(12), 2086\u20132095 (2005)","journal-title":"J. UCS"},{"issue":"4","key":"28_CR22","doi-asserted-by":"publisher","first-page":"1059","DOI":"10.2307\/2274261","volume":"49","author":"A Urquhart","year":"1984","unstructured":"Urquhart, A.: The undecidability of entailment and relevant implication. J. Symb. Log. 49(4), 1059\u20131073 (1984)","journal-title":"J. Symb. Log."},{"issue":"2","key":"28_CR23","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1112\/jlms\/s2-47.2.193","volume":"s2\u201347","author":"W Veldman","year":"1993","unstructured":"Veldman, W., Bezem, M.: Ramsey\u2019s theorem and the pigeonhole principle in intuitionistic mathematics. J. Lond. Math. Soc. s2\u201347(2), 193\u2013211 (1993)","journal-title":"J. Lond. Math. Soc."},{"key":"28_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-642-32347-8_17","volume-title":"Interactive Theorem Proving","author":"D Vytiniotis","year":"2012","unstructured":"Vytiniotis, D., Coquand, T., Wahlstedt, D.: Stop when you are almost-full. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 250\u2013265. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32347-8_17"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-94205-6_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,4]],"date-time":"2020-11-04T14:18:12Z","timestamp":1604499492000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-94205-6_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319942049","9783319942056"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-94205-6_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}