{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,4]],"date-time":"2022-04-04T10:42:09Z","timestamp":1649068929208},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2014,3,20]],"date-time":"2014-03-20T00:00:00Z","timestamp":1395273600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Log. Univers."],"published-print":{"date-parts":[[2014,6]]},"DOI":"10.1007\/s11787-014-0099-z","type":"journal-article","created":{"date-parts":[[2014,3,19]],"date-time":"2014-03-19T22:56:26Z","timestamp":1395269786000},"page":"141-164","source":"Crossref","is-referenced-by-count":3,"title":["Extracting BB\u2032IW Inhabitants of Simple Types From Proofs in the Sequent Calculus $${LT_\\to^{t}}$$ L T \u2192 t for Implicational Ticket Entailment"],"prefix":"10.1007","volume":"8","author":[{"given":"Katalin","family":"Bimb\u00f3","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J.","family":"Michael Dunn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,3,20]]},"reference":[{"key":"99_CR1","first-page":"388","volume":"25","author":"A.R. Anderson","year":"1960","unstructured":"Anderson A.R.: Entailment shorn of modality (abstract). J. Symb. Log. 25, 388 (1960)","journal-title":"J. Symb. Log."},{"key":"99_CR2","unstructured":"Anderson, A.R., Belnap, N.D.: Entailment. The logic of relevance and necessity, vol. I. Princeton University Press, Princeton (1975)"},{"key":"99_CR3","unstructured":"Anderson, A.R., Belnap, N.D., Dunn, J.M.: Entailment. The logic of relevance and necessity, vol. II. Princeton University Press, Princeton (1992)"},{"key":"99_CR4","unstructured":"Awodey, S.: Category theory. Oxford logic guides, vol. 52, 2nd edn. Oxford University Press, Oxford (2010)"},{"key":"99_CR5","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1017\/S0956796899003524","volume":"10","author":"H. Barendregt","year":"2000","unstructured":"Barendregt H., Ghilezan S.: Lambda terms for natural deduction, sequent calculus and cut elimination. J. Funct. Program. 10, 121\u2013134 (2000)","journal-title":"J. Funct. Program."},{"key":"99_CR6","doi-asserted-by":"crossref","unstructured":"Bimb\u00f3 K.: Types of i-free hereditary right maximal terms. J. Philos. Log. 34, 607\u2013620 (2005)","DOI":"10.1007\/s10992-005-2831-x"},{"key":"99_CR7","unstructured":"Bimb\u00f3, K.: Logics, relevance. In: Jacquette, D. (ed.) Philosophy of logic. In: Gabbay, D., Thagard, P., Woods, J. (eds.) Handbook of the Philosophy of Science. vol. 5, pp. 723\u2013789. Elsevier (North-Holland), Amsterdam (2007)"},{"key":"99_CR8","doi-asserted-by":"crossref","unstructured":"Bimb\u00f3, K.: Combinatory logic: pure, applied and typed. Discrete mathematics and its applications. CRC Press, Boca Raton (2012)","DOI":"10.1201\/b11046"},{"key":"99_CR9","unstructured":"Bimb\u00f3, K., Dunn. J.M.: New consecution calculi for $${R_\\to^{\\,\\mathbf{t}}}$$ R \u2192 t . Notre Dame J. Form. Log. 53, 491\u2013509 (2012)"},{"key":"99_CR10","doi-asserted-by":"crossref","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, 214\u2013236 (2013)","journal-title":"J. Symb. Log."},{"key":"99_CR11","unstructured":"Church, A.: The Calculi of Lambda-conversion, 1st edn. Princeton University Press, Princeton (1941)"},{"key":"99_CR12","unstructured":"Curry, H.B.: Foundations of mathematical logic. McGraw-Hill Book Company, New York (1963). (Dover, New York, NY, 1977)"},{"key":"99_CR13","unstructured":"Curry, H.B., Feys, R.: Combinatory Logic. Studies in logic and the foundations of mathematics, vol. I, 1st edn. North-Holland, Amsterdam (1958)"},{"key":"99_CR14","unstructured":"Dunn, J.M.: A \u2018Gentzen system\u2019 for positive relevant implication, (abstract). J. Symb. Log. 38, 356\u2013357 (1973)"},{"key":"99_CR15","doi-asserted-by":"crossref","unstructured":"Dunn. J.M.: Relevance logic and entailment. In: Gabbay, D.,Guenthner, F. (eds.) Handbook of philosophical logic, vol 3, 1st edn. pp. 117\u2013224. D. Reidel, Dordrecht (1986)","DOI":"10.1007\/978-94-009-5203-4"},{"key":"99_CR16","doi-asserted-by":"crossref","first-page":"505","DOI":"10.1093\/jigpal\/5.4.505","volume":"5","author":"J.M. Dunn","year":"1997","unstructured":"Dunn J.M., Meyer R.K.: Combinators and structurally free logic. Log. J. IGPL. 5, 505\u2013537 (1997)","journal-title":"Log. J. IGPL."},{"key":"99_CR17","unstructured":"Gallier, J.: Constructive logics. Part I. Theor. Comput. Sci. 110(2), 249\u2013339 (1993)"},{"key":"99_CR18","first-page":"288","volume":"1","author":"G. Gentzen","year":"1964","unstructured":"Gentzen G.: Investigations into logical deduction. Am. Philos. Q. 1, 288\u2013306 (1964)","journal-title":"Am. Philos. Q."},{"key":"99_CR19","unstructured":"Helman, G.H.: Restricted lambda abstraction and the interpretation of some nonclassical logics. Ph.D. thesis, University of Pittsburgh (1977)"},{"key":"99_CR20","doi-asserted-by":"crossref","unstructured":"Herbelin, H.: A \u03bb-calculus structure isomorphic to Gentzen-style sequent calculus structure. In: Computer Science Logic (CSL\u201994). Lecture Notes in Computer Science, vol. 933, pp. 61\u201375. Springer, New York (1995)","DOI":"10.1007\/BFb0022247"},{"key":"99_CR21","doi-asserted-by":"crossref","unstructured":"Hindley, J.R.: Basic simple type theory. Cambridge tracts in theoretical computer science, vol. 42. Cambridge University Press, Cambridge (1997)","DOI":"10.1017\/CBO9780511608865"},{"key":"99_CR22","doi-asserted-by":"crossref","unstructured":"Kripke, S.A.: The problem of entailment, (abstract). J. Symb. Log. 24, 324 (1959)","DOI":"10.2307\/2964568"},{"key":"99_CR23","first-page":"189","volume":"1","author":"R.K. Meyer","year":"1976","unstructured":"Meyer R.K.: A general Gentzen system for implicational calculi. Relev. Log. Newsl. 1, 189\u2013201 (1976)","journal-title":"Relev. Log. Newsl."},{"key":"99_CR24","doi-asserted-by":"crossref","unstructured":"Padovani, V.: Ticket entailment is decidable. Math. Struct. Comput. Sci. 23, 568\u2013607 (2013)","DOI":"10.1017\/S0960129512000412"},{"key":"99_CR25","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/S0003-4843(77)80004-1","volume":"12","author":"G. Pottinger","year":"1977","unstructured":"Pottinger G.: Normalization as a homomorphic image of cut-elimination. Ann. Math. Log. 12, 323\u2013357 (1977)","journal-title":"Ann. Math. Log."},{"key":"99_CR26","doi-asserted-by":"crossref","unstructured":"S\u00f8rensen, M.H., Urzyczyn, P.: Lectures on the Curry\u2013Howard Isomorphism. Studies in logic and the foundations of mathematics, vol. 149. Elsevier, Amsterdam (2006)","DOI":"10.1016\/S0049-237X(06)80005-4"},{"key":"99_CR27","unstructured":"Trigg, P., Hindley, J.R., Bunder, M.W.: Combinatory abstraction using B, B\u2019 and friends. Theor. Comput. Sci. 135, 405\u2013422 (1994)"},{"key":"99_CR28","doi-asserted-by":"crossref","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, 1059\u20131073 (1984)","journal-title":"J. Symb. Log."},{"key":"99_CR29","first-page":"66","volume":"5","author":"A. Urquhart","year":"2007","unstructured":"Urquhart A.: Four variables suffice. Australas. J. Log. 5, 66\u201373 (2007)","journal-title":"Australas. J. Log."}],"container-title":["Logica Universalis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11787-014-0099-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11787-014-0099-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11787-014-0099-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,8]],"date-time":"2019-08-08T13:29:52Z","timestamp":1565270992000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11787-014-0099-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,3,20]]},"references-count":29,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2014,6]]}},"alternative-id":["99"],"URL":"https:\/\/doi.org\/10.1007\/s11787-014-0099-z","relation":{},"ISSN":["1661-8297","1661-8300"],"issn-type":[{"value":"1661-8297","type":"print"},{"value":"1661-8300","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,3,20]]}}}