The Unification Problem for Confluent Semi-Constructor TRSs

スポンサーリンク

概要

• 論文の詳細を見る

• The unification problem for term rewriting systems (TRSs) is the problem of deciding, for a TRS R and two terms s and t, whether s and t are unifiable modulo R. We have shown that the problem is decidable for confluent simple TRSs. Here, a simple TRS means one where the right-hand side of every rewrite rule is a ground term or a variable. In this paper, we extend this result and show that the unification problem for confluent semi-constructor TRSs is decidable. Here, a semi-constructor TRS means one where all defined symbols appearing in the right-hand side of each rewrite rule occur only in its ground subterms.

• 2010-11-01

著者

• Oyamaguchi Michio

  Graduate School Of Engineering Mie University

• Mitsuhashi Ichiro

  Center For Information Technologies And Networks Mie University

• MATSUURA Kunihiro

  Graduate School of Engineering, Mie University

• Matsuura Kunihiro

  Graduate School Of Engineering Mie University

関連論文

• The Unification Problem for Confluent Semi-Constructor TRSs

スポンサーリンク