Ugo Montanari

Ugo Montanari coauthored the 1982 unification algorithm with Alberto Martelli. Their paper treats first-order terms as equations and derives an efficient implementation from simpler transformation rules, integrating the acyclicity test needed for finite terms.^[ref]

For example, decomposing $f(x,a)=f(b,y)$ gives $x=b$ and $y=a$, whereas $x=f(x)$ has no finite-term solution and must be rejected. The point is to compute a most general unifier without expanding or repeatedly traversing shared term structure unnecessarily. Such unification supports automated deduction and logic programming.