Proof Tree Preserving Interpolation
Proof Tree Preserving Interpolation
复制标题
证明树保留插值
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Alexander Nutz
中科院分区：
文献类型：
--
作者：
Jürgen Christ;Jochen Hoenicke;Alexander Nutz
SMT 中的克雷格插值很困难，因为，例如。例如，理论组合和整数切割引入了混合文字，i。即，包含来自两个输入公式的局部符号的文字。在本文中，我们提出了一种在存在混合文字的情况下计算克雷格插值的方案。与现有方法相反，该方案既不限制 SMT 求解器所做的推理，也不在提取插值之前转换证明树。我们的方案适用于未解释函数和线性算术的组合，但可以扩展到其他理论。该方案在插值 SMT 求解器 SMTInterpol 中实现。
Craig interpolation in SMT is difficult because, e. g., theory combination and integer cuts introduce mixed literals, i. e., literals containing local symbols from both input formulae. In this paper, we present a scheme to compute Craig interpolants in the presence of mixed literals. Contrary to existing approaches, this scheme neither limits the inferences done by the SMT solver, nor does it transform the proof tree before extracting interpolants. Our scheme works for the combination of uninterpreted functions and linear arithmetic but is extendable to other theories. The scheme is implemented in the interpolating SMT solver SMTInterpol.