1997 Fiscal Year Annual Research Report
| Project/Area Number |
07680350
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
酒井 正彦 名古屋大学, 大学院・工学研究科, 助教授 (50215597)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
外山 芳人 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (00251968)
山本 晋一郎 名古屋大学, 大学院・工学研究科, 講師 (40240098)
|
|---|
| Keywords | 項書換え系 / 合流条件 / 停止条件 / E単一化 |
|---|
| Research Abstract |
本研究は等式論理における検証法の確立し,さらに,一般のソフトウェアを代数的手法を用いて等式論理に自動的に変換することにより,これらの検証への応用を図るものである.
今年度は、昨年度に引続き(1)検証の基礎となる完備化アルゴリズムについて考察を行った。このほかに、(2)項集合書換え系の試作、(3)結合律と交換律による商の上の書換え系の停止性について検討した。その結果、以下の知見が得られた。
(1)昨年度に与えた、項集合書換え系の完備化のための推論規則の正当性を示した。この推論規則に基づく完備化を実際に実現するためには、停止性を保証するための順序が必要になる。特殊な場合には(3)の結果を用いることができるが、一般の場合への対処は今後の課題として残った。
(2)項集合書換え系を試作し、効率的な実現を行うためには項の集合の照合操作の効率化が必須となることがわかった。
(3)項集合書換え系の追加規則が交換律と結合律のみである場合には、その停止性はその商の上の書換え系停止性に帰着できることが分かった。そこで、停止性を示すための順序を検討した。
|
-
[Publications] 粕谷,酒井,山本,阿草: "項集合書換え系とその合流性" 電子情報通信学会論文誌. J80-D-I. 325-334 (1997)
-
[Publications] M. Sakai: "Left-Incompatible Term Rewriting Systems and Functional Strategy" IEICE Trans. on Information and System. E80-D. 1176-1182 (1997)
-
[Publications] M.Sakai, Y.Toyama: "Semantics and Strong Sequentiality of Priority Term Rewriting Systems" Theoretical Computer Science. (to appear). (1998)
