| 研究概要 |
本研究は等式論理における検証法の確立し,さらに,一般のソフトウェアを代数的手法を用いて等式論理に自動的に変換することにより,これらの検証への応用を図るものである.
今年度は、昨年度に引続き(1)検証の基礎となる完備化アルゴリズムについて考察を行った。このほかに、(2)項集合書換え系の試作、(3)結合律と交換律による商の上の書換え系の停止性について検討した。その結果、以下の知見が得られた。
(1)昨年度に与えた、項集合書換え系の完備化のための推論規則の正当性を示した。この推論規則に基づく完備化を実際に実現するためには、停止性を保証するための順序が必要になる。特殊な場合には(3)の結果を用いることができるが、一般の場合への対処は今後の課題として残った。
(2)項集合書換え系を試作し、効率的な実現を行うためには項の集合の照合操作の効率化が必須となることがわかった。
(3)項集合書換え系の追加規則が交換律と結合律のみである場合には、その停止性はその商の上の書換え系停止性に帰着できることが分かった。そこで、停止性を示すための順序を検討した。
|
