{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T17:33:05Z","timestamp":1725471185513},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540371045"},{"type":"electronic","value":"9783540371069"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11812289_8","type":"book-chapter","created":{"date-parts":[[2006,9,29]],"date-time":"2006-09-29T08:23:44Z","timestamp":1159518224000},"page":"82-93","source":"Crossref","is-referenced-by-count":6,"title":["Proof Transformation by CERES"],"prefix":"10.1007","author":[{"given":"Matthias","family":"Baaz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Hetzl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Leitsch","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Clemens","family":"Richter","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hendrik","family":"Spohr","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-22343-7","volume-title":"Proofs from THE BOOK","author":"M. Aigner","year":"1998","unstructured":"Aigner, M., Ziegler, G.M.: Proofs from THE BOOK. Springer, Heidelberg (1998)"},{"key":"8_CR2","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. Journal of Symbolic Logic\u00a036, 414\u2013432 (1971)","journal-title":"Journal of Symbolic Logic"},{"key":"8_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/978-3-540-32275-7_32","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"A. Leitsch","year":"2005","unstructured":"Leitsch, A., Baaz, M., Hetzl, S., 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)"},{"issue":"4","key":"8_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 Informaticae\u00a020(4), 353\u2013379 (1994)","journal-title":"Fundamenta Informaticae"},{"key":"8_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"},{"key":"8_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, 149\u2013176 (2000)","journal-title":"Journal of Symbolic Computation"},{"key":"8_CR7","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":"8_CR8","doi-asserted-by":"crossref","unstructured":"Eder, E.: Relative complexities of first-order calculi. Vieweg (1992)","DOI":"10.1007\/978-3-322-84222-0"},{"key":"8_CR9","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/BF01201363","volume":"39","author":"G. Gentzen","year":"1935","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische Schlie\u00dfen. Mathematische Zeitschrift\u00a039, 405\u2013431 (1935)","journal-title":"Mathematische Zeitschrift"},{"key":"8_CR10","unstructured":"Girard, J.Y.: Proof Theory and Logical Complexity. In: Studies in Proof Theory, Bibliopolis, Napoli (1987)"},{"key":"8_CR11","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. The Journal of Symbolic Logic\u00a054, 234\u2013263 (1989)","journal-title":"The Journal of Symbolic Logic"},{"key":"8_CR12","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1016\/B978-044450813-3\/50009-6","volume-title":"Handbook of Automated Reasoning","author":"R. Nieuwenhuis","year":"2001","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based Theorem Proving. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 371\u2013443. Elsevier, Amsterdam (2001)"},{"key":"8_CR13","doi-asserted-by":"crossref","DOI":"10.1515\/9780691218304","volume-title":"Mathematics and plausible reasoning: Induction and Analogy in Mathematics","author":"G. Polya","year":"1954","unstructured":"Polya, G.: Mathematics and plausible reasoning: Induction and Analogy in Mathematics, vol.\u00a0I. Princeton University Press, Princeton (1954)"},{"key":"8_CR14","doi-asserted-by":"crossref","DOI":"10.1515\/9780691218304","volume-title":"Mathematics and plausible reasoning: Patterns of Plausible Inference","author":"G. Polya","year":"1954","unstructured":"Polya, G.: Mathematics and plausible reasoning: Patterns of Plausible Inference, vol.\u00a0II. Princeton University Press, Princeton (1954)"},{"key":"8_CR15","volume-title":"Proof Theory","author":"G. Takeuti","year":"1987","unstructured":"Takeuti, G.: Proof Theory, 2nd edn. North-Holland, Amsterdam (1987)","edition":"2"},{"key":"8_CR16","unstructured":"Urban, C.: Classical Logic and Computation Ph.D. Thesis, University of Cambridge Computer Laboratory (2000)"},{"key":"8_CR17","doi-asserted-by":"publisher","first-page":"611","DOI":"10.1016\/B978-044450813-3\/50012-6","volume-title":"Handbook of Automated Reasoning","author":"A. Degtyarev","year":"2001","unstructured":"Degtyarev, A., Voronkov, A.: Equality Reasoning in Sequent-Based Calculi. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a0I ch. 10, pp. 611\u2013706. Elsevier Science, Amsterdam (2001)"}],"container-title":["Lecture Notes in Computer Science","Mathematical Knowledge Management"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11812289_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,1]],"date-time":"2021-08-01T17:07:57Z","timestamp":1627837677000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11812289_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540371045","9783540371069"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/11812289_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}