{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:49:23Z","timestamp":1740098963215,"version":"3.37.3"},"publisher-location":"Cham","reference-count":9,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319720555"},{"type":"electronic","value":"9783319720562"}],"license":[{"start":{"date-parts":[[2017,11,28]],"date-time":"2017-11-28T00:00:00Z","timestamp":1511827200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-72056-2_4","type":"book-chapter","created":{"date-parts":[[2017,11,27]],"date-time":"2017-11-27T09:33:31Z","timestamp":1511775211000},"page":"55-71","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["A Sequent-Calculus Based Formulation of the Extended First Epsilon Theorem"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7815-2501","authenticated-orcid":false,"given":"Matthias","family":"Baaz","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7084-7878","authenticated-orcid":false,"given":"Alexander","family":"Leitsch","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4753-7302","authenticated-orcid":false,"given":"Anela","family":"Lolic","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,11,28]]},"reference":[{"unstructured":"Aguilera, J.P., Baaz, M.: Unsound inferences make proofs shorter. CoRR, abs\/1608.07703 (2016)","key":"4_CR1"},{"key":"4_CR2","series-title":"Symbolic Computation (Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1007\/978-3-642-81955-1_29","volume-title":"Automation of Reasoning","author":"PB Andrews","year":"1971","unstructured":"Andrews, P.B.: Resolution in type theory. In: Siekmann, J.H., Wrightson, G. (eds.) Automation of Reasoning. Symbolic Computation (Artificial Intelligence), pp. 487\u2013507. Springer, Heidelberg (1971). https:\/\/doi.org\/10.1007\/978-3-642-81955-1_29"},{"issue":"2","key":"4_CR3","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"PB Andrews","year":"1981","unstructured":"Andrews, P.B.: Theorem proving via general matings. J. ACM (JACM) 28(2), 193\u2013214 (1981)","journal-title":"J. ACM (JACM)"},{"issue":"2","key":"4_CR4","doi-asserted-by":"crossref","first-page":"669","DOI":"10.2178\/jsl\/1333566645","volume":"77","author":"M Baaz","year":"2012","unstructured":"Baaz, M., Hetzl, S., Weller, D.: On the complexity of proof deskolemization. J. Symbolic Logic 77(2), 669\u2013686 (2012)","journal-title":"J. Symbolic Logic"},{"issue":"4","key":"4_CR5","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":"1\u20133","key":"4_CR6","doi-asserted-by":"crossref","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. Ann. Pure Appl. Logic 97(1\u20133), 127\u2013177 (1999)","journal-title":"Ann. Pure Appl. Logic"},{"unstructured":"Hilbert, D., Bernays, P.: Grundlagen der Mathematik II (1939)","key":"4_CR7"},{"key":"4_CR8","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. Symbolic Logic 54, 234\u2013263 (1989)","journal-title":"J. Symbolic Logic"},{"issue":"1","key":"4_CR9","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/s11225-006-6610-7","volume":"82","author":"G Moser","year":"2006","unstructured":"Moser, G., Zach, R.: The epsilon calculus and Herbrand complexity. Stud. Logica. 82(1), 133\u2013155 (2006)","journal-title":"Stud. Logica."}],"container-title":["Lecture Notes in Computer Science","Logical Foundations of Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-72056-2_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,22]],"date-time":"2020-10-22T21:35:21Z","timestamp":1603402521000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-72056-2_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,11,28]]},"ISBN":["9783319720555","9783319720562"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-72056-2_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017,11,28]]}}}