|
(1) 単項帰納的定義と暗黙存在のある分離論理のエンテイルメントの決定可能 性を証明した。この体系は、有界木幅分離論理 SLRDbtw から、暗黙存在変数を追加し、帰納的定義を単項に制限することにより得られる。(2) 単項帰納的定義をもつ記号ヒープのエンテイルメント判定器を実装した。効率的実装のためのアイデアとして、木のノード間の同値関係に関する最適化を説明した。(3) 相互再帰手続きをもつポインタープログラムにホーア論理と分離論理の拡張した体系の完全性を証明した。(4) プレスバーガー算術と帰納的定義をもつ分離論理における記号ヒープの充足可能性問題を解いた。
|
