IEICE TRANSACTIONS on Information
The Unification Problem for Confluent Semi-Constructor TRSs
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.
- Publication
- IEICE TRANSACTIONS on Information Vol.E93-D No.11 pp.2962-2978
- Publication Date
- 2010/11/01
- Publicized
- Online ISSN
- 1745-1361
- DOI
- 10.1587/transinf.E93.D.2962
- Type of Manuscript
- PAPER
- Category
- Fundamentals of Information Systems
Authors
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Ichiro MITSUHASHI, Michio OYAMAGUCHI, Kunihiro MATSUURA, "The Unification Problem for Confluent Semi-Constructor TRSs" in IEICE TRANSACTIONS on Information,
vol. E93-D, no. 11, pp. 2962-2978, November 2010, doi: 10.1587/transinf.E93.D.2962.
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.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.E93.D.2962/_p
Copy
@ARTICLE{e93-d_11_2962,
author={Ichiro MITSUHASHI, Michio OYAMAGUCHI, Kunihiro MATSUURA, },
journal={IEICE TRANSACTIONS on Information},
title={The Unification Problem for Confluent Semi-Constructor TRSs},
year={2010},
volume={E93-D},
number={11},
pages={2962-2978},
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.},
keywords={},
doi={10.1587/transinf.E93.D.2962},
ISSN={1745-1361},
month={November},}
Copy
TY - JOUR
TI - The Unification Problem for Confluent Semi-Constructor TRSs
T2 - IEICE TRANSACTIONS on Information
SP - 2962
EP - 2978
AU - Ichiro MITSUHASHI
AU - Michio OYAMAGUCHI
AU - Kunihiro MATSUURA
PY - 2010
DO - 10.1587/transinf.E93.D.2962
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E93-D
IS - 11
JA - IEICE TRANSACTIONS on Information
Y1 - November 2010
AB - 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.
ER -
English
