Anti-unification (AU) is a fundamental operation for generalization computation used for inductive inference. It is the dual operation to unification, an operation at the foundation of automated theorem proving. Interest in AU from the AI and related communities is growing, but without a systematic study of the concept nor surveys of existing work, investigations often resort to developing application-specific methods that existing approaches may cover. We provide the first survey of AU research and its applications and a general framework for categorizing existing and future developments.

翻译：反统一（Anti-unification, AU）是归纳推理中用于泛化计算的基本操作，其与作为自动定理证明基础的统一操作互为对偶。尽管人工智能及相关领域对反统一的兴趣与日俱增，但由于缺乏对该概念的系统性研究及现有工作的综述，相关研究往往倾向于开发可能已涵盖现有方法的特定应用技术。本文首次对反统一研究及其应用进行综述，并提出一个通用框架，用于对现有及未来的发展进行分类。