Generalization algorithms and applications

Temur Kutsia

RISC, Johannes Kepler University Linz, Austria

In this talk, we discuss the generalization problem of logical terms and their applications. Given two terms s and t, their generalization is a term r such that s and t can be obtained from r by some substitutions. Interesting generalizations are the least general ones. Anti-unification is the process used to compute 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 inductive logic programming, case-based reasoning, analogy making, symbolic mathematical computing, computational linguistics, software maintenance, program analysis, synthesis, transformation, etc. Some of these algorithms and applications will be reviewed in the talk. We will also consider recent developments about generalization computation for special theories.