论文标题
EUF：使用DAG代理的算法中的均匀插值
Uniform Interpolants in EUF: Algorithms using DAG-representations
论文作者
论文摘要
从给定的公式列表中的无量词公式的统一插值概念虽然在逻辑文献中众所周知，但很长一段时间以来，正式方法和自动推理社区都不知道。这个概念是精确定义的。提出了两种用于计算无解释符号（EUF）的平等理论中无量词统一插入物（EUF）的算法。第一种算法是非确定性的，并产生均匀的插值剂，表达为文字结合的脱节，而第二算法给出了均匀的interpolant作为喇叭曲线的结合的均匀插入剂的紧凑表示。两种算法都利用了有效的术语专用DAG表示。使用将重写技术与模型理论相结合的参数，提供了正确性和完整性证明。
The concept of uniform interpolant for a quantifier-free formula from a given formula with a list of symbols, while well-known in the logic literature, has been unknown to the formal methods and automated reasoning community for a long time. This concept is precisely defined. Two algorithms for computing quantifier-free uniform interpolants in the theory of equality over uninterpreted symbols (EUF) endowed with a list of symbols to be eliminated are proposed. The first algorithm is non-deterministic and generates a uniform interpolant expressed as a disjunction of conjunctions of literals, whereas the second algorithm gives a compact representation of a uniform interpolant as a conjunction of Horn clauses. Both algorithms exploit efficient dedicated DAG representations of terms. Correctness and completeness proofs are supplied, using arguments combining rewrite techniques with model theory.
