无序目标的反统一
Anti-unification of Unordered Goals
摘要：
逻辑编程中的反统一是指捕获给定目标之间的公共语法结构，计算单个新目标的过程，该目标更一般地称为给定目标的泛化。找到两个目标的任意公共概括是微不足道的，但是寻找那些尽可能大（称为最大公共概括）或尽可能具体（称为最具体概括）的公共概括是一个非平凡的优化问题，特别是当目标被认为是\textit{unordered}原子集时。在这项工作中，我们提供了一个深入研究的问题，通过定义两个不同的泛化关系。我们制定了一个表征什么构成了最具体的概括在这两种设置。虽然这些推广可以计算在多项式时间，我们表明，当变量的数量在推广需要最小化，问题成为NP-难。随后，我们重新审视了最大的共同推广的抽象时，反统一是基于单射变量更名，并证明它可以计算在多项式有界的时间。
英文摘要：
Anti-unification in logic programming refers to the process of capturing common syntactic structure among given goals, computing a single new goal that is more general called a generalization of the given goals. Finding an arbitrary common generalization for two goals is trivial, but looking for those common generalizations that are either as large as possible (called largest common generalizations) or as specific as possible (called most specific generalizations) is a non-trivial optimization problem, in particular when goals are considered to be \textit{unordered} sets of atoms. In this work we provide an in-depth study of the problem by defining two different generalization relations. We formulate a characterization of what constitutes a most specific generalization in both settings. While these generalizations can be computed in polynomial time, we show that when the number of variables in the generalization needs to be minimized, the problem becomes NP-hard. We subsequently revisit an abstraction of the largest common generalization when anti-unification is based on injective variable renamings, and prove that it can be computed in polynomially bounded time.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
