= Ugo Montanari
{c}
<Ugo Montanari> coauthored the 1982 <unification> algorithm with <Alberto Martelli>. Their paper treats <first-order terms> as <equation>[equations] and derives an efficient implementation from simpler transformation rules, integrating the acyclicity test needed for <first-order term>[finite terms].<An Efficient Unification Algorithm by Alberto Martelli and Ugo Montanari>[abstract, §2 and Algorithm1]{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>.
Back to article page
