Anti-unification and Generalization: A Survey

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.