In this paper we show how to extend a set unificationalgorithm that is, an extended unification algorithm incorporatingthe axioms of a simple theory of sets tohyperset unification (roughly speaking, to sets in which membership can form cycles).This result is obtained by enlarging the domain of terms(hence, trees) to that of graphs involvingfree as well as interpreted function symbols (namely, the set elementinsertion and the empty set), whichcan be regarded as a convenient denotation of hypersets.We present a hyperset unification algorithm that(nondeterministically) computes, for each given unification problem,a finite collection of systems of equations in solvable formwhose solutions represent a complete set of solutions for thegiven unification problem.The crucial issue of termination of the algorithmis addressed and solved by the addition of simple nonmembershipconstraints. Finally, the hyperset unification problem in questionis proved to be NP-complete, and the proposed algorithm to bein NP.
展开▼
