Order-Sorted Unification with Regular Expression Sorts

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.

• Type: Conference
• Year: 2010
• Where: RTA
• Authors: Temur Kutsia, Mircea Marin
• Keywords: Bottom-up Hedge Automaton, Regular Expression Sorts, RTA 2010, Theoretical Computer Science, Unification Problems