ABSTRACT. Proximity relations are reflexive and symmetric fuzzy binary relations. They generalize similarity relations (similarity, in itself, is a generalization of equivalence in fuzzy setting) and have been introduced to deal with certain limitations of latter, related to incorrect representation of fuzzy information in some cases.

Following [1], we consider signatures where some function symbols are allowed to be in a proximity relation with each other. In our opinion, such a representation is more adequate than similarity to deal with possible mismatches between the names of symbols. Our terms are first-order terms, and the proximity relation is extended to them. In [1], a unification algorithm has been introduced for such terms. The problem we deal in this paper is a dual one: We are looking for generalizations, which, roughly, means that for two terms t1 and t2 we want to find a term r such that there exist substitution instances of r which are 'close enough to' (i.e., are in the given proximity relation with) t1 and t2.

Interestingly, the problem of computing a minimal complete set of generalizations with respect to a given proximity relation requires computing all possible maximal vertex-clique partitions in an undirected graph. We develop an algorithm for the all maximal clique partition problem, which is optimal in the sense that, first, it computes each maximal clique partition only once and, second, avoids generating and discarding false answers. Based on this method, we show that proximity-based anti-unification has the finitary type and develop a terminating, sound, and complete algorithm for computing a minimal complete set of generalizations.

[1] P. Julián-Iranzo and C. Rubio-Manzano. Proximity-based unification theory. Fuzzy Sets and Systems 262 (2015) 21–43.