We present a fast algorithm for uniform semi-unification based on adapting the Huet unification closure method for standard
unification. It solves the following decision problem in O(n
2
α(n)
2), where n is the size of the two terms, and α is the functional inverse of Ackermann's function: Given two terms s and t, do there exist two substitutions σ and ρ such that ρ(σ(s)) = σ(t)? In the affirmative case, a solution σ can be constructed within the same time bound. However, if a principal solution (analogous to an mgu) is required, some modifications
to the algorithm must be made, and the upper bound increases to O(n
2
log
2(nα(n))α(n)
2).