We extend first-order order-sorted unification by permitting regular expression sorts for variables and in the domains of function symbols. The set of basic sorts is finite. The obtained signature corresponds to a finite bottom-up hedge automaton. The unification problem in such a theory generalizes some known unification problems. Its unification type is infinitary. We give a complete unification procedure and prove decidability.
This data center is not currently reporting usage information. For information on how your repository can submit usage information, please see our documentation.
We found no citations for this text. For information on how to provide citation information, please see our documentation.