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.