{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,20]],"date-time":"2025-09-20T22:12:04Z","timestamp":1758406324899},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540851097"},{"type":"electronic","value":"9783540851103"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-85110-3_38","type":"book-chapter","created":{"date-parts":[[2008,7,26]],"date-time":"2008-07-26T06:00:32Z","timestamp":1217052032000},"page":"462-477","source":"Crossref","is-referenced-by-count":16,"title":["Herbrand Sequent Extraction"],"prefix":"10.1007","author":[{"given":"Stefan","family":"Hetzl","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Leitsch","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Weller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bruno","family":"Woltzenlogel Paleo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"38_CR1","doi-asserted-by":"crossref","unstructured":"Baaz, M., Hetzl, S., Leitsch, A., Richter, C., Spohr, H.: Ceres: An Analysis of F\u00fcrstenberg\u2019s Proof of the Infinity of Primes. Theoretical Computer Science (to appear)","DOI":"10.1016\/j.tcs.2008.02.043"},{"key":"38_CR2","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"481","DOI":"10.1007\/978-3-540-32275-7_32","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M. Baaz","year":"2005","unstructured":"Baaz, M., Hetzl, S., Leitsch, A., Richter, C., Spohr, H.: Cut-Elimination: Experiments with CERES. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol.\u00a03452, pp. 481\u2013495. Springer, Heidelberg (2005)"},{"key":"38_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/11812289_8","volume-title":"Mathematical Knowledge Management","author":"M. Baaz","year":"2006","unstructured":"Baaz, M., Hetzl, S., Leitsch, A., Richter, C., Spohr, H.: Proof Transformation by CERES. In: Borwein, J.M., Farmer, W.M. (eds.) MKM 2006. LNCS (LNAI), vol.\u00a04108, pp. 82\u201393. Springer, Heidelberg (2006)"},{"key":"38_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 Matematicae\u00a020, 353\u2013379 (1994)","journal-title":"Fundamenta Matematicae"},{"key":"38_CR5","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"},{"issue":"2","key":"38_CR6","doi-asserted-by":"publisher","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. Journal of Symbolic Computation\u00a029(2), 149\u2013176 (2000)","journal-title":"Journal of Symbolic Computation"},{"key":"38_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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, p. 195. Springer, Heidelberg (1995)"},{"key":"38_CR8","first-page":"68","volume-title":"The Collected Papers of Gerhard Gentzen","author":"G. Gentzen","year":"1969","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische Schlie\u00dfen. In: Szabo, M.E. (ed.) The Collected Papers of Gerhard Gentzen, pp. 68\u2013131. North-Holland Publishing Company, Amsterdam (1969)"},{"key":"38_CR9","doi-asserted-by":"crossref","unstructured":"Gerhardy, P., Kohlenbach, U.: Extracting herbrand disjunctions by functional interpretation. Archive for Mathematical Logic\u00a044(5) (2005)","DOI":"10.1007\/s00153-005-0275-1"},{"key":"38_CR10","unstructured":"Herbrand, J.: Recherches sur la th\u00e9orie de la d\u00e9monstration. Travaux de la Societ\u00e9 des Sciences et des Lettres de Varsovie, Class III, Sciences Math\u00e9matiques et Physiques\u00a033 (1930)"},{"key":"38_CR11","unstructured":"Hetzl, S.: Characteristic Clause Sets and Proof Transformations. PhD thesis, Vienna University of Technology (2007)"},{"key":"38_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-540-75939-3_13","volume-title":"Algebraic and Proof-theoretic Aspects of Non-classical Logics","author":"S. Hetzl","year":"2007","unstructured":"Hetzl, S., Leitsch, A.: Proof transformations and structural invariance. In: Aguzzoli, S., Ciabattoni, A., Gerla, B., Manara, C., Marra, V. (eds.) ManyVal 2006. LNCS (LNAI), vol.\u00a04460, pp. 201\u2013230. Springer, Heidelberg (2007)"},{"key":"38_CR13","doi-asserted-by":"publisher","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. Journal of Symbolic Logic\u00a054, 234\u2013263 (1989)","journal-title":"Journal of Symbolic Logic"},{"key":"38_CR14","doi-asserted-by":"publisher","first-page":"104","DOI":"10.2307\/2042682","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"},{"issue":"1","key":"38_CR15","first-page":"35","volume":"19","author":"G. Sutcliffe","year":"2006","unstructured":"Sutcliffe, G., Suttner, C.: The State of CASC. AI Communications\u00a019(1), 35\u201348 (2006)","journal-title":"AI Communications"},{"key":"38_CR16","unstructured":"Paleo, B.W.: Herbrand sequent extraction. Master\u2019s thesis, Technische Universitaet Dresden; Technische Universitaet Wien, Dresden, Germany, Wien, Austria (2007)"},{"key":"38_CR17","series-title":"VDM-Verlag","volume-title":"Herbrand Sequent Extraction","author":"B.W. Paleo","year":"2008","unstructured":"Paleo, B.W.: Herbrand Sequent Extraction. VDM-Verlag. Saarbruecken, Germany (2008)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-85110-3_38.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:22:04Z","timestamp":1606184524000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-85110-3_38"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540851097","9783540851103"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-85110-3_38","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}