A-011 An Extension of E-overlapping Notion in Term Rewriting Systems and its Applications

概要

論文の詳細を見る
For nonlinear term rewriting systems(TRSs), the notion of E-overlapping extending that of usual overlapping has been proposed and some sufficient conditions for ensuring the decidability of some decision problems have been obtained by using this notion. Here, TRS R is E-overlapping if there exist two rewrite rules α→β and α'→β' in R such that α and some subterm of α' are unifiable modulo rewrite rules. In this paper, we introduce a new notion called LR-E-overlapping which is extending that of E-overlapping. Here, TRS R is LR-E-overlapping if there exist two rules α→β and α'→β' in R such that a or β is unifiable to some subterm of α' or β' modulo rewrite rules. Using this notion we give some new sufficient conditions for ensuring the decidability of some decision problems such as Church-Rosser property and E-unification for subclasses of nonlinear TRSs.
FIT(電子情報通信学会・情報処理学会)推進委員会の論文
2008-08-20