Please login using the form on menu list.|
It is required to login for Full-Text PDF.
The Unification Problem for Confluent Semi-Constructor TRSs
IEICE TRANSACTIONS on Information and Systems Vol.E93-D No.11 pp.2962-2978
Publication Date: 2010/11/01
Online ISSN: 1745-1361
Print ISSN: 0916-8532
Type of Manuscript: PAPER
Category: Fundamentals of Information Systems
term rewriting system,
Full Text: PDF(355.1KB)
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.