In unification, given a set of equations, a standard problem is to compute a most general unifier (mgu). I am interested in a somewhat reversed problem. Imagine having a set of equations that do not have an mgu, like this one:
x = a x = b
x here is a variable, whereas
b are terms. I am interested are there any algorithms that could find a possible replacement for
b such that the resulting equations have mgu? In the above example, that would be
a -> y, b -> y,
y being a variable. Lets call this a fix. I am particularly interested in most specific fixes. I could not find anything so far, but this seems like a natural problem, or not?