Supported by the Austrian Science Fund (FWF), Project P 28789-N32 (2016-2019)
Generalization is a process of obtaining more general objects from concrete ones. It is a key concept in inductive reasoning. In its simplest form, generalization of two terms s and t is a term r such that s and t can be obtained from r by some variable substitutions. From all such generalizations, the interesting ones are those that can not be made more specific: least general generalizations.
The process of computing least general generalizations is known as anti-unification. It is a procedure dual to unification, which can be seen as a computation of most general common instances of the given terms (most general specifications).
Current research on anti-unification is dominated by practically oriented topics, which is not surprising, because generalization computation, in various forms, is an important ingredient of many applications in reasoning, learning, information extraction, data compression, software development and analysis, etc.
In this project we address challenges to generalization computation posed by new application domains. Some require studying generalization problems in a completely new theory. Some others may be dealt more adequately by improving existing algorithms. It is well-known that in many applications, the standard first-order anti-unification is too weak. We are concerned with the development of generalization algorithms for equational and higher-order theories (also with respect to special similarity relations and for terms in specific forms), their analysis, investigation of efficient special cases, free open source implementation, and applications.