A similarity-based resolution rule

We propose an extension of the resolution rule as the core of a logic programming language based on similarity. Starting from a fuzzy unification algorithm described in Ref. 2 and then extended in Ref. 10, we introduce a fuzzy resolution rule, based on an extended most general unifier supplied by the extended unification algorithm. In our approach, unification fades into a unification degree because of a similarity introduced in a first-order language. Intuitively, the unification degree of a set of first-order terms is the cost one has to pay to consider these terms as equal. For this reason, our extension of the resolution is more structured than its classic counterpart;that is, when the empty clause is reached, in addition to a computed answer, a set of conditions is also determined. We give both the operational and fixed-point semantics of our extended logic programming language, and we prove their equivalence.