{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,11]],"date-time":"2026-11-11T06:34:18Z","timestamp":1794378858554,"version":"4.9.0"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642142024","type":"print"},{"value":"9783642142031","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14203-1_36","type":"book-chapter","created":{"date-parts":[[2010,7,12]],"date-time":"2010-07-12T09:10:58Z","timestamp":1278925858000},"page":"427-433","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["System Description: The Proof Transformation System CERES"],"prefix":"10.1007","author":[{"given":"Tsvetan","family":"Dunchev","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alexander","family":"Leitsch","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tomer","family":"Libal","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Daniel","family":"Weller","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bruno","family":"Woltzenlogel Paleo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2010,7,13]]},"reference":[{"key":"36_CR1","doi-asserted-by":"publisher","first-page":"414","DOI":"10.2307\/2269949","volume":"36","author":"P.B. Andrews","year":"1971","unstructured":"Andrews, P.B.: Resolution in Type Theory. J. of Symbolic Logic\u00a036, 414\u2013432 (1971)","journal-title":"J. of Symbolic Logic"},{"key":"36_CR2","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":"36_CR3","unstructured":"Baaz, M., Hetzl, S., Leitsch, A., Richter, C., Spohr, H.: System Description: The Cut-Elimination System CERES. In: Proc. ESCoR 2006, pp. 159\u2013167 (2006)"},{"key":"36_CR4","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1016\/j.tcs.2008.02.043","volume":"403","author":"M. Baaz","year":"2008","unstructured":"Baaz, M., Hetzl, S., Leitsch, A., Richter, C., Spohr, H.: CERES: An analysis of F\u00fcrstenberg\u2019s proof of the infinity of primes. Th. Co. Sci.\u00a0403, 160\u2013175 (2008)","journal-title":"Th. Co. Sci."},{"key":"36_CR5","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, 149\u2013176 (2000)","journal-title":"Journal of Symbolic Computation"},{"key":"36_CR6","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1016\/j.jsc.2003.10.005","volume":"41","author":"M. Baaz","year":"2006","unstructured":"Baaz, M., Leitsch, A.: Towards a Clausal Analysis of Cut-Elimination. Journal of Symbolic Computation\u00a041, 381\u2013410 (2006)","journal-title":"Journal of Symbolic Computation"},{"key":"36_CR7","unstructured":"Dunchev, T.: Simplification of Herbrand Sequents. Master Thesis (2009)"},{"key":"36_CR8","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1934","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische Schliessen. Mathematische Zeitschrift\u00a039, 176\u2013210, 405\u2013431 (1934-1935)","journal-title":"Mathematische Zeitschrift"},{"key":"36_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/978-3-540-85110-3_38","volume-title":"Intelligent Computer Mathematics","author":"S. Hetzl","year":"2008","unstructured":"Hetzl, S., Leitsch, A., Weller, D., Woltzenlogel Paleo, B.: Herbrand sequent extraction. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.) AISC 2008, Calculemus 2008, and MKM 2008. LNCS (LNAI), vol.\u00a05144, pp. 462\u2013477. Springer, Heidelberg (2008)"},{"key":"36_CR10","doi-asserted-by":"crossref","unstructured":"Hetzl, S., Leitsch, A., Weller, D., Woltzenlogel Paleo, B.: A Clausal Approach to Proof Analysis in Second-Order Logic. In: Logical Foundations of Computer Sci. (2009)","DOI":"10.1007\/978-3-540-92687-0_15"},{"key":"36_CR11","unstructured":"Woltzenlogel Paleo, B.: Herbrand Sequent Extraction. VDM-Verlag (2008)"},{"key":"36_CR12","unstructured":"Woltzenlogel Paleo, B.: A General Analysis of Cut-Elimination by CERes. PhD Thesis (2009)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14203-1_36","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,25]],"date-time":"2021-10-25T22:12:47Z","timestamp":1635199967000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-642-14203-1_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642142024","9783642142031"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14203-1_36","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-642-14203-1","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]},"assertion":[{"value":"13 July 2010","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}