一句话：提出两种基于项 DAG 表示的算法，用于在 EUF 中计算无量词一致插值，并给出正确性与完备性证明。
本文研究 EUF（未解释符号上的相等理论）中带待消去符号列表的无量词一致插值（uniform interpolant）计算问题。尽管该概念在逻辑文献中早已出现，形式方法与自动推理社区长期较少关注。作者首先精确界定一致插值，然后提出两种算法：第一种非确定性算法生成由文字的合取之析取表示的插值；第二种算法给出更紧凑的表示，将插值表示为 Horn 子句的合取。两种算法都利用高效的专用 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.
@article{paperbot1709,
title = {Uniform Interpolants in EUF: Algorithms using DAG-representations},
author = {Silvio Ghilardi and Alessandro Gianola and Deepak Kapur},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 2},
year = {2022},
doi = {10.46298/lmcs-18(2:2)2022}
}