WEKO3
アイテム
等式論理系における制約解消による証明記述の枠組み
https://ipsj.ixsq.nii.ac.jp/records/132008
https://ipsj.ixsq.nii.ac.jp/records/1320082591019c-2e2e-4fde-8b84-5cbb17ee93fa
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
KJ00001345773.pdf (184.2 kB)
|
|
| Item type | National Convention(1) | |||||
|---|---|---|---|---|---|---|
| 公開日 | 1997-09-24 | |||||
| タイトル | ||||||
| タイトル | 等式論理系における制約解消による証明記述の枠組み | |||||
| タイトル | ||||||
| 言語 | en | |||||
| タイトル | A 8cheme for descril)ing proofH by c()n8traint 8olving in eqllationallogic | |||||
| 言語 | ||||||
| 言語 | jpn | |||||
| 資源タイプ | ||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_5794 | |||||
| 資源タイプ | conference paper | |||||
| 著者所属 | ||||||
| 日本ユニシス株式会社 | ||||||
| 著者所属 | ||||||
| (株) SRAソフトウェア工学研究所 | ||||||
| 著者所属(英) | ||||||
| en | ||||||
| Nihon Unisys Ltd. | ||||||
| 著者所属(英) | ||||||
| en | ||||||
| SRA Software Engineering Laboratory | ||||||
| 論文抄録 | ||||||
| 内容記述タイプ | Other | |||||
| 内容記述 | 代数仕様言語CafeOBJで記述された形式仕様の様々な性質をKnuth-Bendix完備化, 構造帰納法, 項書き換え系などの等式論理のための検証系(ツール)を使って証明するための記述の枠組みを提案する。この枠組みは制約解消の考え方を証明記述に適用した『証明=編集』パラダイムに基づいている。すなわち証明された証明記述が持つべき文書間の関係を先に"制約"という形で証明前の文書中に関係付け, その"制約"で記された関係になるように文書を変化させること("解消")によって証明を進めていくというアプローチである。その証明までの手順の概略は次のようになる。1. 文書中に仕様を記述する。2. 証明したい定理を文書中の部分間の制約として関係付ける。制約には検証系の情報も記述する。3. 制約を解消する。すなわち指定された検証系により証明を行う。4. 制約解消の結果が他の制約の部分になることも可能であり, その場合は制約の解消が繰り返し行われる。このように証明作業は入れ子になった制約を繰り返し解消することによって進められる。これにより利用者は次のような柔軟性を得ることかできる。・ある定理は複数の制約によって関係付けられることができ, また複数の定理が一つの制約によって関係付けられることもできる。・証明の順序はボトムアップでもトップダウンでもそれらの併用でも構わない。・全ての証明を一度に行うのではなく, 利用者が全体の戦略や個々の証明に関して判断を下しながら対話的に証明を行うことができる。 | |||||
| 書誌レコードID | ||||||
| 収録物識別子タイプ | NCID | |||||
| 収録物識別子 | AN00349328 | |||||
| 書誌情報 |
全国大会講演論文集 巻 第55回, 号 ソフトウェア科学・工学, p. 349-350, 発行日 1997-09-24 |
|||||
| 出版者 | ||||||
| 言語 | ja | |||||
| 出版者 | 情報処理学会 | |||||
