WEKO3
-
RootNode
アイテム
定理証明支援系Coqにおける手続き的証明から宣言的証明への変換
https://uec.repo.nii.ac.jp/records/8708
https://uec.repo.nii.ac.jp/records/8708cfb7db1b-c777-4c94-9f42-c250edd56032
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
1631156 (1.3 MB)
|
|
| Item type | 学位論文 / Thesis or Dissertation(1) | |||||||||
|---|---|---|---|---|---|---|---|---|---|---|
| 公開日 | 2018-04-13 | |||||||||
| タイトル | ||||||||||
| タイトル | 定理証明支援系Coqにおける手続き的証明から宣言的証明への変換 | |||||||||
| 言語 | ja | |||||||||
| 言語 | ||||||||||
| 言語 | jpn | |||||||||
| 資源タイプ | ||||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_46ec | |||||||||
| 資源タイプ | thesis | |||||||||
| 著者 |
山田, 伊織
× 山田, 伊織
|
|||||||||
| 抄録 | ||||||||||
| 内容記述タイプ | Abstract | |||||||||
| 内容記述 | 定理証明支援系Coqにおける証明は、一般に手続き的証明と呼ばれる形式で記述される。これは対話的証明を前提としており、自然言語による証明記述と大きく異なるため、可読性が高いものではない。この問題を解決するためにCoq用宣言的証明言語C-zarが開発された。宣言的証明は可読性が高く、また外部ツールを導入し易い。しかし、C-zar は手続き的証明に対して記述量が多い上に柔軟性が低く、Coq ユーザに受け入れられなかった。本研究では、Coq の手続き的証明からC-zarの証明を生成することで、両者間の橋渡しを行う。一般に手続き的証明から宣言的証明への変換手法としては、証明項や証明木のような中間表現を経由する方法が考えられ、既に定理証明支援系Matitaでは証明項を経由する手続き的証明から宣言的証明への変換が存在する。しかし、中間表現は元の証明と比べて詳細かつ巨大になり、元の手続き的証明1ステップに対して数百ステップの宣言的証明が生成されてしまう場合もある。一方で、C-zar は手続き的証明で用いられるタクティックと呼ばれるコマンドを利用することができ、これによって手続き的証明の1ステップは、多くの場合C-zarの数ステップと対応させることができる。本研究では、元の手続き的証明と証明項の両方を用いて変換を行うことで、元の証明に近い粒度の宣言的証明の生成を実現する。 | |||||||||
| 学位名 | ||||||||||
| 学位名 | 修士 | |||||||||
| 学位授与機関 | ||||||||||
| 学位授与機関名 | 電気通信大学 | |||||||||
| 学位授与年度 | ||||||||||
| 内容記述タイプ | Other | |||||||||
| 内容記述 | 2017 | |||||||||
| 学位授与年月日 | ||||||||||
| 学位授与年月日 | 2018-03-23 | |||||||||
| 著者版フラグ | ||||||||||
| 出版タイプ | AM | |||||||||
| 出版タイプResource | http://purl.org/coar/version/c_ab4af688f83e57aa | |||||||||
| 専攻 | ||||||||||
| 情報理工学研究科 | ||||||||||
| 専攻 | ||||||||||
| 情報・ネットワーク工学専攻 | ||||||||||
