| 研究概要 |
本研究は等式論理における検証法の確立し,さらに,一般のソフトウェアを代数的手法を用いて等式論理に自動的に変換することにより,これらの検証への応用を図るものである.
今年度は,(1)停止的な項集合書換え系の非線形規則における合流条件性質の解析,ならびに,(2)検証の基礎となる完備化アルゴリズムについて考察を行なった.その結果,以下の知見が得られた.
(1)危険対の概念を集合に拡張し,危険対のみの合流性をを示すことによる停止的な項集合書換え系が非線形規則を持つ場合の合流条件を与えた.しかしがら,この照明に必要な一つの補題が未解決な問題として残った.
(2)項集合書換え系の完備化のための推論規則を与え,その正当性を検討した.
また,書換え系の効率的実現のための試験システムを作成し.その高速性を実証した.これにより,項集合書換え系の効率的実現の基礎が与えられた.
|
