{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:39:39Z","timestamp":1753889979611,"version":"3.41.2"},"reference-count":21,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,2,16]],"date-time":"2012-02-16T00:00:00Z","timestamp":1329350400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Theory interpolation has found several successful applications in model\nchecking. We present a novel method for computing interpolants for ground\nformulas in the theory of equality. The method produces interpolants from\ncolored congruence graphs representing derivations in that theory. These graphs\ncan be produced by conventional congruence closure algorithms in a\nstraightforward manner. By working with graphs, rather than at the level of\nindividual proof steps, we are able to derive interpolants that are pleasingly\nsimple (conjunctions of Horn clauses) and smaller than those generated by other\ntools. Our interpolation method can be seen as a theory-specific implementation\nof a cooperative interpolation game between two provers. We present a generic\nversion of the interpolation game, parametrized by the theory T, and define a\ngeneral method to extract runs of the game from proofs in T and then generate\ninterpolants from these runs.<\/jats:p>","DOI":"10.2168\/lmcs-8(1:6)2012","type":"journal-article","created":{"date-parts":[[2012,9,6]],"date-time":"2012-09-06T10:03:11Z","timestamp":1346925791000},"source":"Crossref","is-referenced-by-count":5,"title":["Ground interpolation for the theory of equality"],"prefix":"10.46298","volume":"Volume 8, Issue 1","author":[{"given":"Alexander","family":"Fuchs","sequence":"first","affiliation":[]},{"given":"Amit","family":"Goel","sequence":"additional","affiliation":[]},{"given":"Jim","family":"Grundy","sequence":"additional","affiliation":[]},{"given":"Sava","family":"Krsti\u0107","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6726-775X","authenticated-orcid":false,"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,2,16]]},"reference":[{"key":"10.2168\/LMCS-8(1:6)2012_BarST-SMTLIB","unstructured":"Clark Barrett, Aaron Stump, and Cesare Tinelli. The Satisfiability Modulo Theories Library (SMT-LIB). http:\/\/www.SMT-LIB.org, 2011."},{"key":"10.2168\/LMCS-8(1:6)2012_CimGS-TACAS-08","doi-asserted-by":"crossref","unstructured":"Alessandro Cimatti, Alberto Griggio, and Roberto Sebastiani. Efficient interpolant generation in satisfiability modulo theories. In C. R. Ramakrishnan and Jakob Rehof, editors,TACAS, volume 4963 ofLNCS, pages 397-412. Springer, 2008.","DOI":"10.1007\/978-3-540-78800-3_30"},{"key":"10.2168\/LMCS-8(1:6)2012_Cra-JSL-57","doi-asserted-by":"publisher","DOI":"10.2307\/2963594"},{"key":"10.2168\/LMCS-8(1:6)2012_DefNS-JACM-05","doi-asserted-by":"publisher","DOI":"10.1145\/1066100.1066102"},{"key":"10.2168\/LMCS-8(1:6)2012_FucGGKT-TACAS-09","doi-asserted-by":"crossref","unstructured":"Alexander Fuchs, Amit Goel, Jim Grundy, Sava Krsti\u00c4\u0087, and Cesare Tinelli. Ground interpolation for the theory of equality. In S. Kowalewski and A. Philippou, editors,Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (York, UK), volume 5505 ofLecture Notes in Computer Science, pages 413-427. Springer, 2009.","DOI":"10.1007\/978-3-642-00768-2_34"},{"key":"10.2168\/LMCS-8(1:6)2012_Ghi-JAR-05","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-004-6241-5"},{"key":"10.2168\/LMCS-8(1:6)2012_GoeKT-CADE-09","doi-asserted-by":"crossref","unstructured":"Amit Goel, Sava Krsti\u00c4\u0087, and Cesare Tinelli. Ground interpolation for combined theories. In R. Schmidt, editor,Proceedings of the 22nd International Conference on Automated Deduction (Montreal, Canada), volume 5663 ofLecture Notes in Artificial Intelligence, pages 183-198. Springer, 2009.","DOI":"10.1007\/978-3-642-02959-2_16"},{"key":"10.2168\/LMCS-8(1:6)2012_JaiCG-CAV-08","doi-asserted-by":"crossref","unstructured":"Himanshu Jain, Edmund M. Clarke, and Orna Grumberg. Efficient craig interpolation for linear diophantine (dis)equations and linear modular equations. InProceedings of the 20th International Conference on Computer-Aided Verification, pages 254-267, 2008.","DOI":"10.1007\/978-3-540-70545-1_24"},{"key":"10.2168\/LMCS-8(1:6)2012_JahMcM-CAV-05","doi-asserted-by":"crossref","unstructured":"Ranjit Jhala and Kenneth L. McMillan. Interpolant-based transition relation approximation. In Kousha Etessami and Sriram K. Rajamani, editors,Proceedings of 17th International Conference on Computer Aided Verification (Edinburgh, Scotland, UK), volume 3576 ofLecture Notes in Computer Science, pages 39-51. Springer, 2005.","DOI":"10.1007\/11513988_6"},{"key":"10.2168\/LMCS-8(1:6)2012_JhaMcM-TACAS-06","doi-asserted-by":"crossref","unstructured":"Ranjit Jhala and Kenneth L. McMillan. A practical and complete approach to predicate refinement. InProceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 459-473, 2006.","DOI":"10.1007\/11691372_33"},{"key":"10.2168\/LMCS-8(1:6)2012_KapMZ-SIGSOFT-06","doi-asserted-by":"crossref","unstructured":"Deepak Kapur, Rupak Majumdar, and Calogero G. Zarba. Interpolation for data structures. In Michal Young and Premkumar T. Devanbu, editors,SIGSOFT FSE, pages 105-116. ACM, 2006.","DOI":"10.1145\/1181775.1181789"},{"key":"10.2168\/LMCS-8(1:6)2012_McC-CAV-03","doi-asserted-by":"crossref","unstructured":"Ken McMillan. Interpolation and SAT-based model checking. In W. A. Hunt Jr. and F. Somenzi, editors,CAV, volume 2725 ofLNCS, pages 1-13. Springer, 2003.","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"10.2168\/LMCS-8(1:6)2012_McM-TACAS-05","doi-asserted-by":"crossref","unstructured":"Kenneth L. McMillan. Applications of Craig interpolants in model checking. In Nicolas Halbwachs and Lenore D. Zuck, editors,TACAS, volume 3440 ofLNCS, pages 1-12. Springer, 2005.","DOI":"10.1007\/978-3-540-31980-1_1"},{"key":"10.2168\/LMCS-8(1:6)2012_McM-TCS-05","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.07.003"},{"key":"10.2168\/LMCS-8(1:6)2012_McM-CAV-06","doi-asserted-by":"crossref","unstructured":"Kenneth L. McMillan. Lazy abstraction with interpolants. In T. Ball and R. Jones, editors,CAV, volume 4144 ofLNCS, pages 123-136. Springer, 2006.","DOI":"10.1007\/11817963_14"},{"issue":"2","key":"10.2168\/LMCS-8(1:6)2012_NelOpp-TPLS-79","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"Greg Nelson and Derek C. Oppen","year":"1979","journal-title":"\u00c3\u0085CM Transactions on Programming Languages and Systems 1(2):245-257, 1979"},{"key":"10.2168\/LMCS-8(1:6)2012_NelOpp-JACM-80","doi-asserted-by":"publisher","DOI":"10.1145\/322186.322198"},{"key":"10.2168\/LMCS-8(1:6)2012_NieOli-RTA-05","doi-asserted-by":"crossref","unstructured":"Robert Nieuwenhuis and Albert Oliveras. Proof-producing congruence closure. In J. Giesl, editor,RTA, volume 3467 ofLNCS, pages 453-468. Springer, 2005.","DOI":"10.1007\/978-3-540-32033-3_33"},{"key":"10.2168\/LMCS-8(1:6)2012_Pud-JSL-97","doi-asserted-by":"crossref","unstructured":"Pavel Pudl\u00e1k. Lower bounds for resolution and cutting planes proofs and monotone computations.Journal of Symbolic Logic, 62(3), 1997.","DOI":"10.2307\/2275583"},{"key":"10.2168\/LMCS-8(1:6)2012_DPT","unstructured":"Various. Decision Procedure Toolkit."},{"key":"10.2168\/LMCS-8(1:6)2012_YorMus-CADE-05","doi-asserted-by":"crossref","unstructured":"Greta Yorsh and Madanlal Musuvathi. A combination method for generating interpolants. In Robert Nieuwenhuis, editor,CADE, volume 3632 ofLNCS, pages 353-368. Springer, 2005.","DOI":"10.1007\/11532231_26"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/709\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/709\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:54:18Z","timestamp":1681242858000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/709"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,2,16]]},"references-count":21,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(1:6)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1111.5652","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1111.5652","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,2,16]]},"article-number":"709"}}