WEKO3
アイテム
条件付き項書換え系の健全性と完全性
https://ipsj.ixsq.nii.ac.jp/records/30289
https://ipsj.ixsq.nii.ac.jp/records/30289bd46d190-2257-45c4-b865-61c67882e556
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-PRO96009004.pdf (406.3 kB)
|
Copyright (c) 1996 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | SIG Technical Reports(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 1996-09-03 | |||||||
| タイトル | ||||||||
| タイトル | 条件付き項書換え系の健全性と完全性 | |||||||
| タイトル | ||||||||
| 言語 | en | |||||||
| タイトル | Soundness and Completeness of Conditional Term Rewriting Systems | |||||||
| 言語 | ||||||||
| 言語 | jpn | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_18gh | |||||||
| 資源タイプ | technical report | |||||||
| 著者所属 | ||||||||
| 筑波大学博士課程工学研究科 | ||||||||
| 著者所属 | ||||||||
| 筑波大学電子情報工学系 | ||||||||
| 著者所属 | ||||||||
| 筑波大学電子情報工学系 | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Doctoral Programin Engineering, University of Tsukuba | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Institute of Information Sciences and Electronics, University of Tsukuba | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Institute of Information Sciences and Electronics, University of Tsukuba | ||||||||
| 著者名 |
山田, 俊行
× 山田, 俊行
|
|||||||
| 著者名(英) |
Toshiyuki, Yamada
× Toshiyuki, Yamada
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | 条件付き等式系εに対する条件付き項書換え系(TR)が健全かつ完全であるととは，εのすべてのモデルにおける等価性（=M_ε）とεのもとで等しいことの証明可能性（〓）とが一致することを意味する．本論文では，oriented CTRSの完全性に関するAvenhausとLoria?Saenzの主張を反駁し，絶対不可約性(bsolute irreduciblit)がoriented CTRSの完全性を保証するのに不適切であることを指摘する．この性質に代え，安定性という性質を導入することにより，oriented CTRSが完全であるための新たな十分条件を提示する．Suzukiらにより提案された，階層合流性をもっOriented CTRSが健全かつ完全であることは，本論文の結果により明らかになる． | |||||||
| 論文抄録(英) | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | Soundness and completeness of a conditional term rewriting system (CTRS) for a conditional equational system ε means the equivalence of equality in all models (=M_ε) and the provability by equational reasoning (〓). In this paper a claim of Avenhaus and Loria-Saenz about the completeness of oriented CTRSs is refuted. We point out that absolute irreduciblity is an insufficient for ensuring the completeness of oriented CTRSs. As a substitute, we introduce stability and provide a new sufficient condition for completeness of oriented CTRSs. The level-confluent oriented CTRSs proposed by Suzuki et al. turn out to be sound and complete by using the result in this paper. | |||||||
| 書誌レコードID | ||||||||
| 収録物識別子タイプ | NCID | |||||||
| 収録物識別子 | AN10485570 | |||||||
| 書誌情報 |
情報処理学会研究報告プログラミング（PRO） 巻 1996, 号 83(1996-PRO-009), p. 19-24, 発行日 1996-09-03 |
|||||||
| Notice | ||||||||
| SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc. | ||||||||
| 出版者 | ||||||||
| 言語 | ja | |||||||
| 出版者 | 情報処理学会 | |||||||
