{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T17:16:50Z","timestamp":1694625410489},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2005,12,28]],"date-time":"2005-12-28T00:00:00Z","timestamp":1135728000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2005,12,28]],"date-time":"2005-12-28T00:00:00Z","timestamp":1135728000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Arch. Math. Logic"],"published-print":{"date-parts":[[2006,5]]},"DOI":"10.1007\/s00153-005-0327-6","type":"journal-article","created":{"date-parts":[[2005,12,26]],"date-time":"2005-12-26T14:36:29Z","timestamp":1135607789000},"page":"447-503","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Herbrand's theorem and term induction"],"prefix":"10.1007","volume":"45","author":[{"given":"Matthias","family":"Baaz","sequence":"first","affiliation":[]},{"given":"Georg","family":"Moser","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,12,28]]},"reference":[{"key":"327_CR1","doi-asserted-by":"crossref","unstructured":"Baader, F., Snyder, W.: Unification Theory. Vol. I. Elsevier Science Publisher, 2001, pp. 445\u2013532","DOI":"10.1016\/B978-044450813-3\/50010-2"},{"key":"327_CR2","unstructured":"Baaz, M.: \u00dcber den allgemeinen Gehalt von Beweisen. In: Contributions to General Algebra 6, H\u00f6lder-Pichler-Tempsky, Teubner, 1988, pp. 21\u201329"},{"key":"327_CR3","doi-asserted-by":"crossref","unstructured":"Baaz, M., Ferm\u00fcller, C.: A Note on the Proof-Theoretic Strength of a Single Application of the Schema of Identity. In: Proof Theory in Computer Science, International Seminar, PTCS 2001, Dagstuhl Castle, Germany, October 7\u201312, 2001, Proceedings, Springer Verlag, 2001, pp. 38\u201348","DOI":"10.1007\/3-540-45504-3_3"},{"key":"327_CR4","doi-asserted-by":"crossref","first-page":"353","DOI":"10.3233\/FI-1994-2044","volume":"20","author":"Baaz","year":"4","unstructured":"Baaz, M., Leitsch, A.: On Skolemization and Proof Complexity. Fund. Informaticae 20 (4), 353\u2013379 (1994)","journal-title":"Fund. Informaticae"},{"key":"327_CR5","unstructured":"Baaz, M., Leitsch, A.: Cut Elimination by Resolution. J. Symb. Comp. (1999)"},{"key":"327_CR6","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1016\/S0168-0072(98)00026-8","volume":"97","author":"Baaz","year":"1999","unstructured":"Baaz, M., Leitsch, A.: Cut Normal Forms and Proof Complexity. Ann. Pure Appl. Logic 97, 127\u2013177 (1999)","journal-title":"Ann. Pure Appl. Logic"},{"key":"327_CR7","doi-asserted-by":"crossref","unstructured":"Baaz, M., Leitsch, A., Moser, G.: System Description: CutRes 0.1: Cut Elimination by Resolution. In: Proc. of CADE'99, 1999, pp. 212\u2013216","DOI":"10.1007\/3-540-48660-7_16"},{"key":"327_CR8","unstructured":"Baaz, M., Pudl\u00e1k, P.: Kreisel's conjecture for L\u22031. In: P. Clote and J. Kraj\u00ed\u0107ek (eds), Arithmetic, Proof Theory and Computational Complexity, Oxford University, 1993, pp. 29\u201359. With a postscript by G. Kreisel"},{"key":"327_CR9","unstructured":"Baaz, M., Wojtylak, P.: Generalizing Proofs in Monadic Languages. With a postscript by G. Kreisel, submitted to Ann. Pure Appl. Logic, 2001"},{"key":"327_CR10","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0168-0072(94)00054-7","volume":"75","author":"Baaz","year":"1995","unstructured":"Baaz, M., Zach, R.: Generalizing Theorems in Real Closed Fields. Ann. Pure Appl. Logic 75, 3\u201323 (1995)","journal-title":"Ann. Pure Appl. Logic"},{"key":"327_CR11","doi-asserted-by":"crossref","unstructured":"Boerger, E., Graedel, E., Gurevich, Y.: The Classical Decision Problem. Springer-Verlag, 1997","DOI":"10.1007\/978-3-642-59207-2"},{"key":"327_CR12","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic Handbook. Academia Press, 1988"},{"key":"327_CR13","doi-asserted-by":"crossref","unstructured":"Bundy, A.: The Automation of Proof by Mathematical Induction. In: A. Robinson and A. Voronkov, (eds), Handbook of Automated Reasoning, Vol. I, chapter 13, Elsevier Science, 2001, pp. 845\u2013911","DOI":"10.1016\/B978-044450813-3\/50015-1"},{"key":"327_CR14","doi-asserted-by":"crossref","unstructured":"Buss, S.R.: An Introduction to Proof Theory. In: S.R. Buss, (ed), Handbook of Proof Theory, Elsevier Science, 1998, pp. 1\u201379","DOI":"10.1016\/S0049-237X(98)80016-5"},{"key":"327_CR15","unstructured":"Farmer, W.M.: Length of Proofs and Unification Theory. PhD thesis, University of Wisconsin-Madison, Madison, Wisconsin, 1984"},{"key":"327_CR16","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"Gentzen","year":"1934","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische Schlie\u00df en I\u2013II. Mathematische Zeitschrift, 39, 176\u2013210, 405\u2013431 (1934)","journal-title":"Mathematische Zeitschrift,"},{"key":"327_CR17","unstructured":"Gentzen, G.: Neue Fassung des Widerspruchsfreiheitsbeweises f\u00fcr die reine Zahlentheorie. Forschungen zur Logik und zur Grundlegung der exakten Wissenschaften, 4, 1938"},{"key":"327_CR18","doi-asserted-by":"crossref","unstructured":"Gericke, H.: Mathematik in Antike und Orient. Springer Verlag, 1984","DOI":"10.1007\/978-3-642-68630-6"},{"key":"327_CR19","doi-asserted-by":"crossref","unstructured":"Herbrand, J.: Jacques Herbrand: Logical Writings. D. Reidel Publishing Company, Holland, 1971","DOI":"10.1007\/978-94-010-3072-4"},{"key":"327_CR20","doi-asserted-by":"crossref","unstructured":"Hilbert, D., Bernays, P.: Grundlagen der Mathematik 2. Spinger Verlag, 1970","DOI":"10.1007\/978-3-642-86896-2"},{"key":"327_CR21","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/BF01625836","volume":"27","author":"Kraj\u00ed\u0107ek","year":"1988","unstructured":"Kraj\u00ed\u0107ek, J., Pudl\u00e1k, P.: The Number of Proof Lines and the Size of Proofs in First-Order Logic. Arch. Math. Logic 27, 69\u201384 (1988)","journal-title":"Arch. Math. Logic"},{"key":"327_CR22","unstructured":"Kr\u00f6ger, F.: Temporal Logics of Programs. Springer Verlag, 1985"},{"key":"327_CR23","unstructured":"Moser, G.: Term Induction. PhD thesis, Vienna University of Technology, June 2001"},{"key":"327_CR24","doi-asserted-by":"crossref","unstructured":"Parikh, R.J.: Some Results on the Length of Proofs. Trans. Amer. Math. Soc. 1973, pp. 29\u201336","DOI":"10.1090\/S0002-9947-1973-0432416-X"},{"key":"327_CR25","doi-asserted-by":"crossref","unstructured":"Pudlak, P.: The Lengths of Proofs. In: S. Buss, (ed), Handbook of Proof Theory, Elsevier, 1998, pp. 547\u2013639","DOI":"10.1016\/S0049-237X(98)80023-2"},{"key":"327_CR26","doi-asserted-by":"publisher","first-page":"235","DOI":"10.2307\/2272636","volume":"39","author":"Richardson","year":"2","unstructured":"Richardson, D.: Sets of theorems with short proofs. J. Symb. Logic 39 (2), 235\u2013242 (1974)","journal-title":"J. Symb. Logic"},{"key":"327_CR27","doi-asserted-by":"crossref","unstructured":"Sch\u00fctte, K.: Proof Theory. Springer, Berlin and New York, 1977","DOI":"10.1007\/978-3-642-66473-1"},{"key":"327_CR28","unstructured":"Takeuti, G.: Proof Theory. North-Holland, Amsterdam, 2nd edition, 1987"},{"key":"327_CR29","unstructured":"Walther, C.: Mathematical Induction, Vol. 12, Oxford University Press, 1994, pp. 122\u2013227"},{"key":"327_CR30","first-page":"195","volume":"6","author":"Yukami","year":"1984","unstructured":"Yukami, T.: Some Results on Speed-up. Ann. Japan Assoc. Philos. Sci. 6, 195\u2013205 (1984)","journal-title":"Ann. Japan Assoc. Philos. Sci."}],"container-title":["Archive for Mathematical Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00153-005-0327-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00153-005-0327-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00153-005-0327-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00153-005-0327-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,14]],"date-time":"2022-05-14T01:05:53Z","timestamp":1652490353000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00153-005-0327-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,12,28]]},"references-count":30,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2006,5]]}},"alternative-id":["327"],"URL":"https:\/\/doi.org\/10.1007\/s00153-005-0327-6","relation":{},"ISSN":["0933-5846","1432-0665"],"issn-type":[{"value":"0933-5846","type":"print"},{"value":"1432-0665","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,12,28]]},"assertion":[{"value":"7 September 2001","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"28 December 2005","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}