等式理论的基插值
Ground interpolation for the theory of equality
摘要：
理论插值在模型检验中得到了成功的应用。提出了一种新的计算等式理论中基公式插值的方法。该方法产生插值从彩色同余图表示在该理论中的推导。这些图可以产生传统的同余闭包算法在一个简单的方式。通过使用图，而不是在单个证明步骤的水平上，我们能够推导出令人愉快的简单（Horn子句的合取）和小于其他工具生成的插值。我们的插值方法可以被看作是一个理论特定的实现两个证明者之间的合作插值游戏。我们提出了一个通用版本的插值游戏，参数化的理论T，并定义了一个通用的方法来提取运行的游戏证明T，然后从这些运行生成插值。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
