等式論理系における制約解消による証明記述の枠組み
スポンサーリンク
概要
- 論文の詳細を見る
代数仕様言語CafeOBJで記述された形式仕様の様々な性質をKnuth-Bendix完備化, 構造帰納法, 項書き換え系などの等式論理のための検証系(ツール)を使って証明するための記述の枠組みを提案する。この枠組みは制約解消の考え方を証明記述に適用した『証明=編集』パラダイムに基づいている。すなわち証明された証明記述が持つべき文書間の関係を先に"制約"という形で証明前の文書中に関係付け, その"制約"で記された関係になるように文書を変化させること("解消")によって証明を進めていくというアプローチである。その証明までの手順の概略は次のようになる。1. 文書中に仕様を記述する。2. 証明したい定理を文書中の部分間の制約として関係付ける。制約には検証系の情報も記述する。3. 制約を解消する。すなわち指定された検証系により証明を行う。4. 制約解消の結果が他の制約の部分になることも可能であり, その場合は制約の解消が繰り返し行われる。このように証明作業は入れ子になった制約を繰り返し解消することによって進められる。これにより利用者は次のような柔軟性を得ることかできる。・ある定理は複数の制約によって関係付けられることができ, また複数の定理が一つの制約によって関係付けられることもできる。・証明の順序はボトムアップでもトップダウンでもそれらの併用でも構わない。・全ての証明を一度に行うのではなく, 利用者が全体の戦略や個々の証明に関して判断を下しながら対話的に証明を行うことができる。
- 一般社団法人情報処理学会の論文
- 1997-09-24
著者
関連論文
- 代数仕様統合開発のための枠組と実装
- 分散オブジェクトによる抽象ドキュメントの管理方法
- 項書換え系に基づく定理証明支援環境の構築
- 代数仕様言語CafeOBJのパラメータ化機構
- 実行可能な形式仕様言語CafeOBJ(4) : CafeOBJによるZ仕様のアニメーションの枠組み
- 実行可能な形式仕様言語cafeOBJ(3) : CafeOBJによるオブジェクト指向システムの仕様記述ライブラリの記述
- 実行可能な形式仕様言語CafeOBJ(2) : Cafeシステムの核アーキテクチャ
- 実行可能な形式仕様言語CafeOBJ(1) : CafeOBJの宣言的意味論
- CafeOBJによるプロセス記述ライブラリの作成
- 等式論理系における制約解消による証明支援環境構築の試み
- ネットワーク環境におけるインタラクティブな証明支援環境
- 等式論理系における制約解消による証明記述の枠組み
- 代数的仕様記述言語CafeOBJ