{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,2,19]],"date-time":"2023-02-19T03:24:06Z","timestamp":1676777046218},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2010,4,26]],"date-time":"2010-04-26T00:00:00Z","timestamp":1272240000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Arch. Math. Logic"],"published-print":{"date-parts":[[2010,6]]},"DOI":"10.1007\/s00153-010-0186-7","type":"journal-article","created":{"date-parts":[[2010,4,25]],"date-time":"2010-04-25T10:49:10Z","timestamp":1272192550000},"page":"529-554","source":"Crossref","is-referenced-by-count":4,"title":["On the form of witness terms"],"prefix":"10.1007","volume":"49","author":[{"given":"Stefan","family":"Hetzl","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2010,4,26]]},"reference":[{"key":"186_CR1","unstructured":"Baaz, M., Stefan, H.: On the non-confluence of cut-elimination. to appear"},{"key":"186_CR2","doi-asserted-by":"crossref","unstructured":"Baaz, M., Stefan, H., Leitsch, A., Richter, C., Spohr, H.: Cut-elimination: experiments with CERES. In: Baader, F. Voronkov, A. (eds.) Logic for programming, artificial intelligence, and reasoning (LPAR) 2004. Lecture Notes in Computer Science, vol. 3452, pp. 481\u2013495. Springer (2005)","DOI":"10.1007\/978-3-540-32275-7_32"},{"issue":"2\u20133","key":"186_CR3","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1016\/j.tcs.2008.02.043","volume":"403","author":"M. Baaz","year":"2008","unstructured":"Baaz M., Stefan H., Leitsch A., Richter C., Spohr H.: CERES: An analysis of F\u00fcrstenberg\u2019s proof of the infinity of primes. Theor. Comput. Sci. 403(2\u20133), 160\u2013175 (2008)","journal-title":"Theor. Comput. Sci."},{"issue":"4","key":"186_CR4","doi-asserted-by":"crossref","first-page":"353","DOI":"10.3233\/FI-1994-2044","volume":"20","author":"M. Baaz","year":"1994","unstructured":"Baaz M., Leitsch A.: On skolemization and proof Complexity. Fundamenta Informaticae 20(4), 353\u2013379 (1994)","journal-title":"Fundamenta Informaticae"},{"issue":"2","key":"186_CR5","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1006\/jsco.1999.0359","volume":"29","author":"M. Baaz","year":"2000","unstructured":"Baaz M., Leitsch A.: Cut-elimination and redundancy-elimination by resolution. J. Symb. Comput. 29(2), 149\u2013176 (2000)","journal-title":"J. Symb. Comput."},{"key":"186_CR6","first-page":"2","volume-title":"Handbook of proof theory pages","author":"S Buss","year":"1998","unstructured":"Buss S: An introduction to proof theory. In: Buss, S (eds) Handbook of proof theory pages, pp. 2\u201378. Elsevier, Amsterdam (1998)"},{"key":"186_CR7","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1016\/S0168-0072(98)00031-1","volume":"96","author":"A Carbone","year":"1999","unstructured":"Carbone A: Turning cycles into spirals. Ann. Pure Appl. Log. 96, 57\u201373 (1999)","journal-title":"Ann. Pure Appl. Log."},{"key":"186_CR8","doi-asserted-by":"crossref","first-page":"2049","DOI":"10.1090\/S0002-9947-99-02300-4","volume":"352","author":"A. Carbone","year":"2000","unstructured":"Carbone A.: Cycling in proofs and feasibility. Trans. Am. Math. Soc. 352, 2049\u20132075 (2000)","journal-title":"Trans. Am. Math. Soc."},{"key":"186_CR9","unstructured":"Comon, H., Dauchet, M., Gilleron, R., L\u00f6ding, C., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata: techniques and applications. Available on: http:\/\/www.grappa.univ-lille3.fr\/tata2007 . release October 12th 2007"},{"key":"186_CR10","doi-asserted-by":"crossref","unstructured":"Curien, P.-L., Herbelin, H.: The duality of computation. In: Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP \u201900), pp. 233\u2013243. ACM (2000)","DOI":"10.1145\/351240.351262"},{"issue":"3","key":"186_CR11","doi-asserted-by":"crossref","first-page":"755","DOI":"10.2307\/2275572","volume":"62","author":"V. Danos","year":"1997","unstructured":"Danos V., Joinet J.-B., Schellinx H.: A new deconstructive logic: linear logic. J. Symb. Log. 62(3), 755\u2013807 (1997)","journal-title":"J. Symb. Log."},{"key":"186_CR12","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-9307-8","volume-title":"Fermat\u2019s Last Theorem: A Genetic Introduction to Algebraic Number Theory","author":"H.M. Edwards","year":"1977","unstructured":"Edwards H.M.: Fermat\u2019s Last Theorem: A Genetic Introduction to Algebraic Number Theory. Springer, Berlin (1977)"},{"issue":"2","key":"186_CR13","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1016\/0304-3975(93)90011-H","volume":"110","author":"J. Gallier","year":"1993","unstructured":"Gallier J.: Constructive logics. Part I: a tutorial on proof systems and typed \u03bb-calculi. Theor. Comput. Sci. 110(2), 249\u2013339 (1993)","journal-title":"Theor. Comput. Sci."},{"key":"186_CR14","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-642-59126-6_1","volume-title":"Handbook of Formal Languages, vol 3.","author":"F. G\u00e9cseg","year":"1997","unstructured":"G\u00e9cseg F., Steinby M.: Tree languages. In: Rozenberg, G., Salomaa, A. (eds) Handbook of Formal Languages, vol 3., pp. 1\u201368. Springer, Berlin (1997)"},{"key":"186_CR15","doi-asserted-by":"crossref","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische Schlie\u00dfen. Mathematische Zeitschrift 39:176\u2013210, 405\u2013431, (1934\u20131935)","DOI":"10.1007\/BF01201353"},{"key":"186_CR16","doi-asserted-by":"crossref","first-page":"493","DOI":"10.1007\/BF01565428","volume":"112","author":"G. Gentzen","year":"1936","unstructured":"Gentzen G.: Die Widerspruchsfreiheit der reinen Zahlentheorie. Mathematische Annalen 112, 493\u2013565 (1936)","journal-title":"Mathematische Annalen"},{"key":"186_CR17","doi-asserted-by":"crossref","unstructured":"Gerhardy, P.: Refined Complexity Analysis of Cut Elimination. In: Baaz, M., Makowsky, J. (eds), Computer Science Logic (CSL) 2003, vol. 2803 of Lecture Notes in Computer Science, pp. 212\u2013225. Springer (2003)","DOI":"10.1007\/978-3-540-45220-1_19"},{"key":"186_CR18","doi-asserted-by":"crossref","unstructured":"Gerhardy, P.: The role of quantifier alternations in cut elimination. Notre Dame J. Formal Log. 46(2), 165\u2013171 (2005)","DOI":"10.1305\/ndjfl\/1117755147"},{"key":"186_CR19","volume-title":"Proof Theory and Logical Complexity","author":"J.-Y. Girard","year":"1987","unstructured":"Girard J.-Y.: Proof Theory and Logical Complexity. Elsevier, Amsterdam (1987)"},{"key":"186_CR20","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1111\/j.1746-8361.1958.tb01464.x","volume":"12","author":"G. Kurt","year":"1958","unstructured":"Kurt G.: \u00dcber eine noch nicht ben\u00fctzte Erweiterung des finiten Standpunktes. Dialectica 12, 280\u2013287 (1958)","journal-title":"Dialectica"},{"key":"186_CR21","unstructured":"Heijltjes, W.: Proof Forests with Cut-Elimination Based on Herbrand\u2019s Theorem. In: Classical Logic and Computation (CL&C) 2008, participant\u2019s proceedings. available at http:\/\/www.homes.doc.ic.ac.uk\/svb\/CLaC08\/programme.html"},{"issue":"1\u20132","key":"186_CR22","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1016\/j.apal.2008.10.010","volume":"159","author":"S. Hetzl","year":"2009","unstructured":"Hetzl S.: Describing proofs by short tautologies. Ann. Pure Appl. Log. 159(1\u20132), 129\u2013145 (2009)","journal-title":"Ann. Pure Appl. Log."},{"key":"186_CR23","volume-title":"Grundlagen der Mathematik II","author":"D. Hilbert","year":"1939","unstructured":"Hilbert D., Bernays P.: Grundlagen der Mathematik II. Springer, Berlin (1939)"},{"key":"186_CR24","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, Berlin (2008)"},{"key":"186_CR25","doi-asserted-by":"crossref","unstructured":"Kreisel, G.: Finiteness theorems in arithmetic: An Application of Herbrand\u2019s Theorem for \u03a32-Formulas. In: Stern, J. (eds.), Logic Colloquium 1981, pp. 39\u201355. Elsevier, Amsterdam (1982)","DOI":"10.1016\/S0049-237X(08)71876-7"},{"issue":"1","key":"186_CR26","doi-asserted-by":"crossref","first-page":"234","DOI":"10.2307\/2275028","volume":"54","author":"H. Luckhardt","year":"1989","unstructured":"Luckhardt H.: Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken. J. Symb. Log. 54(1), 234\u2013263 (1989)","journal-title":"J. Symb. Log."},{"key":"186_CR27","unstructured":"McKinley, R.: Herbrand expansion proofs and proof identity. In: Classical Logic and Computation (CL&C) 2008, participant\u2019s proceedings. available at http:\/\/www.homes.doc.ic.ac.uk\/svb\/CLaC08\/programme.html"},{"issue":"4","key":"186_CR28","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1007\/BF00370646","volume":"46","author":"D. Miller","year":"1987","unstructured":"Miller D.: A compact representation of proofs. Studia Logica 46(4), 347\u2013370 (1987)","journal-title":"Studia Logica"},{"key":"186_CR29","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 88, 137\u2013161 (1979)","journal-title":"Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta"},{"key":"186_CR30","volume-title":"Natural Deduction: A Proof-Theoretical Study","author":"D. Prawitz","year":"1965","unstructured":"Prawitz D.: Natural Deduction: A Proof-Theoretical Study. Almqvist and Wicksell, Stockholm (1965)"},{"key":"186_CR31","doi-asserted-by":"crossref","first-page":"547","DOI":"10.1016\/S0049-237X(98)80023-2","volume-title":"Handbook of Proof Theory","author":"P. Pudl\u00e1k","year":"1998","unstructured":"Pudl\u00e1k P. : The Lengths of Proofs. In: Buss, S. (eds) Handbook of Proof Theory, pp. 547\u2013637. Elsevier, Amsterdam (1998)"},{"key":"186_CR32","doi-asserted-by":"crossref","unstructured":"Ratiu, D., Trifonov, T.: Exploring the computational content of the infinite pigeonhole principle. J. Log. Comput. (to appear)","DOI":"10.1093\/logcom\/exq011"},{"key":"186_CR33","doi-asserted-by":"crossref","first-page":"867","DOI":"10.1016\/S0049-237X(08)71124-8","volume-title":"Handbook of Mathematical Logic","author":"H. Schwichtenberg","year":"1977","unstructured":"Schwichtenberg H.: Proof Theory: Some Applications of Cut-Elimination. In: Barwise, J. (eds) Handbook of Mathematical Logic, pp. 867\u2013895. Elsevier, Amsterdam (1977)"},{"key":"186_CR34","first-page":"104","volume":"75","author":"R. Statman","year":"1979","unstructured":"Statman R.: Lower bounds on Herbrand\u2019s theorem. Proc. Am. Math. Soc. 75, 104\u2013107 (1979)","journal-title":"Proc. Am. Math. Soc."},{"key":"186_CR35","doi-asserted-by":"crossref","unstructured":"Tait, W.W.: Normal derivability in classical logic. In: Barwise, J. (ed.) The Syntax and Semantics of Infinitary Languages, vol. 72 of Lecture Notes in Mathematics, pp. 204\u2013236. Springer (1968)","DOI":"10.1007\/BFb0079691"},{"key":"186_CR36","unstructured":"Takeuti, G.: Proof Theory, 2nd edn. Elsevier, Amsterdam, March 1987"},{"key":"186_CR37","unstructured":"Urban, C.: Classical Logic and Computation. PhD thesis, University of Cambridge, October 2000"},{"key":"186_CR38","first-page":"123","volume":"45","author":"C. Urban","year":"2000","unstructured":"Urban C., Bierman G.: Strong Normalization of Cut-Elimination in Classical Logic. Fundamenta Informaticae 45, 123\u2013155 (2000)","journal-title":"Fundamenta Informaticae"},{"key":"186_CR39","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1016\/0304-3975(91)90086-H","volume":"91","author":"W. Zhang","year":"1991","unstructured":"Zhang W.: Cut elimination and automatic proof procedures. Theor. Comput. Sci. 91, 265\u2013284 (1991)","journal-title":"Theor. Comput. Sci."},{"key":"186_CR40","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1016\/0304-3975(94)90087-6","volume":"129","author":"W. Zhang","year":"1994","unstructured":"Zhang W.: Depth of proofs, depth of cut-formulas and complexity of cut formulas. Theor. Comput. Sci. 129, 193\u2013206 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"186_CR41","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0003-4843(74)90010-2","volume":"7","author":"J. Zucker","year":"1974","unstructured":"Zucker J.: The correspondence between cut-elimination and normalization. Ann. Math. Log. 7, 1\u2013112 (1974)","journal-title":"Ann. Math. Log."}],"container-title":["Archive for Mathematical Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00153-010-0186-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00153-010-0186-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00153-010-0186-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,4]],"date-time":"2020-06-04T00:56:49Z","timestamp":1591232209000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00153-010-0186-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,4,26]]},"references-count":41,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2010,6]]}},"alternative-id":["186"],"URL":"https:\/\/doi.org\/10.1007\/s00153-010-0186-7","relation":{},"ISSN":["0933-5846","1432-0665"],"issn-type":[{"value":"0933-5846","type":"print"},{"value":"1432-0665","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,4,26]]}}}