A modular order-sorted equational generalization algorithm (Q2437800)

Generalization algorithms attract interest because of their wide scope of applications. In various forms, they are used in machine learning, inductive logic programming, cognitive modeling, program analysis and synthesis, automated reasoning, symbolic computation, linguistics, etc. The problem these algorithms solve is the following: Given two terms \(t_1\) and \(t_2\) in a certain theory, find a term \(t\) such that \(t_1\) and \(t_2\) are substitution instances of \(t\). Such a \(t\) is called a generalization of \(t_1\) and \(t_2\). The task is to find least general generalizations. The algorithms that compute generalizations are also called anti-unification algorithms, since the process is seen to be dual to unification that aims to unify two terms and, in this way, obtain their most general common instance. The paper addresses this problem in several first-order equational theories with and without sorts, namely, (i) syntactic order-sorted anti-unification, (ii) modular anti-unification for equational theories of associativity, commutativity, identity, and their combinations, (iii) order-sorted modular equational generalization that combines the rules of the mentioned algorithms: order-sorted anti-unification on the one hand, and equational anti-unification on the other hand. Order-sorted equational anti-unification in the considered theories is finitary, i.e., the minimal complete set of generalizations is finite, not necessarily a singleton. This is in contrast to the syntactic first-order anti-unification (which is unitary), and also to some equational unification problems (e.g., associative unification is infinitary, while the corresponding anti-unification problem is finitary). The authors provide a rigorous treatment of these problems, design the corresponding algorithms, and prove their properties. The algorithms are implemented and freely available.