From Set to Hyperset Unification
Davide Aliffi, Agostino Dovier, Gianfranco Rossi · 1999
In this paper we show how to extend a set unification algorithm -- i.e., an extended unification algorithm incorporating the axioms of a simple theory of sets -- to hyperset unification, that is to sets in which, roughly speaking, membership can form cycles. This is obtained by enlarging the domain from that of terms (hence, trees) to that of graphs involving free as well as interpreted function symbols (namely, the set element insertion and the empty set), which can be regarded as a convenient denotation of hypersets. We present a hyperset unification algorithm which (non-deterministically) computes, for each given unification problem, a finite collection of systems of equations in solvable form whose solutions represent a complete set of solutions for the given unification problem. The crucial issue of termination of the algorithm is addressed and solved by the addition of simple non-membership constraints. Finally, the hyperset unification problem dealt with is proved to be NP-comp...