乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,17]],"date-time":"2023-01-17T11:49:34Z","timestamp":1673956174791},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"7","license":[{"start":{"date-parts":[[2020,6,24]],"date-time":"2020-06-24T00:00:00Z","timestamp":1592956800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,6,24]],"date-time":"2020-06-24T00:00:00Z","timestamp":1592956800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"name":"ANR-FWF TICAMORE","award":["ANR-16-CE91-0002"]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2020,10]]},"DOI":"10.1007\/s10817-020-09555-y","type":"journal-article","created":{"date-parts":[[2020,6,24]],"date-time":"2020-06-24T04:13:09Z","timestamp":1592971989000},"page":"1197-1219","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Constructive Decision via Redundancy-Free Proof-Search"],"prefix":"10.1007","volume":"64","author":[{"ORCID":"http:\/\/orcid.org\/0000-0001-9860-7203","authenticated-orcid":false,"given":"Dominique","family":"Larchey-Wendling","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,6,24]]},"reference":[{"key":"9555_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. Theor. Comput. Sci. 597, 1\u201317 (2015)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"9555_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":"9555_CR3","doi-asserted-by":"crossref","unstructured":"Coquand, T.: A direct proof of the intuitionistic Ramsey Theorem. In: Pitt D.H., Curien PL., Abramsky S., Pitts A.M., Poign\u00e9 A., Rydeheard D.E. (eds) Category Theory and Computer Science. CTCS 1991. Lecture Notes in Computer Science, vol 530, pp. 164\u2013172. Springer (1991)","DOI":"10.1007\/BFb0013465"},{"key":"9555_CR4","doi-asserted-by":"crossref","unstructured":"Coquand, T.: Constructive topology and combinatorics. In: Myers J.P., O\u2019Donnell M.J. (eds) Constructivity in Computer Science. Constructivity in CS 1991. Lecture Notes in Computer Science, vol 613, pp. 159\u2013164. Springer (1992)","DOI":"10.1007\/BFb0021089"},{"key":"9555_CR5","volume-title":"A Theory of Formal Deductibility. Notre Dame mathematical lectures","author":"HB Curry","year":"1957","unstructured":"Curry, H.B.: A Theory of Formal Deductibility. Notre Dame mathematical lectures. University of Notre Dame, Notre Dame (1957)"},{"key":"9555_CR6","doi-asserted-by":"crossref","unstructured":"Dawson, J.E., Gor\u00e9, R.: Issues in Machine-Checking the Decidability of Implicational Ticket Entailment. In: TABLEAUX 2017, LNAI, vol. 10501, pp. 347\u2013363. Springer International Publishing, Berlin (2017)","DOI":"10.1007\/978-3-319-66902-1_21"},{"issue":"1","key":"9555_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. Syst. Sci. 79(1), 23\u201338 (2012). https:\/\/doi.org\/10.1016\/j.jcss.2012.04.002","journal-title":"J. Comput. Syst. Sci."},{"key":"9555_CR8","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1109\/LICS.2011.39","volume":"2011","author":"D Figueira","year":"2011","unstructured":"Figueira, D., Figueira, S., Schmitz, S., Schnoebelen, P.: Ackermannian and Primitive-Recursive Bounds with Dickson\u2019s Lemma. LICS 2011, 269\u2013278 (2011). https:\/\/doi.org\/10.1109\/LICS.2011.39","journal-title":"LICS"},{"key":"9555_CR9","doi-asserted-by":"publisher","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.\u00a080, pp. 119:1\u201314. Schloss Dagstuhl (2017). https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2017.119","DOI":"10.4230\/LIPIcs.ICALP.2017.119"},{"key":"9555_CR10","doi-asserted-by":"crossref","unstructured":"Fridlender, D.: An Interpretation of the Fan Theorem in Type Theory. In: TYPES\u201998 Selected Papers, LNCS, vol. 1657, pp. 93\u2013105. Springer, Berlin (1999)","DOI":"10.1007\/3-540-48167-2_7"},{"issue":"6","key":"9555_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). https:\/\/doi.org\/10.1017\/S0960129505004858","journal-title":"Math. Struct. Comput. Sci."},{"key":"9555_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":"9555_CR13","doi-asserted-by":"crossref","unstructured":"Larchey-Wendling, D.: Constructive decision via redundancy-free proof-search. In: Automated Reasoning\u20149th International Joint Conference, IJCAR 2018, Lecture Notes in Computer Science, vol. 10900, pp. 422\u2013438. Springer, Berlin (2018)","DOI":"10.1007\/978-3-319-94205-6_28"},{"key":"9555_CR14","first-page":"191","volume-title":"Improved Decision Procedures for Pure Relevant Logic","author":"RK Meyer","year":"2001","unstructured":"Meyer, R.K.: Improved Decision Procedures for Pure Relevant Logic, pp. 191\u2013217. Springer, Dordrecht (2001)"},{"issue":"1\u20132","key":"9555_CR15","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1016\/S0304-3975(02)00024-5","volume":"281","author":"M Okada","year":"2002","unstructured":"Okada, M.: A uniform semantic proof for cut-elimination and completeness of various first and higher order logics. Theor. Comput. Sci. 281(1\u20132), 471\u2013498 (2002)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"9555_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). https:\/\/doi.org\/10.1017\/S0960129512000412","journal-title":"Math. Struct. Comput. Sci."},{"issue":"1","key":"9555_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":"9555_CR18","doi-asserted-by":"crossref","unstructured":"Riche, J., Meyer, R.K.: Kripke, Belnap, Urquhart and Relevant Decidability & Complexity. In: CSL\u201999, pp. 224\u2013240. Springer (1999)","DOI":"10.1007\/10703163_16"},{"issue":"2","key":"9555_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":"9555_CR20","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1145\/2893582.2893585","journal-title":"ACM SIGLOG News"},{"issue":"12","key":"9555_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"},{"key":"9555_CR22","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/j.tcs.2019.02.022","volume":"768","author":"L Stra\u00dfburger","year":"2019","unstructured":"Stra\u00dfburger, L.: On the decision problem for MELL. Theor. Comput. Sci. 768, 91\u201398 (2019)","journal-title":"Theor. Comput. Sci."},{"issue":"4","key":"9555_CR23","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":"9555_CR24","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). https:\/\/doi.org\/10.1112\/jlms\/s2-47.2.193","journal-title":"J. Lond. Math. Soc."},{"key":"9555_CR25","doi-asserted-by":"crossref","unstructured":"Vytiniotis, D., Coquand, T., Wahlstedt, D.: Stop when you are almost-full\u2014adventures in constructive termination. In: ITP 2012, LNCS, vol. 7406, pp. 250\u2013265 (2012)","DOI":"10.1007\/978-3-642-32347-8_17"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09555-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-020-09555-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09555-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,6,23]],"date-time":"2021-06-23T23:51:18Z","timestamp":1624492278000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-020-09555-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,6,24]]},"references-count":25,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2020,10]]}},"alternative-id":["9555"],"URL":"https:\/\/doi.org\/10.1007\/s10817-020-09555-y","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,6,24]]},"assertion":[{"value":"17 April 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 April 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 June 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}