|
|
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
Ichiro MITSUHASHI
Michio OYAMAGUCHI
Kunihiro MATSUURA
Publication
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
Keyword:
term rewriting system,
decision problem,
unification,
semi-constructor,
Full Text: PDF(355.1KB)
Summary:
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.
|
|
