{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:00:24Z","timestamp":1750309224562,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":28,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,7,8]],"date-time":"2024-07-08T00:00:00Z","timestamp":1720396800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,7,8]]},"DOI":"10.1145\/3661814.3662112","type":"proceedings-article","created":{"date-parts":[[2024,6,21]],"date-time":"2024-06-21T12:30:12Z","timestamp":1718973012000},"page":"1-13","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["On the Completeness of Interpolation Algorithms"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6461-5982","authenticated-orcid":false,"given":"Stefan","family":"Hetzl","sequence":"first","affiliation":[{"name":"Institute of Discrete Mathematics and Geometry, Vienna University of Technology, Vienna, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3321-8087","authenticated-orcid":false,"given":"Raheleh","family":"Jalali","sequence":"additional","affiliation":[{"name":"Computer Science, Czech Academy of Sciences, Prague, Czech Republic"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,7,8]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2004.11.004"},{"key":"e_1_3_2_1_2_1","volume-title":"Mathematical Logic and Computation","author":"Avigad J.","year":"2023","unstructured":"J. Avigad. Mathematical Logic and Computation. Cambridge University Press, 2023."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2003.10.005"},{"key":"e_1_3_2_1_4_1","series-title":"Trends in Logic","volume-title":"Methods of Cut-Elimination","author":"Baaz M.","year":"2011","unstructured":"M. Baaz and A. Leitsch. Methods of Cut-Elimination, volume 34 of Trends in Logic. Springer, 2011."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1385-7258(53)50042-3"},{"key":"e_1_3_2_1_6_1","volume-title":"Handbook of proof theory","author":"Buss S. R.","year":"1998","unstructured":"S. R. Buss. Handbook of proof theory. Elsevier, 1998."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46081-8_2"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.2307\/2963594"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"crossref","unstructured":"V. V. D'Silva D. Kroening M. Purandare and G. Weissenbacher. Interpolant strength. In G. Barthe and M. V. Hermenegildo editors 11th International Conference on Verification Model Checking and Abstract Interpretation (VMCAI) volume 5944 of Lecture Notes in Computer Science pages 129--145. Springer 2010.","DOI":"10.1007\/978-3-642-11319-2_12"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511576430"},{"key":"e_1_3_2_1_11_1","first-page":"259","volume-title":"Symposium on Principles of Programming Languages (POPL) 2012","author":"Hoder K.","year":"2012","unstructured":"K. Hoder, L. Kov\u00e1cs, and A. Voronkov. Playing in the Grey Area of Proofs. In J. Field and M. Hicks, editors, Symposium on Principles of Programming Languages (POPL) 2012, pages 259--272. ACM, 2012."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030832"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"crossref","unstructured":"R. Jhala and K. L. McMillan. Interpolant-based transition relation approximation. In K. Etessami and S. K. Rajamani editors 17th International Conference on Computer Aided Verification (CAV) volume 3576 of Lecture Notes in Computer Science pages 39--51. Springer 2005.","DOI":"10.1007\/11513988_6"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","unstructured":"R. Jhala and K. L. McMillan. A practical and complete approach to predicate refinement. In H. Hermanns and J. Palsberg editors 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) volume 3920 of Lecture Notes in Computer Science pages 459--473. Springer 2006.","DOI":"10.1007\/11691372_33"},{"key":"e_1_3_2_1_15_1","volume-title":"Interpolant-Based Transition Relation Approximation. Logical Methods in Computer Science, 3(4)","author":"Jhala R.","year":"2007","unstructured":"R. Jhala and K. L. McMillan. Interpolant-Based Transition Relation Approximation. Logical Methods in Computer Science, 3(4), 2007."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"crossref","unstructured":"L. Kov\u00e1cs and A. Voronkov. Interpolation and symbol elimination. In R. A. Schmidt editor 22nd International Conference on Automated Deduction (CADE-22) volume 5663 of Lecture Notes in Computer Science pages 199--213. Springer 2009.","DOI":"10.1007\/978-3-642-02959-2_17"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275250"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275541"},{"key":"e_1_3_2_1_19_1","volume-title":"North-Holland","author":"Kreisel G.","year":"1967","unstructured":"G. Kreisel and J.-L. Krivine. Elements of Mathematical Logic (Model Theory). North-Holland, 1967."},{"issue":"3","key":"e_1_3_2_1_20_1","first-page":"313","article-title":"Interpolations - Essays","volume":"164","author":"Mancosu P.","year":"2008","unstructured":"P. Mancosu. Introduction: Interpolations - Essays in Honor of William Craig. Synthese, 164(3):313--319, 2008.","journal-title":"Honor of William Craig. Synthese"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_14"},{"key":"e_1_3_2_1_22_1","volume-title":"Structural proof theory","author":"Negri S.","year":"2008","unstructured":"S. Negri and J. Von Plato. Structural proof theory. Cambridge university press, 2008."},{"key":"e_1_3_2_1_23_1","volume-title":"Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems (TOPLAS), 1(2):245--257","author":"Nelson G.","year":"1979","unstructured":"G. Nelson and D. C. Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems (TOPLAS), 1(2):245--257, 1979."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275583"},{"key":"e_1_3_2_1_25_1","volume-title":"Proof Theory. North-Holland","author":"Takeuti G.","year":"1987","unstructured":"G. Takeuti. Proof Theory. North-Holland, Amsterdam, 2nd edition, March 1987.","edition":"2"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022587501759"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139168717"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31612-8_24"}],"event":{"name":"LICS '24: 39th Annual ACM\/IEEE Symposium on Logic in Computer Science","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation","IEEE Computer Society","EACSL"],"location":"Tallinn Estonia","acronym":"LICS '24"},"container-title":["Proceedings of the 39th Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3661814.3662112","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3661814.3662112","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T23:44:09Z","timestamp":1750290249000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3661814.3662112"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,7,8]]},"references-count":28,"alternative-id":["10.1145\/3661814.3662112","10.1145\/3661814"],"URL":"https:\/\/doi.org\/10.1145\/3661814.3662112","relation":{},"subject":[],"published":{"date-parts":[[2024,7,8]]},"assertion":[{"value":"2024-07-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}