Order-Sorted Unification with Regular Expression Sorts

Authors Temur Kutsia, Mircea Marin



PDF
Thumbnail PDF

File

LIPIcs.RTA.2010.193.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)
https://doi.org/10.4230/LIPIcs.RTA.2010.193

Abstract

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

Metrics

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

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail