1996 Fiscal Year Annual Research Report
| Project/Area Number |
07680350
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
酒井 正彦 北陸先端科学技術大学院大学, 情報科学研究科, 助教授 (50215597)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
山本 晋一郎 名古屋大学, 工学部, 講師 (40240098)
外山 芳人 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (00251968)
|
|---|
| Keywords | 項書換え系 / 合流条件 / 停止条件 / E単一化 |
|---|
| Research Abstract |
本研究は等式論理における検証法の確立し,さらに,一般のソフトウェアを代数的手法を用いて等式論理に自動的に変換することにより,これらの検証への応用を図るものである.
今年度は,(1)停止的な項集合書換え系の非線形規則における合流条件性質の解析,ならびに,(2)検証の基礎となる完備化アルゴリズムについて考察を行なった.その結果,以下の知見が得られた.
(1)危険対の概念を集合に拡張し,危険対のみの合流性をを示すことによる停止的な項集合書換え系が非線形規則を持つ場合の合流条件を与えた.しかしがら,この照明に必要な一つの補題が未解決な問題として残った.
(2)項集合書換え系の完備化のための推論規則を与え,その正当性を検討した.
また,書換え系の効率的実現のための試験システムを作成し.その高速性を実証した.これにより,項集合書換え系の効率的実現の基礎が与えられた.
|
Research Products
(6 results)
-
[Publications] 高橋宜孝: "条件付き項書換え系の合流性について" 電子情報通信学会論文誌. J79-D-l011. 897-902 (1996)
-
[Publications] 粕谷英人: "項集合書換え系とその合流性" 電子情報通信学会論文誌. 掲載予定.
-
[Publications] Masahiko Sakai: "Semantics and Strong Sequentiality of Prioority Term Rewriting Systems" Proc. on Rewriting Techniques and AppricatIon,LNCS. 1103. 377-391 (1996)
-
[Publications] Keiichiro Kusakari: "Church-Rosser Property of Finite Ranked Terms of Non-linear Term Rewriting Systems" LAシンポジウム論文集. 160-165 (1996)
-
[Publications] Takashi Nagaya: "Index Reduction of Overlapping Strong Sequential Systems" Tech. Rep,of IEICE. COMP96・32. 39-48 (1996)
-
[Publications] Munehiro Iwami: "An Improved Recursive Decomposition Ordering for Higher-order Rewrite Systems" Tech Rep. of IEICF. COMP96・73. 17-24 (1997)
