{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,11]],"date-time":"2025-01-11T06:40:11Z","timestamp":1736577611949,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540371878"},{"type":"electronic","value":"9783540371885"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11814771_31","type":"book-chapter","created":{"date-parts":[[2006,10,5]],"date-time":"2006-10-05T15:44:21Z","timestamp":1160063061000},"page":"347-361","source":"Crossref","is-referenced-by-count":3,"title":["Strong Cut-Elimination Systems for Hudelmaier\u2019s Depth-Bounded Sequent Calculus for Implicational Logic"],"prefix":"10.1007","author":[{"given":"Roy","family":"Dyckhoff","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Delia","family":"Kesner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"St\u00e9phane","family":"Lengrand","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"31_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F. Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"key":"31_CR2","doi-asserted-by":"crossref","unstructured":"Dyckhoff, R., Kesner, D., Lengrand, S.: Strong cut-elimination systems for Hudelmaier\u2019s depth-bounded sequent calculus for implicational logic(2006), Full version available at http:\/\/www.pps.jussieu.fr\/~lengrand\/Work\/Papers.html","DOI":"10.1007\/11814771_31"},{"key":"31_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.\u00a03988, Springer, Heidelberg (2006)"},{"issue":"8","key":"31_CR4","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1145\/359138.359142","volume":"22","author":"N. Dershowitz","year":"1979","unstructured":"Dershowitz, N., Manna, Z.: Proving termination with multiset orderings. Communications of the ACM\u00a022(8), 465\u2013476 (1979)","journal-title":"Communications of the ACM"},{"issue":"4","key":"31_CR5","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. The Journal of Symbolic Logic\u00a065(4), 1499\u20131518 (2000)","journal-title":"The Journal of Symbolic Logic"},{"issue":"3","key":"31_CR6","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. The Journal of Symbolic Logic\u00a057(3), 795\u2013807 (1992)","journal-title":"The Journal of Symbolic Logic"},{"key":"31_CR7","unstructured":"Hudelmaier, J.: Bounds for Cut Elimination in Intuitionistic Logic. PhD thesis, Universit\u00e4t T\u00fcbingen (1989)"},{"key":"31_CR8","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/BF01627506","volume":"31","author":"J. Hudelmaier","year":"1992","unstructured":"Hudelmaier, J.: Bounds on cut-elimination in intuitionistic propositional logic. Archive for Mathematical Logic\u00a031, 331\u2013354 (1992)","journal-title":"Archive for Mathematical Logic"},{"key":"31_CR9","unstructured":"Kamin, S., L\u00e9vy, J.-J.: Attempts for generalizing the recursive path orderings. Handwritten paper, University of Illinois (1980)"},{"key":"31_CR10","doi-asserted-by":"crossref","unstructured":"Lincoln, P., Scedrov, A., Shankar, N.: Linearizing intuitionistic implication. In: Proc. of the Sixth Annual IEEE Symposium on Logic in Computer Science, Amsterdam, The Netherlands, pp. 51\u201362 (1991)","DOI":"10.1109\/LICS.1991.151630"},{"key":"31_CR11","unstructured":"Matthes, R.: Contraction-aware \u03bb-calculus, Seminar at Oberwolfach (2002)"},{"key":"31_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-08531-9","volume-title":"Computing in Systems Described by Equations","author":"M.J. O\u2019Donnell","year":"1977","unstructured":"O\u2019Donnell, M.J.: Computing in Systems Described by Equations. LNCS, vol.\u00a058. Springer, Heidelberg (1977)"},{"key":"31_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/11554554_19","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"J. Otten","year":"2005","unstructured":"Otten, J., Raths, T., Kreitz, C.: The ILTP Library. In: Beckert, B. (ed.) TABLEAUX 2005. LNCS (LNAI), vol.\u00a03702, pp. 333\u2013337. Springer, Heidelberg (2005)"},{"key":"31_CR14","doi-asserted-by":"publisher","first-page":"33","DOI":"10.2307\/2275175","volume":"57","author":"A.M. Pitts","year":"1992","unstructured":"Pitts, A.M.: On an interpretation of second order quantification in first-order intuitionistic propositional logic. Journal of Symbolic Logic\u00a057, 33\u201352 (1992)","journal-title":"Journal of Symbolic Logic"},{"key":"31_CR15","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/S0890-5401(03)00138-X","volume":"186","author":"A.M. Pitts","year":"2003","unstructured":"Pitts, A.M.: Nominal logic, a first order theory of names and binding. Information and Computation\u00a0186, 165\u2013193 (2003)","journal-title":"Information and Computation"},{"key":"31_CR16","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139168717","volume-title":"Basic Proof Theory","author":"A.S. Troelstra","year":"2000","unstructured":"Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory. Cambridge University Press, Cambridge (2000)"},{"key":"31_CR17","unstructured":"Vestergaard, R.: Revisiting Kreisel: A computational anomaly in the Troelstra-Schwichtenberg g3i system (March 1999), available at http:\/\/www.cee.hw.ac.uk\/homedirjrvest\/"},{"issue":"2","key":"31_CR18","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1090\/trans2\/094\/02","volume":"94","author":"N.N. Vorob\u2019ev","year":"1970","unstructured":"Vorob\u2019ev, N.N.: A new algorithm for derivability in the constructive propositional calculus. American Mathematical Society Translations\u00a094(2), 37\u201371 (1970)","journal-title":"American Mathematical Society Translations"},{"key":"31_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1007\/3-540-58140-5_35","volume-title":"Logical Foundations of Computer Science","author":"V. Oostrom van","year":"1994","unstructured":"van Oostrom, V., van Raamsdonk, F.: Weak orthogonality implies confluence: the higher-order case. In: Matiyasevich, Y.V., Nerode, A. (eds.) LFCS 1994. LNCS, vol.\u00a0813, pp. 379\u2013392. Springer, Heidelberg (1994)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11814771_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,11]],"date-time":"2025-01-11T06:08:39Z","timestamp":1736575719000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11814771_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540371878","9783540371885"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/11814771_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}