WEKO3
アイテム
CoqとIsabelle を用いたユークリッド原論の定理証明
https://doi.org/10.14990/00003612
https://doi.org/10.14990/00003612c8f67749-7118-4506-aff5-ec9982872f11
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
K03411.pdf (658.7 kB)
|
|
| Item type | 紀要論文 / Departmental Bulletin Paper(1) | |||||
|---|---|---|---|---|---|---|
| 公開日 | 2020-07-18 | |||||
| タイトル | ||||||
| タイトル | CoqとIsabelle を用いたユークリッド原論の定理証明 | |||||
| 言語 | ||||||
| 言語 | jpn | |||||
| キーワード | ||||||
| 主題 | Coq | |||||
| キーワード | ||||||
| 主題 | Isabelle/HOL | |||||
| キーワード | ||||||
| 主題 | ユークリッド原論 | |||||
| キーワード | ||||||
| 主題 | 定理証明 | |||||
| 資源タイプ | ||||||
| 資源タイプ | departmental bulletin paper | |||||
| ID登録 | ||||||
| ID登録 | 10.14990/00003612 | |||||
| ID登録タイプ | JaLC | |||||
| 著者 |
岩間, 詞也
× 岩間, 詞也× 高橋, 正 |
|||||
| 抄録 | ||||||
| 内容記述タイプ | Abstract | |||||
| 内容記述 | ソフトウェアを用いて数学の定理の証明を行うことについては，多くのソフトウェアが開発されている。本研究では，定理証明ソフトウェアCoq とIsabelle を用いてユークリッド原論の定理証明を行った。この活動によってプログラミング技術と数学の本質についての理解を深めることが支援できる。Coq およびIsabelle を用いて同じユークリッド原論の定理証明を行い, それぞれの特徴と差異を調べた。 | |||||
| 書誌情報 |
甲南大学教育学習支援センター紀要 en : Memoirs of Learning Utility Center for Konan University Students 巻 5, p. 1-16, 発行日 2020-03-23 |
|||||
| 出版者 | ||||||
| 出版者 | 甲南大学教育教職センター | |||||
| ISSN | ||||||
| 収録物識別子タイプ | ISSN | |||||
| 収録物識別子 | 2432-2334 | |||||
| 書誌レコードID | ||||||
| 収録物識別子タイプ | NCID | |||||
| 収録物識別子 | AA12776153 | |||||
| フォーマット | ||||||
| 内容記述タイプ | Other | |||||
| 内容記述 | application/pdf | |||||
| 著者版フラグ | ||||||
| 出版タイプ | VoR | |||||
| 出版タイプResource | http://purl.org/coar/version/c_970fb48d4fbd8a85 | |||||
