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