Optimal Unification of Bounded Simple Set Terms

This paper is concerned with the problem of unification of bounded simple set terms, i.e., terms of the form {e1,...,en}, where ei is a constant or a variable. Such simplified types of set terms are used in many application areas such as databases and logic programming. We present a precise formalization of the problem through the identification of a hierarchy of subproblems and establish the exact output size of the problem and its special cases by providing formulas for determining the number of unifiers. We present also the first two phases on an optimal (five phases) unification algorithm.