WEKO3
アイテム
機械学習を用いたCoq上の命題論理の自動証明
https://ipsj.ixsq.nii.ac.jp/records/185307
https://ipsj.ixsq.nii.ac.jp/records/1853073d1ede18-9284-4cc5-842b-884a131e5e02
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-WWS2018025.pdf (308.6 kB)
|
Copyright (c) 2018 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | Symposium(1) | |||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 公開日 | 2018-01-11 | |||||||||||||
| タイトル | ||||||||||||||
| タイトル | 機械学習を用いたCoq上の命題論理の自動証明 | |||||||||||||
| 言語 | ||||||||||||||
| 言語 | jpn | |||||||||||||
| キーワード | ||||||||||||||
| 主題Scheme | Other | |||||||||||||
| 主題 | 形式手法－導入支援と技術教育－ | |||||||||||||
| 資源タイプ | ||||||||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_5794 | |||||||||||||
| 資源タイプ | conference paper | |||||||||||||
| 著者所属 | ||||||||||||||
| 九州大学 | ||||||||||||||
| 著者所属 | ||||||||||||||
| 九州大学 | ||||||||||||||
| 著者所属 | ||||||||||||||
| 九州大学 | ||||||||||||||
| 著者所属 | ||||||||||||||
| 九州大学 | ||||||||||||||
| 著者名 |
金原, 雅典
× 金原, 雅典
× 佐藤, 亮介
× 鵜林, 尚靖
× 亀井, 靖高
|
|||||||||||||
| 論文抄録 | ||||||||||||||
| 内容記述タイプ | Other | |||||||||||||
| 内容記述 | プログラムの正しさを形式的に保証することは，そのプログラムに誤りがないということを確認する点で開発者にとって有用である．形式的に保証することは大変であり，自動化することでその手間を減らすことができる．そこで本研究では，機械学習を用いた命題の自動証明を試みる．その第一段階として，対象の論理を命題論理に限定して既存の機械学習によって学習 ・ 自動証明が可能かどうかを検証する．本研究での "証明" は，自然言語により書かれたものではなく，定理証明支援システム Coq 上での証明である．Coq とは，プログラムの正しさの証明や安全なプログラムを書くことに使用される証明支援システムである．学習は既存の機械学習モデルであるシーケンス変換モデルを用いて行う．これにより，学習に用いるデータセットが十分な量あれば既存の機械学習の方法でも学習可能かどうかを検証する． | |||||||||||||
| 書誌情報 |
ウィンターワークショップ2018・イン・宮島 論文集 巻 2018, p. 50-51, 発行日 2018-01-11 |
|||||||||||||
| 出版者 | ||||||||||||||
| 言語 | ja | |||||||||||||
| 出版者 | 情報処理学会 | |||||||||||||
