Document Open Access Logo

Order-Sorted Unification with Regular Expression Sorts

Authors Temur Kutsia, Mircea Marin

Thumbnail PDF


  • Filesize: 185 kB
  • 16 pages

Document Identifiers

Author Details

Temur Kutsia
Mircea Marin

Cite AsGet BibTex

Temur Kutsia and Mircea Marin. Order-Sorted Unification with Regular Expression Sorts. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 193-208, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2010)


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.
  • Unification
  • sorts
  • regular expression


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail