Anti-Unification: Algorithms and Applications

30^th April 2015, 13:00 Ashton Lecture Theater
Dr Temur Kutsia
Research Institute for Symbolic Computation
Linz
Austria

Abstract

The anti-unification problem of two terms t1 and t2 is concerned with finding a term t which generalizes both t1 and t2. 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 in the 1970s, with the works by Gordon 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, program analysis, synthesis, transformation, verification, etc. After briefly reviewing some of these algorithms and applications, we will discuss recent developments in unranked and nominal generalization computation.