¶Abstract

Term equations involving individual and sequence variables and sequence function symbols are studied. Function symbols can have either fixed or flexible arity. A sequence variable can be instantiated by any finite sequence of terms. A sequence function abbreviates a finite sequence of functions all having the same argument lists. It is proved that solvability of systems of equations of this form is decidable. A new unification procedure that enumerates a complete almost minimal set of solutions is presented, together with variations for special cases. The procedure terminates if the solution set is finite. Applications in various areas of artificial intelligence, symbolic computation, and programming are discussed.

¶Notes

This is the primary paper describing sequence unification, which is the unification strategy we use in stack graph path stitching.

§6.3 shows that sequence unification is unitary if “sequence variables occur only in the last argument positions in terms”.