In this paper we show how to extend a set unification algorithm that is, an extended unification algorithm incorporating the axioms of a simple theory of sets to hyperset 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 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 that (nondeterministically) 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 nonmembership constraints. Finally, the hyperset unification problem in question is proved to be NP-complete, and the proposed algorithm to be in NP.

From Set to Hyperset Unification

DOVIER, Agostino;
1999

Abstract

In this paper we show how to extend a set unification algorithm that is, an extended unification algorithm incorporating the axioms of a simple theory of sets to hyperset 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 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 that (nondeterministically) 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 nonmembership constraints. Finally, the hyperset unification problem in question is proved to be NP-complete, and the proposed algorithm to be in NP.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11390/675357
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact