@techreport{oai:ipsj.ixsq.nii.ac.jp:00212244,
 author = {大渡, 勝己 and Ohto, Katsuki},
 issue = {5},
 month = {Aug},
 note = {数学の証明を，計算機上で再現性のあるルールの元で厳密な記述する形式的証明は，定理の妥当性を検証する有効な手段であり，Coq のような定理証明支援系は形式的証明を作成する有用なツールである．本研究では，トランプゲームの大富豪（大貧民）を簡略化した組合せゲームである「二人単貧民」における定理の証明を Coq で検証する．結果として，先行研究で明らかにされている「二人単貧民の必勝プレイヤを，手札の総数 ???? に対して O(????) 時間で判定できる」という定理の証明を Coq 上で構築し，ゲームの理論的解析における形式的証明の有効性を議論する．},
 title = {定理証明支援系Coqによる二人単貧民の定理の証明},
 year = {2021}
}