Pattern Unification with Sequence Variables and Flexible Arity Symbols
Temur Kutsia · Electronic Notes in Theoretical Computer Science · 2002
A unification procedure for a theory with individual and sequence variables, free constants, free fixed and flexible arity function symbols and patterns is described. The procedure enumerates a set of substitution/constraint pairs which constitutes the minimal complete set of unifiers.