2008 Fiscal Year Final Research Report

Group structure of n-way contingency tables with a proof assistant system

Research Project

Project/Area Number	19700269
Research Category	Grant-in-Aid for Young Scientists (B)
Allocation Type	Single-year Grants
Research Field	Statistical science
Research Institution	Niigata University of International and Information Studies
Principal Investigator	ONO Yoko Niigata University of International and Information Studies, 情報文化学部, 講師 (60339140)
Project Period (FY)	2007 – 2008
Keywords	計算機集約的統計 / 汎用証明支援システム / 形式化手法 / 半自動証明 / 分割表
Research Abstract	本研究の目的は、対話型汎用証明支援システムであるIsabelleを用い、群構造を考慮した多次元分割表の性質を明らかにすることである。特に、これまでに蓄積されている群論等の証明成功過程ライブラリを知識として用い、分割表の数え上げに関する問題を群の問題として置き直した命題を作成し、この命題を計算機上でIsabelleを用いて証明を行った。この証明とは、計算機を集中的に酷使する全列挙的なものではなく、論理構造を辿るものである。