ORDER-SORTED UNIFICATION WITH REGULAR EXPRESSION SORTS

21st International Conference on Rewriting Techniques and Applications

TEMUR KUTSIA 1 AND MIRCEA MARIN 2 ; URL: http://www.risc.uni-linz.ac.at/people/tkutsia/

Others  :  http://drops.dagstuhl.de/opus/volltexte/2010/2653/pdf/10002.KutsiaTemur.2653.pdf
PID  :  44827

来源: CEUR

【 摘 要 】

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.