高效的完全高阶一致化
摘要：通过Jensen和Pietrzykowski的研究，我们开发了一种枚举高阶统一器的完整集合的方法。我们的方法通过仔细限制搜索空间，并紧密集成可接受有限完整统一器集合的决策过程来消除许多多余的统一器。我们确定了一个新的片段，并描述了计算其统一器的方法。我们的统一程序与新的高阶术语索引数据结构一起实现在Zipperposition定理证明器中。实验评估显示与Jensen和 Pietrzykowski的方法相比具有明显的优势。
作者：Petar Vukmirovi''c, Alexander Bentkamp, Visa Nummelin
论文ID：2011.09507
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22