> I have an interesting problem with unification algorithm.
> The problem is basically that given two terms,
> either that unify, they don't unify, or *NEW* they don't
> unify yet but might later.

I believe you're looking for something called "residualization" in
constraint and logic programming: if the unification algorithm can return
not just a substitution but also some residual constraints that it wasn't
able to resolve (but which may be resolvable later).


        Stefan