Matching - a special case of unification? (Q582272)

A generalization of the notions of matching and unrestricted unification - so-called variable-restricted unification - is proposed. The author investigates relationships between matching and unification and shows that for collapse-free theories (i.e. for theories where a non-variable term is never E-equal to a variable) matching and unification have similar behavior with respect to the existence and the cardinality of minimal complete sets of solutions. Some counter-examples where matching and unification behave differently are presented. It is shown that the existence of solutions is decidable for the unification problem but is undecidable for the matching problem. Since the matching problem may be reduced to a unification problem by introducing new free constants in signature, these counterexamples show that a decidable unification problem may become undecidable after adding free constants to a signature.