ORDER-SORTED UNIFICATION WITH REGULAR EXPRESSION SORTS

被引：2
|
作者：
Kutsia, Temur [1 ]
Marin, Mircea [2 ]
机构：
[1] Johannes Kepler Univ Linz, Symbol Computat Res Inst, Linz, Austria
[2] Univ Tsukuba, Grad Sch Syst & Informat Engn, Tsukuba, Ibaraki, Japan
来源：
PROCEEDINGS OF THE 21ST INTERNATIONAL CONFERENCE ON REWRITING TECHNIQUES AND APPLICATIONS (RTA'10) | 2010年 / 6卷
关键词：
Unification; sorts; regular expressions;
D O I：
10.4230/LIPIcs.RTA.2010.193
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
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.
引用
收藏
页码：193 / 207
页数：15
相关论文
共 50 条
12345