{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:17:24Z","timestamp":1725484644110},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540425540"},{"type":"electronic","value":"9783540448020"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44802-0_33","type":"book-chapter","created":{"date-parts":[[2007,6,1]],"date-time":"2007-06-01T04:15:38Z","timestamp":1180671338000},"page":"469-483","source":"Crossref","is-referenced-by-count":0,"title":["On a Generalisation of Herbrand\u2019s Theorem"],"prefix":"10.1007","author":[{"given":"Matthias","family":"Baaz","sequence":"first","affiliation":[]},{"given":"Georg","family":"Moser","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,8,30]]},"reference":[{"key":"33_CR1","first-page":"21","volume-title":"Contributions to General Algebra 6","author":"M. Baaz","year":"1988","unstructured":"M. Baaz. \u00dcber den allgemeinen Gehalt von Beweisen. In Contributions to General Algebra 6, pages 21\u201329. H\u00f6lder-Pichler-Tempsky, Teubner, 1988."},{"issue":"4","key":"33_CR2","doi-asserted-by":"crossref","first-page":"353","DOI":"10.3233\/FI-1994-2044","volume":"20","author":"M. Baaz","year":"1994","unstructured":"M. Baaz and A. Leitsch. On skolemization and proof complexity. Fund. Informaticae, 20(4):353\u2013379, 1994.","journal-title":"Fund. Informaticae"},{"key":"33_CR3","doi-asserted-by":"crossref","unstructured":"M. Baaz and A. Leitsch. Cut normal forms and proof complexity. Annals of Pure and Applied Logic, pages 127\u2013177, 1997.","DOI":"10.1016\/S0168-0072(98)00026-8"},{"key":"33_CR4","unstructured":"M. Baaz and A. Leitsch. Cut elimination by resolution. J. Symbolic Computation, 1999."},{"key":"33_CR5","doi-asserted-by":"crossref","unstructured":"M. Baaz, A. Leitsch, and G. Moser. System Description: CutRes 0.1: Cut Elimination by Resolution. 1999.","DOI":"10.1007\/3-540-48660-7_16"},{"key":"33_CR6","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0168-0072(94)00054-7","volume":"75","author":"M. Baaz","year":"1995","unstructured":"M.Baaz and R. Zach. Generalizing theorems in real closed fields. Ann. of Pure and Applied Logics, 75:3\u201323, 1995.","journal-title":"Ann. of Pure and Applied Logics"},{"key":"33_CR7","unstructured":"R.S. Boyer and J.S. Moore. A Computational Logic Handbook. Academia Press, 1988."},{"key":"33_CR8","doi-asserted-by":"crossref","unstructured":"A. Bundy. The Automation of Proof By Mathematical Induction. Elsevier Science Publisher, 2001. To appear.","DOI":"10.1016\/B978-044450813-3\/50015-1"},{"key":"33_CR9","doi-asserted-by":"crossref","unstructured":"S. R. Buss. An introduction to proof theory. In S. R. Buss, editor, Handbook of Proof Theory, pages 1\u201379. Elsevier Science, 1998.","DOI":"10.1016\/S0049-237X(98)80016-5"},{"key":"33_CR10","doi-asserted-by":"crossref","unstructured":"W.M. Farmer. A unification-theoretic method for investigating the k-provability problem. ANAP, pages 173\u2013214, 1991.","DOI":"10.1016\/0168-0072(91)90015-E"},{"key":"33_CR11","doi-asserted-by":"crossref","unstructured":"H. Gericke. Mathematik in Antike und Orient. Springer Verlag, 1984.","DOI":"10.1007\/978-3-642-68630-6"},{"key":"33_CR12","doi-asserted-by":"crossref","unstructured":"D. Hilbert and P. Bernays. Grundlagen der Mathematik 2. Spinger Verlag, 1970.","DOI":"10.1007\/978-3-642-86896-2"},{"key":"33_CR13","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/BF01625836","volume":"27","author":"J. Kraj\u00ed\u0107ek","year":"1988","unstructured":"J. Kraj\u00ed\u0107ek and P. Pudl\u00e1k. 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":"33_CR14","doi-asserted-by":"crossref","unstructured":"A. Leitsch. The Resolution Calculus. EATCS-Texts in Theoretical Computer Science. Springer, 1997.","DOI":"10.1007\/978-3-642-60605-2"},{"key":"33_CR15","doi-asserted-by":"crossref","unstructured":"R.J. Parikh. Some results on the length of proofs. Trans. Amer. Math. Soc., pages 29\u201336, 1973.","DOI":"10.1090\/S0002-9947-1973-0432416-X"},{"key":"33_CR16","doi-asserted-by":"crossref","unstructured":"P. Pudlak. The lengths of proofs. In S. Buss editor, Handbook of Proof Theory, pages 547\u2013639. Elsevier, 1998.","DOI":"10.1016\/S0049-237X(98)80023-2"},{"issue":"2","key":"33_CR17","doi-asserted-by":"publisher","first-page":"235","DOI":"10.2307\/2272636","volume":"39","author":"D. Richardson","year":"1974","unstructured":"D. Richardson. Sets of theorems with short proofs. J. Symbolic Logic, 39(2):235\u2013242, 1974.","journal-title":"J. Symbolic Logic"},{"key":"33_CR18","unstructured":"H. Schwichtenberg. Some applications of cut-elimination, pages 867\u2013897. North Holland, 5th edition, 1989."},{"key":"33_CR19","unstructured":"J. H. Siekmann. Unification Theory, pages 1\u201368. Academic Press, 1990."},{"key":"33_CR20","volume-title":"Proof Theory","author":"G. Takeuti","year":"1980","unstructured":"G. Takeuti. Proof Theory. North-Holland, Amsterdam, 2nd edition, 1980.","edition":"2nd edition"},{"key":"33_CR21","first-page":"122","volume":"12","author":"C. Walther","year":"1994","unstructured":"C. Walther. Mathematical induction, volume 12, pages 122\u2013227. Oxford University Press, 1994.","journal-title":"Mathematical induction"},{"key":"33_CR22","unstructured":"C. Weidenbach. Sorted unification and tree automata. In Wolfgang Bibel and Peter H. Schmitt, editors, Automated Deduction-A Basis for Applications, volume 1 of Applied Logic, chapter 9, pages 291\u2013320. Kluwer, 1998."},{"key":"33_CR23","first-page":"195","volume":"6","author":"T. Yukami","year":"1984","unstructured":"T. Yukami. Some results on speed-up. Ann. Japan Assoc. Philos. Sci., 6:195\u2013205, 1984.","journal-title":"Ann. Japan Assoc. Philos. Sci."}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44802-0_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,22]],"date-time":"2020-04-22T16:24:35Z","timestamp":1587572675000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44802-0_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540425540","9783540448020"],"references-count":23,"URL":"http:\/\/dx.doi.org\/10.1007\/3-540-44802-0_33","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}
