Anti-unification (AU), also known as generalization,1 is a fundamental operation used for inductive in-2 ference and is the dual operation to unification, an3 operation at the foundation of theorem proving. In-4 terest in AU from the AI and related communities5 is growing, but without a systematic study of the6 concept, nor surveys of existing work, investigations7 often resort to developing application specific meth-8 ods that may be covered by existing approaches. We9 provide the first survey of AU research and its ap-10 plications, together with a general framework for11 categorizing existing and future developments.
翻译:反统一(Anti-unification,AU),也称为泛化,是归纳推理中使用的基本操作,并且是定理证明基础操作——统一的对偶操作。AI及相关领域对AU的兴趣日益增长,但由于缺乏对该概念的系统性研究,也缺少对现有工作的综述,相关研究往往开发可能已被现有方法涵盖的特定应用方法。我们首次对AU研究及其应用进行了综述,同时提出了一个用于对现有及未来进展进行分类的通用框架。