Solvable Set II. A Goal-Driven Unification Algorithm for the Blended Case. - Dovier, Agostino (Applicable algebra in engineering, communication and computing.)
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.