2007 Fiscal Year Annual Research Report
汎用証明支援システムを用いた多次元分割表における群構造に関する研究
| Project/Area Number |
19700269
|
|---|
| Research Institution | Niigata University of International and Information Studies |
|---|
Principal Investigator |
小野 陽子 Niigata University of International and Information Studies, 情報文化学部, 講師 (60339140)
|
|---|
| Keywords | Isabelle / 分割表 / 群論 / 数え上げ |
|---|
| Research Abstract |
本研究の目的は、対話型汎用証明支援システムであるIsabelleとプルーフチェッカであるMizarを用い、群構造を考慮した多次元分割表の性質を明らかにすることである。具体的には次の2点が主眼である。第一に、Isabelle・Mizarにおいて、これまでに申請者が蓄積した群論の証明成功過程ライブラリを知識として用い、多次元分割表の持つ群構造の存在を明示化する。第二に、多次元分割表の数え上げに関する問題を群の問題として置き直し命題を作成する。この命題を計算機上でIsabelleもしくはMizarを用いて証明を行う。この証明とは、計算機を集中的に酷使する全列挙的なものではなく、論理構造を辿るものである。
平成19年度に行った事柄は次の3点である。
1.国際会議(ISI 56th)にて"On Comparison of p-values for Contingency Tables between MCMC and Direct Sampling"を発表した。数値実験を通し、どのくらいの差が生じるかという事柄に着目し、各々の手法による数値結果の比較を行った。
2.国際会議(Computers Scientific Discovery4)にて"A Proof by Automated Reasoning"を発表した。数学の証明手法がIsabelleと人間ではどのように異なるのかということを明らかにし、自動証明に必要な事柄について検討した。
3.Isabelleと人間が理解する数学テキストにおける証明との差異の洗い出しと、証明の鍵となる事柄を半自動的に発見するための基礎的研究を行った。群論の基礎的な証明をあらかじめ用意しなければ、Isabelleを用いることができないため、基本的な部品とも言うべき証明のパーツを作成した。証明に必要な鍵を与えることの必要性について検討中である。
|
Research Products
(2 results)
