Anti-Unification: Algorithms and Applications

Abstract

The anti-unification problem of two terms t<sub>1</sub> and t<sub>2</sub> is concerned with finding a term t which generalizes both t<sub>1</sub> and t<sub>2</sub>. That is, the input terms should be substitution instances of the generalization term. Interesting generalizations are the least general ones. The purpose of anti-unification algorithms is to compute such least general generalizations. Research on anti-unification has been initiated more than four decades ago, with the pioneering works by Gordon~D.~Plotkin and John~C.~Reynolds. Since then, a number of algorithms and their modifications have been developed, addressing the problem in first-order or higher-order languages, for syntactic or equational theories, over ranked or unranked alphabets, with or without sorts/types, etc. Anti-unification has found applications in machine learning, inductive logic programming, case-based reasoning, analogy making, symbolic mathematical computing, software maintenance, program analysis, synthesis, transformation, and verification. Some of these algorithms and applications will be reviewed in the talk. We will also consider recent developments in unranked and higher-order generalization computation.