文章基本信息

标题：Ground interpolation for the theory of equality
本地全文：下载
作者：Alexander Fuchs ; Amit Goel ; Jim Grundy 等
期刊名称：Logical Methods in Computer Science
印刷版ISSN：1860-5974
电子版ISSN：1860-5974
出版年度：2012
卷号：8
期号：1
页码：1
DOI：10.2168/LMCS-8(1:6)2012
出版社：Technical University of Braunschweig
摘要：Theory interpolation has found several successful applications in model checking. We present a novel method for computing interpolants for ground formulas in the theory of equality. The method produces interpolants from colored congruence graphs representing derivations in that theory. These graphs can be produced by conventional congruence closure algorithms in a straightforward manner. By working with graphs, rather than at the level of individual proof steps, we are able to derive interpolants that are pleasingly simple (conjunctions of Horn clauses) and smaller than those generated by other tools. Our interpolation method can be seen as a theory-specific implementation of a cooperative interpolation game between two provers. We present a generic version of the interpolation game, parametrized by the theory T, and define a general method to extract runs of the game from proofs in T and then generate interpolants from these runs.
其他关键词：Logical Interpolation, Satisfiability Modulo Theories