Generalization: Algorithms and Applications

Generalization is a process of obtaining more general objects from concrete ones. It is a key concept in inductive reasoning. In its simplest form, a generalization of two logical terms is a term from which the original ones are obtained by variable substitution. 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 a similarity relation and for compressed terms), their analysis, investigation of efficient special cases, free open source implementation, and applications.

Generalization is a process of obtaining more general objects from concrete ones. It is a key concept in inductive reasoning. In its simplest form, a generalization of two logical terms is a term from which the original ones are obtained by variable substitution. 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 addressed challenges to generalization computation posed by new application domains. We developed new generalization algorithms for equational and higher-order theories (also with respect to proximity relations and for compressed terms), analyzed them, investigated efficient special cases, provided free open source implementation, and discussed applications. The project made important contributions towards advancing the state-of-the-art of generalization algorithms and raised new research problems to be investigated in the future.