A unification algorithm for second-order monadic terms (Q1109019)

The paper presents an algorithm for simultaneous unification of finite sets E of pairs of second-order terms which contain no function constants with arity greater than or equal to two. In fact the algorithm is not only a decision procedure. It generates a set \({\mathcal U}(E)\) of substitution schemata such that: \({\mathcal U}(E)=\emptyset\) iff E is not unifiable and for all substitutions \(\sigma\), \(\sigma\) unifies E iff \(\sigma\) is an instance of some member of \({\mathcal U}(E)\). It has strong similarities with Huet's algorithm for second order monadic terms except that it works with ``parameterized terms'' and ``parameterized substitutions''. In this way it terminates on all inputs and \({\mathcal U}(E)\) is finite in all cases. However for some unifiers only an ``initial segment'' of the unifier is characterized explicitly in \({\mathcal U}(E)\). A preliminary version of the algorithm has appeared in the author's Ph. D. thesis and it has proven to be very useful for investigating some proof complexity problems. The paper is self- contained. Not only are the procedures provided but also the necessary proofs and definitions.