The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. ex. Some numerals are expressed as "XNUMX".
Copyrights notice
The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. Copyrights notice
용어 재작성 시스템(TRS)의 통일 문제는 TRS에 대한 결정 문제입니다. R 그리고 두 개의 용어 s 및 t여부 s 및 t 모듈로를 통합할 수 있습니다. R. 우리는 융합 단순 TRS에 대해 문제가 결정 가능하다는 것을 보여주었습니다. 여기서 단순 TRS는 모든 다시 쓰기 규칙의 오른쪽이 기본 용어 또는 변수인 TRS를 의미합니다. 본 논문에서는 이 결과를 확장하여 합류형 반도체 TRS에 대한 통합 문제가 결정 가능함을 보여줍니다. 여기서, 세미컨스트럭터 TRS는 각 다시 쓰기 규칙의 오른쪽에 나타나는 모든 정의된 기호가 해당 기본 하위 항목에만 나타나는 것을 의미합니다.
용어 다시 쓰기 시스템, 결정 문제, 통일, 반도체
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.
부
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
부
@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},}
부
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 -