{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,12]],"date-time":"2025-06-12T14:03:37Z","timestamp":1749737017507,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662469057"},{"type":"electronic","value":"9783662469064"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46906-4_8","type":"book-chapter","created":{"date-parts":[[2015,4,30]],"date-time":"2015-04-30T09:59:50Z","timestamp":1430387990000},"page":"117-136","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Cut-Elimination and Proof Schemata"],"prefix":"10.1007","author":[{"given":"Cvetan","family":"Dunchev","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Leitsch","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mikheil","family":"Rukhaia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Weller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,5,1]]},"reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-02716-1_4","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"V Aravantinos","year":"2009","unstructured":"Aravantinos, V., Caferra, R., Peltier, N.: A schemata calculus for propositional logic. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS (LNAI), vol. 5607, pp. 32\u201346. Springer, Heidelberg (2009)"},{"key":"8_CR2","doi-asserted-by":"crossref","first-page":"599","DOI":"10.1613\/jair.3351","volume":"40","author":"V Aravantinos","year":"2011","unstructured":"Aravantinos, V., Caferra, R., Peltier, N.: Decidability and undecidability results for propositional schemata. J. Artif. Intell. Res. 40, 599\u2013656 (2011)","journal-title":"J. Artif. Intell. Res."},{"issue":"2","key":"8_CR3","doi-asserted-by":"crossref","first-page":"101","DOI":"10.3233\/FI-2013-855","volume":"125","author":"V Aravantinos","year":"2013","unstructured":"Aravantinos, V., Echenim, M., Peltier, N.: A resolution calculus for first-order schemata. Fundamenta Informaticae 125(2), 101\u2013133 (2013)","journal-title":"Fundamenta Informaticae"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science (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":"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. 3452, pp. 481\u2013495. Springer, Heidelberg (2005)"},{"key":"8_CR5","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. Theoret. Comput. Sci. 403, 160\u2013175 (2008)","journal-title":"Theoret. Comput. Sci."},{"issue":"2","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. J. Symbolic Comput. 29(2), 149\u2013176 (2000)","journal-title":"J. Symbolic Comput."},{"issue":"3\u20134","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. J. Symbolic Comput. 41(3\u20134), 381\u2013410 (2006)","journal-title":"J. Symbolic Comput."},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/11554554_8","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"J Brotherston","year":"2005","unstructured":"Brotherston, J.: Cyclic proofs for first-order logic with inductive definitions. In: Beckert, B. (ed.) TABLEAUX 2005. LNCS (LNAI), vol. 3702, pp. 78\u201392. Springer, Heidelberg (2005)"},{"issue":"6","key":"8_CR9","doi-asserted-by":"publisher","first-page":"1177","DOI":"10.1093\/logcom\/exq052","volume":"21","author":"J Brotherston","year":"2011","unstructured":"Brotherston, J., Simpson, A.: Sequent calculi for induction and infinite descent. J. Log. Comput. 21(6), 1177\u20131216 (2011)","journal-title":"J. Log. Comput."},{"key":"8_CR10","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1017\/S0960129507006573","volume":"18","author":"A Ciabattoni","year":"2008","unstructured":"Ciabattoni, A., Leitsch, A.: Towards an algorithmic construction of cut-elimination procedures. Math. Struct. Comput. Sci. 18, 81\u2013105 (2008)","journal-title":"Math. Struct. Comput. Sci."},{"key":"8_CR11","unstructured":"Dunchev, C.: Automation of Cut-Elimination in Proof Schemata. Ph.D. thesis, Vienna University of Technology (2012)"},{"key":"8_CR12","unstructured":"Dunchev, C., Leitsch, A., Rukhaia, M., Weller, D.: CERES for First-Order Schemata. Technical report, Vienna University of Technology (2012). http:\/\/arxiv.org\/abs\/1303.4257"},{"key":"8_CR13","unstructured":"Fontaine, P., Merz, S., Paleo, B.W.: Exploring and exploiting algebraic and graphical properties of resolution. In: SMT 2010. Edinburgh (2010)"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Martin-L\u00f6f, P.: Hauptsatz for the Intuitionistic Theory of Iterated Inductive Definitions. In: Proceedings of the Second Scandinavian Logic Symposium, vol. 63 of Studies in Logic and the Foundations of Mathematics, pp. 179\u2013216 (1971)","DOI":"10.1016\/S0049-237X(08)70847-4"},{"issue":"1\u20132","key":"8_CR15","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/S0304-3975(99)00171-1","volume":"232","author":"R McDowell","year":"2000","unstructured":"McDowell, R., Miller, D.: Cut-elimination for a logic with definitions and induction. Theoret. Comput. Sci. 232(1\u20132), 91\u2013119 (2000)","journal-title":"Theoret. Comput. Sci."},{"key":"8_CR16","unstructured":"Rukhaia, M.: CERES in Proof Schemata. Ph.D. thesis, Vienna University of Technology (2012)"},{"key":"8_CR17","unstructured":"Salzer, G.: On the Relationship between Cycle Unification and the Unification of Infinite Sets of Terms. In: Baader, F., Snyder, W. (eds.) UNIF 1993, Mass, Boston (1993)"},{"key":"8_CR18","volume-title":"Proof Theory","author":"G Takeuti","year":"1987","unstructured":"Takeuti, G.: Proof Theory, 2nd edn. North Holland, Amsterdam (1987)","edition":"2"}],"container-title":["Lecture Notes in Computer Science","Logic, Language, and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46906-4_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,15]],"date-time":"2023-02-15T07:30:41Z","timestamp":1676446241000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-46906-4_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662469057","9783662469064"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46906-4_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"1 May 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}