无序目标的反统一
计算复杂性
2021-10-22 v2 计算机科学中的逻辑
摘要
逻辑规划中的反统一指捕捉给定目标间公共句法结构、计算一个更一般的单一新目标(称为给定目标的泛化)的过程。为两个目标寻找任意公共泛化是平凡的,但寻找那些尽可能大(称为最大公共泛化)或尽可能具体(称为最具体泛化)的公共泛化是一个非平凡的优化问题,特别是当目标被视为原子的无序集合时。本文通过定义两种不同的泛化关系对该问题进行了深入研究。我们给出了两种设定下最具体泛化构成的刻画。尽管这些泛化可在多项式时间内计算,我们证明当泛化中变量数目需最小化时,该问题变为 NP-hard。随后我们重新审视了基于单射变量重命名的反统一下最大公共泛化的一种抽象,并证明其可在多项式有界时间内计算。
引用
@article{arxiv.2107.00341,
title = {Anti-unification of Unordered Goals},
author = {Gonzague Yernaux and Wim Vanhoof},
journal= {arXiv preprint arXiv:2107.00341},
year = {2021}
}
备注
CSL 2022 paper with appendices