A unification algorithm for second-order monadic terms

This paper presents an algorithm that, given a finite set E of pairs of second-order monadic terms, returns a finite set U(E) of ‘substitution schemata’ such that a substitution unifies E iff it is an instance of some member of U(E). Moreover, E is unifiable precisely if U(E) is not empty. The algorithm terminates on all inputs, unlike the unification algorithms for second-order monadic terms developed by G. Huet and G. Winterstein.The substitution schemata in U(E) use expressions (called ‘parametric terms’) which represent sets of terms that differ only in how many times designated strings of (monadic) function constants follow themselves. The substitution schemata may contain unresolved ‘identity restrictions’; consequently, the members of U(E) generally do not characterize all the unifiers of E in a completely explicit way.The algorithm is particularly useful for investigating the complexity of formal proofs.