{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T19:16:07Z","timestamp":1770750967842,"version":"3.50.0"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032111753","type":"print"},{"value":"9783032111760","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,23]],"date-time":"2025-11-23T00:00:00Z","timestamp":1763856000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,23]],"date-time":"2025-11-23T00:00:00Z","timestamp":1763856000000},"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":[[2026]]},"DOI":"10.1007\/978-3-032-11176-0_12","type":"book-chapter","created":{"date-parts":[[2025,11,22]],"date-time":"2025-11-22T20:11:30Z","timestamp":1763842290000},"page":"185-201","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Efficient Interpolation Beyond Cut-Free Proofs: Admissible Cuts and\u00a0Optimized Extraction"],"prefix":"10.1007","author":[{"given":"Simon","family":"Corbard","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anela","family":"Loli\u0107","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,11,23]]},"reference":[{"issue":"2","key":"12_CR1","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. Symb. Comput. 29(2), 149\u2013177 (2000)","journal-title":"J. Symb. Comput."},{"issue":"3\u20134","key":"12_CR2","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. Symb. Comput. 41(3\u20134), 381\u2013410 (2006)","journal-title":"J. Symb. Comput."},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Baaz, M., Leitsch, A.: Methods of Cut-Elimination, vol. 34. Springer (2011)","DOI":"10.1007\/978-94-007-0320-9"},{"issue":"3","key":"12_CR4","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1016\/S0168-0072(96)00019-X","volume":"83","author":"A Carbone","year":"1997","unstructured":"Carbone, A.: Interpolants, cut elimination and flow graphs for the propositional calculus. Ann. Pure Appl. Log. 83(3), 249\u2013299 (1997)","journal-title":"Ann. Pure Appl. Log."},{"key":"12_CR5","unstructured":"Cerna, D.: Advances in schematic cut elimination. Ph.D. thesis, TU Wien (2015)"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/978-3-319-40229-1_17","volume-title":"Automated Reasoning","author":"DM Cerna","year":"2016","unstructured":"Cerna, D.M., Leitsch, A.: Schematic cut elimination and the ordered pigeonhole principle. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 241\u2013256. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_17"},{"issue":"5","key":"12_CR7","doi-asserted-by":"publisher","first-page":"599","DOI":"10.1007\/s10817-020-09583-8","volume":"65","author":"DM Cerna","year":"2021","unstructured":"Cerna, D.M., Leitsch, A., Lolic, A.: Schematic refutations of formula schemata. J. Autom. Reason. 65(5), 599\u2013645 (2021)","journal-title":"J. Autom. Reason."},{"issue":"03","key":"12_CR8","doi-asserted-by":"publisher","first-page":"269","DOI":"10.2307\/2963594","volume":"22","author":"W Craig","year":"1957","unstructured":"Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symb. Logic 22(03), 269\u2013285 (1957)","journal-title":"J. Symb. Logic"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische Schlie\u00dfen. Mathematische Zeitschrift 39, 176\u2013210, 405\u2013431 (1934-35)","DOI":"10.1007\/BF01201363"},{"issue":"3","key":"12_CR10","doi-asserted-by":"publisher","first-page":"619","DOI":"10.1007\/s11225-019-09867-0","volume":"108","author":"G Gherardi","year":"2020","unstructured":"Gherardi, G., Maffezioli, P., Orlandelli, E.: Interpolation in extensions of first-order logic. Stud. Logica. 108(3), 619\u2013648 (2020)","journal-title":"Stud. Logica."},{"issue":"2","key":"12_CR11","doi-asserted-by":"publisher","first-page":"457","DOI":"10.2307\/2275541","volume":"62","author":"J Kraj\u00edcek","year":"1997","unstructured":"Kraj\u00edcek, J.: Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. J. Symb. Log. 62(2), 457\u2013486 (1997)","journal-title":"J. Symb. Log."},{"issue":"3","key":"12_CR12","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/s10817-018-9453-9","volume":"62","author":"A Leitsch","year":"2019","unstructured":"Leitsch, A., Lolic, A.: Extraction of expansion trees. J. Autom. Reason. 62(3), 393\u2013430 (2019)","journal-title":"J. Autom. Reason."},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Leitsch, A., Lolic, A.: Herbrand\u2019s theorem in inductive proofs. In: LPAR. EPiC Series in Computing, vol. 100, pp. 295\u2013310. EasyChair (2024)","DOI":"10.29007\/dwdf"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Leitsch, A., Lolic, A.: Extracting herbrand systems from refutation schemata. J. Logic Comput. 35(7), exaf010 (2025)","DOI":"10.1093\/logcom\/exaf010"},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"Leitsch, A., Lolic, A., Mahler, S.: On proof schemata and primitive recursive arithmetic. In: LPAR 2024 Complementary Volume. Kalpa Publications in Computing, vol. 18, pp. 117\u2013130. EasyChair (2024)","DOI":"10.29007\/4g2q"},{"issue":"7","key":"12_CR16","first-page":"1897","volume":"27","author":"A Leitsch","year":"2017","unstructured":"Leitsch, A., Peltier, N., Weller, D.: CERES for first-order schemata. J. Log. Comput. 27(7), 1897\u20131954 (2017)","journal-title":"J. Log. Comput."},{"key":"12_CR17","unstructured":"Lolic, A.: Automated Proof Analysis by CERES. Ph.D. thesis, TU Wien (2020)"},{"issue":"1","key":"12_CR18","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23\u201341 (1965)","journal-title":"J. ACM"},{"key":"12_CR19","unstructured":"Takeuti, G.: Proof Theory, 2nd edn. North Holland (1987)"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2025"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-11176-0_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T11:09:45Z","timestamp":1770721785000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-11176-0_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,23]]},"ISBN":["9783032111753","9783032111760"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-11176-0_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,23]]},"assertion":[{"value":"23 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICTAC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Colloquium on Theoretical Aspects of Computing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Marrakesh","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Morocco","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 November 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 November 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ictac2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ictac2025.digital-hub.sh\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}