EUF中的均匀插值：使用DAG表示的算法
摘要：用给定的符号列表从一个公式中为一个无量词的公式概念生成统一插值器，并在逻辑文献中已被广为人知，然而长期以来形式方法和自动推理社区对此概念并不了解。该概念已被准确定义。本文提出了两种算法，用于在带有一个要消除的符号列表的未解释符号相等理论（EUF）中计算无量词的统一插值器。第一种算法是非确定性算法，生成以文字的合取为析取的统一插值器，而第二种算法以Horn子句的合取形式给出统一插值器的紧凑表示。两种算法都利用了有效的专用DAG表示术语。使用重写技术和模型理论结合的论证提供了正确性和完备性证明。
作者：Silvio Ghilardi and Alessandro Gianola and Deepak Kapur
论文ID：2002.09784
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22