2008 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を用い、群構造を考慮した多次元分割表の性質を明らかにすることである。目的遂行のため平成20年度に行った事柄は主に次の2点である。
1. 2次元分割表の数え上げとして知られるFoulkes' lemmaについて、Isabelleを利用した証明を行い、人間の直観を利用した証明手法と計算機上での証明手法の差異を比較した。この比較結果から、直観の導入と鍵となる証明過程の挿入が証明の自動化へと繋がることが明らかになった。しかし、現状では一般的な他次元分割表の数えあげに拡張することはできず、特殊な形の分割表にのみ留まっている。
2. 国際会議(The 2^<nd> Workshop on Programming Languages for Mechanized Mathematics Systems)にて、"Comparison a human proof with a proof in Isabelle"を発表した。人間が証明を行う際に利用する直観を汎用証明システムへ導入するために必要な事柄を検討し、現状の問題点とその解決法の一端を明らかにした。
3. Isabelleを用いた証明過程を自動化するための手法を検討し、証明成功過程のデータベース作成と半自動化証明システムの構築に着手した。半自動化証明システムを構築するにあたり、事柄1での成果を利用した上でシステム設計を行った。これらの過程において、群論を利用した多次元分割表の数え上げを試みたところ、証明過程におけるdescentの概念が拡張できず、多次元分割表の数えあげに関する指標作成には至らなかった。しかし、Isabelleの持つ特性を利用した隙間のない証明過程を半自動で作成するシステムの実現により、群論によるアプローチが不足している箇所を明確にすることが可能となるものと思われる。
|
