这是indexloc提供的服务,不要输入任何密码
IEICE Transactions on Information and Systems
Online ISSN : 1745-1361
Print ISSN : 0916-8532
Regular Section
The Unification Problem for Confluent Semi-Constructor TRSs
Ichiro MITSUHASHIMichio OYAMAGUCHIKunihiro MATSUURA
Author information
JOURNAL FREE ACCESS

2010 Volume E93.D Issue 11 Pages 2962-2978

Details
Abstract
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.
Content from these authors
© 2010 The Institute of Electronics, Information and Communication Engineers
Previous article Next article
feedback
Top