2008 年度研究成果報告書

汎用証明支援システムを用いた多次元分割表における群構造に関する研究

研究課題

研究課題/領域番号	19700269
研究種目	若手研究(B)
配分区分	補助金
研究分野	統計科学
研究機関	新潟国際情報大学
研究代表者	小野陽子新潟国際情報大学, 情報文化学部, 講師 (60339140)
研究期間 (年度)	2007 – 2008
キーワード	計算機集約的統計 / 汎用証明支援システム / 形式化手法 / 半自動証明 / 分割表
研究概要	本研究の目的は、対話型汎用証明支援システムであるIsabelleを用い、群構造を考慮した多次元分割表の性質を明らかにすることである。特に、これまでに蓄積されている群論等の証明成功過程ライブラリを知識として用い、分割表の数え上げに関する問題を群の問題として置き直した命題を作成し、この命題を計算機上でIsabelleを用いて証明を行った。この証明とは、計算機を集中的に酷使する全列挙的なものではなく、論理構造を辿るものである。