Proximity-based unification theory

Similarity-based Logic Programming has been proposed to enhance the Logic Programming paradigm with similarity relations, in order to represent and manage vague or imprecise information. A similarity relation is a reflexive, symmetric, transitive fuzzy binary relation, extending the standard notion of equivalence relation with the purpose of weakening the concept of equality. As is reported, similarity relations have significant limitations, due to the transitivity restriction, that can lead to representing fuzzy information incorrectly in some situations.Recently we have proposed the use of proximity relations (i.e., reflexive, symmetric, fuzzy binary relations) in the context of a logic programming system, called Bousi∼Prolog, as a way of solving this problem and generalizing later approaches exclusively based on similarity relations. However, a naive combination of proximity relations and the existing unification algorithms may cause incompleteness problems. Hence, in this paper, we introduce an accurate definition of proximity between expressions (terms or atomic formulas) and a new unification algorithm able to manage proximity relations properly. The so-called weak unification algorithm is an extension of Martelli and Montanari's unification algorithm supported by the new notion of proximity. As major relevant properties, we prove that the weak unification algorithm terminates and it is sound (i.e., it produces a weak unifier of two expressions, if they are unifiable) and complete (i.e., it is able to compute a weak most general unifier for two unifiable expressions).