WEKO3
アイテム
定理証明支援系Coqによる二人単貧民の定理の証明
https://ipsj.ixsq.nii.ac.jp/records/212244
https://ipsj.ixsq.nii.ac.jp/records/212244af6c67d6-3be1-467a-abb2-4240dc6a8835
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-AL21184005.pdf (896.4 kB)
|
Copyright (c) 2021 by the Institute of Electronics, Information and Communication Engineers This SIG report is only available to those in membership of the SIG.
|
|
| AL:会員：¥0, DLIB:会員：¥0 | ||
| Item type | SIG Technical Reports(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 2021-08-18 | |||||||
| タイトル | ||||||||
| タイトル | 定理証明支援系Coqによる二人単貧民の定理の証明 | |||||||
| タイトル | ||||||||
| 言語 | en | |||||||
| タイトル | Proving A Theorem of two-player TANHINMIN via Coq Proof Assistant | |||||||
| 言語 | ||||||||
| 言語 | jpn | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_18gh | |||||||
| 資源タイプ | technical report | |||||||
| 著者名 |
大渡, 勝己
× 大渡, 勝己
|
|||||||
| 著者名(英) |
Ohto, Katsuki
× Ohto, Katsuki
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | 数学の証明を，計算機上で再現性のあるルールの元で厳密な記述する形式的証明は，定理の妥当性を検証する有効な手段であり，Coq のような定理証明支援系は形式的証明を作成する有用なツールである．本研究では，トランプゲームの大富豪（大貧民）を簡略化した組合せゲームである「二人単貧民」における定理の証明を Coq で検証する．結果として，先行研究で明らかにされている「二人単貧民の必勝プレイヤを，手札の総数 ???? に対して O(????) 時間で判定できる」という定理の証明を Coq 上で構築し，ゲームの理論的解析における形式的証明の有効性を議論する． | |||||||
| 書誌レコードID | ||||||||
| 収録物識別子タイプ | NCID | |||||||
| 収録物識別子 | AN1009593X | |||||||
| 書誌情報 |
研究報告アルゴリズム（AL） 巻 2021-AL-184, 号 5, p. 1-5, 発行日 2021-08-18 |
|||||||
| ISSN | ||||||||
| 収録物識別子タイプ | ISSN | |||||||
| 収録物識別子 | 2188-8566 | |||||||
| Notice | ||||||||
| SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc. | ||||||||
| 出版者 | ||||||||
| 言語 | ja | |||||||
| 出版者 | 情報処理学会 | |||||||
