{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,14]],"date-time":"2025-10-14T06:58:23Z","timestamp":1760425103122},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642283314"},{"type":"electronic","value":"9783642283321"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28332-1_26","type":"book-chapter","created":{"date-parts":[[2012,2,29]],"date-time":"2012-02-29T09:45:36Z","timestamp":1330508736000},"page":"301-312","source":"Crossref","is-referenced-by-count":13,"title":["Applying Tree Languages in Proof Theory"],"prefix":"10.1007","author":[{"given":"Stefan","family":"Hetzl","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"26_CR1","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1016\/S0168-0072(98)00026-8","volume":"97","author":"M. Baaz","year":"1999","unstructured":"Baaz, M., Leitsch, A.: Cut Normal Forms and Proof Complexity. Annals of Pure and Applied Logic\u00a097, 127\u2013177 (1999)","journal-title":"Annals of Pure and Applied Logic"},{"key":"26_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/3-540-60178-3_85","volume-title":"Logic and Computational Complexity","author":"S.R. Buss","year":"1995","unstructured":"Buss, S.R.: On Herbrand\u2019s Theorem. In: Leivant, D. (ed.) LCC 1994. LNCS, vol.\u00a0960, pp. 195\u2013209. Springer, Heidelberg (1995)"},{"key":"26_CR3","unstructured":"Comon, H., Dauchet, M., Gilleron, R., L\u00f6ding, C., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree Automata: Techniques and Applications (2007), \n                    \n                      http:\/\/www.grappa.univ-lille3.fr\/tata\n                    \n                    \n                   (release October 12, 2007)"},{"key":"26_CR4","doi-asserted-by":"crossref","unstructured":"Cook, S., Nguyen, P.: Logical Foundations of Proof Complexity. Perspectives in Logic. Cambridge University Press (2010)","DOI":"10.1017\/CBO9780511676277"},{"key":"26_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-540-74915-8_13","volume-title":"Computer Science Logic","author":"E. Filiot","year":"2007","unstructured":"Filiot, E., Talbot, J.-M., Tison, S.: Satisfiability of a Spatial Logic with Tree Variables. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol.\u00a04646, pp. 130\u2013145. Springer, Heidelberg (2007)"},{"key":"26_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/978-3-540-85780-8_25","volume-title":"Developments in Language Theory","author":"E. Filiot","year":"2008","unstructured":"Filiot, E., Talbot, J.-M., Tison, S.: Tree Automata with Global Constraints. In: Ito, M., Toyama, M. (eds.) DLT 2008. LNCS, vol.\u00a05257, pp. 314\u2013326. Springer, Heidelberg (2008)"},{"issue":"4","key":"26_CR7","doi-asserted-by":"publisher","first-page":"571","DOI":"10.1142\/S012905411000743X","volume":"21","author":"E. Filiot","year":"2010","unstructured":"Filiot, E., Talbot, J.M., Tison, S.: Tree Automata With Global Constraints. International Journal of Foundations of Computer Science\u00a021(4), 571\u2013596 (2010)","journal-title":"International Journal of Foundations of Computer Science"},{"key":"26_CR8","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1934","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische Schlie\u00dfen. Mathematische Zeitschrift\u00a039, 176\u2013210, 405\u2013431 (1934-1935)","journal-title":"Mathematische Zeitschrift"},{"key":"26_CR9","unstructured":"Herbrand, J.: Recherches sur la th\u00e9orie de la d\u00e9monstration. Ph.D. thesis, Universit\u00e9 de Paris (1930)"},{"key":"26_CR10","unstructured":"Hetzl, S.: Proofs as Tree Languages (preprint), \n                    \n                      http:\/\/hal.archives-ouvertes.fr\/hal-00613713\/"},{"issue":"5","key":"26_CR11","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1007\/s00153-010-0186-7","volume":"49","author":"S. Hetzl","year":"2010","unstructured":"Hetzl, S.: On the form of witness terms. Archive for Mathematical Logic\u00a049(5), 529\u2013554 (2010)","journal-title":"Archive for Mathematical Logic"},{"key":"26_CR12","unstructured":"Hetzl, S., Leitsch, A., Weller, D.: Towards Algorithmic Cut-Introduction (submitted)"},{"key":"26_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1007\/978-3-642-00982-2_38","volume-title":"Language and Automata Theory and Applications","author":"F. Jacquemard","year":"2009","unstructured":"Jacquemard, F., Klay, F., Vacher, C.: Rigid Tree Automata. In: Dediu, A.H., Ionescu, A.M., Mart\u00edn-Vide, C. (eds.) LATA 2009. LNCS, vol.\u00a05457, pp. 446\u2013457. Springer, Heidelberg (2009)"},{"key":"26_CR14","doi-asserted-by":"publisher","first-page":"486","DOI":"10.1016\/j.ic.2010.11.015","volume":"209","author":"F. Jacquemard","year":"2011","unstructured":"Jacquemard, F., Klay, F., Vacher, C.: Rigid tree automata and applications. Information and Computation\u00a0209, 486\u2013512 (2011)","journal-title":"Information and Computation"},{"key":"26_CR15","volume-title":"Applied Proof Theory: Proof Interpretations and their Use in Mathematics","author":"U. Kohlenbach","year":"2008","unstructured":"Kohlenbach, U.: Applied Proof Theory: Proof Interpretations and their Use in Mathematics. Springer, Heidelberg (2008)"},{"issue":"4","key":"26_CR16","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/BF00370646","volume":"46","author":"D. Miller","year":"1987","unstructured":"Miller, D.: A Compact Representation of Proofs. Studia Logica\u00a046(4), 347\u2013370 (1987)","journal-title":"Studia Logica"},{"key":"26_CR17","first-page":"137","volume":"88","author":"V.P. Orevkov","year":"1979","unstructured":"Orevkov, V.P.: Lower bounds for increasing complexity of derivations after cut elimination. Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta\u00a088, 137\u2013161 (1979)","journal-title":"Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta"},{"key":"26_CR18","doi-asserted-by":"crossref","unstructured":"Pudl\u00e1k, P.: The Lengths of Proofs. In: Buss, S. (ed.) Handbook of Proof Theory, pp. 547\u2013637. Elsevier (1998)","DOI":"10.1016\/S0049-237X(98)80023-2"},{"key":"26_CR19","unstructured":"Schwichtenberg, H., Troelstra, A.S.: Basic Proof Theory. Cambridge University Press (1996)"},{"key":"26_CR20","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1006\/jcss.1996.0046","volume":"53","author":"J. Shallit","year":"1996","unstructured":"Shallit, J., Breitbart, Y.: Automaticity I: Properties of a Measure of Descriptional Complexity. Journal of Computer and System Sciences\u00a053, 10\u201325 (1996)","journal-title":"Journal of Computer and System Sciences"},{"issue":"4","key":"26_CR21","first-page":"537","volume":"6","author":"J. Shallit","year":"2001","unstructured":"Shallit, J., Wang, M.W.: Automatic complexity of strings. Journal of Automata, Languages and Combinatorics\u00a06(4), 537\u2013554 (2001)","journal-title":"Journal of Automata, Languages and Combinatorics"},{"key":"26_CR22","unstructured":"Shoenfield, J.R.: Mathematical Logic, 2nd edn. AK Peters (2001)"},{"key":"26_CR23","first-page":"104","volume":"75","author":"R. Statman","year":"1979","unstructured":"Statman, R.: Lower bounds on Herbrand\u2019s theorem. Proceedings of the American Mathematical Society\u00a075, 104\u2013107 (1979)","journal-title":"Proceedings of the American Mathematical Society"}],"container-title":["Lecture Notes in Computer Science","Language and Automata Theory and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28332-1_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T04:29:24Z","timestamp":1556425764000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28332-1_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642283314","9783642283321"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28332-1_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}