{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,7]],"date-time":"2025-07-07T10:05:04Z","timestamp":1751882704379},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540569923"},{"type":"electronic","value":"9783540478904"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-56992-8_4","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T07:00:43Z","timestamp":1330239643000},"page":"29-42","source":"Crossref","is-referenced-by-count":5,"title":["Algorithmic structuring of cut-free proofs"],"prefix":"10.1007","author":[{"given":"Matthias","family":"Baaz","sequence":"first","affiliation":[]},{"given":"Richard","family":"Zach","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"4_CR1","unstructured":"Baaz, M. [1993] Note on the existence of most general semi-unifiers. In Arithmetic, Proof Theory and Computational Complexity, P. Clote and J. Kraj\u00ed\u010dek, editors, pp. 19\u201328. Oxford University Press."},{"key":"4_CR2","unstructured":"Baaz, M. and P. Pudl\u00e1k. [1993] Kreisel's conjecture for L\u22031. In Arithmetic, Proof Theory and Computational Complexity, P. Clote and J. Kraj\u00ed\u010dek, editors, pp. 29\u201359. Oxford University Press."},{"key":"4_CR3","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1016\/0168-0072(91)90059-U","volume":"53","author":"S. R. Buss","year":"1991","unstructured":"Buss, S. R. [1991] The undecidability of k-provability. Ann. Pure Appl. Logic, 53, 75\u2013102.","journal-title":"Ann. Pure Appl. Logic"},{"key":"4_CR4","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1016\/0168-0072(91)90015-E","volume":"51","author":"W. M. Farmer","year":"1991","unstructured":"Farmer, W. M. [1991] A unification-theoretic method for investigating the k-provability problem. Ann. Pure Appl. Logic, 51, 173\u2013214.","journal-title":"Ann. Pure Appl. Logic"},{"key":"4_CR5","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1934","unstructured":"Gentzen, G. [1934] Untersuchungen \u00fcber das logische Schlie\u00dfen I\u2013II. Math. Z., 39, 176\u2013210, 405\u2013431.","journal-title":"Math. Z."},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Kfoury, A. J., J. Tiuryn, and P. Urzyczyn. [1990] The undecidability of the semi-unification problem. In Proc. 22nd ACM STOC, pp. 468\u2013476. journal version to appear in Inf. Comp.","DOI":"10.1145\/100216.100279"},{"key":"4_CR7","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/BF01625836","volume":"27","author":"J. Kraj\u00ed\u010dek","year":"1988","unstructured":"Kraj\u00ed\u010dek, J. and P. Pudl\u00e1k. [1988] The number of proof lines and the size of proofs in first order logic. Arch. Math. Logic, 27, 69\u201384.","journal-title":"Arch. Math. Logic"},{"key":"4_CR8","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1090\/S0002-9947-1973-0432416-X","volume":"177","author":"R. J. Parikh","year":"1973","unstructured":"Parikh, R. J. [1973] Some results on the length of proofs. Trans. Am. Math. Soc., 177, 29\u201336.","journal-title":"Trans. Am. Math. Soc."},{"issue":"3","key":"4_CR9","first-page":"551","volume":"29","author":"P. Pudl\u00e1k","year":"1988","unstructured":"Pudl\u00e1k, P. [1988] On a unification problem related to Kreisel's conjecture. Comm. Math. Univ. Carol., 29(3), 551\u2013556.","journal-title":"Comm. Math. Univ. Carol."},{"key":"4_CR10","unstructured":"Statman, R. [1974] Structural Complexity of Proofs. PhD thesis, Stanford University."},{"key":"4_CR11","doi-asserted-by":"crossref","first-page":"204","DOI":"10.1007\/BFb0079691","volume-title":"The Syntax and Semantics of Infinitary Languages","author":"W. W. Tait","year":"1968","unstructured":"Tait, W. W. [1968] Normal derivability in classical logic. In The Syntax and Semantics of Infinitary Languages, J. Barwise, editor, pp. 204\u2013236. Springer, Berlin."}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-56992-8_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T20:58:05Z","timestamp":1619557085000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-56992-8_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540569923","9783540478904"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-56992-8_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]}}}