Solvable Set/Hyperset Contexts: II. A Goal-Driven Unification Algorithm for the Blended Case

A universe composed by rational ground terms is characterized, both constructively and axiomatically, where the interpreted construct with which designates the operation of adjoining one element to a set, coexists with free Herbrand functors. Ordinary syntactic equivalence must be superseded by a bisimilarity relation ≈, between trees labeled over a signature, that suitably reflects the semantics of with. Membership (definable as “d∈t =_Def (t with d≈t”) meets the non-well-foundedness property characteristic of hyperset theory A goal-driven algorithm for solving the corresponding unification problem is provided, it is proved to be totally correct, and exploited to show that the problem itself is NP-complete. The results are then extended to the treatment of the operator less, designating the one-element removal operation. Applications to the automaton matching and type-finding problems are illustrated. Received: March 4, 1996; revised version: August 24, 1998