| 研究課題/領域番号 |
23500029
|
|---|
| 研究機関 | 長野工業高等専門学校 |
|---|
研究代表者 |
遠藤 登 長野工業高等専門学校, 電子制御工学科, 准教授 (30342497)
|
|---|
| 研究期間 (年度) |
2011-04-28 – 2015-03-31
|
| キーワード | 証明検証システム / 数理論理学 / 形式化数学 |
|---|
| 研究概要 |
形式化数学とは、数学的対象をコンピュータプログラムのように形式化することでコンピュータが認識できる対象に変換し、さらにその証明部分までも同様の形式化を行うことでコンピュータにより証明の正当性の検証を実現し、理論全体が形式化された推論データベースを構築することである。近年の数理科学、工学技術の急速な発展によって、より複雑な理論の展開やシステム開発がなされており、これらの正当性を一つ一つ人間が検証することは難しくなりつつあるのが現状である。そこでこのような複雑な理論の検証、あるいはシステムの解析等をコンピュータにより正確かつ迅速に行うシステムの構築が必要になると考えられる。このような要求に対し、本研究では形式化を行うシステムとしてMizar（ミザール）システムを取り上げ、その上でいくつかの数学的対象（微分積分、関数空間）の形式化を行うことを主たる目的とし、数理論理学を基礎としたコンピュータによる自動証明、自動推論を実行するシステムの確立に向けた基礎的研究を行った。平成２３年度はルベーグ式積分論の形式化及び偏微分の形式化を中心とした微分積分学の形式化を目指し研究を行った。結果、高階の偏微分に関する形式化を行い、海外論文誌に１通の論文を発表、合わせて推論データベースへ追加した。またｎ次元実数空間上のルベーグ測度について形式化を行ったが、従来の推論データベースでは対応できない点があり、追加のデータベースを構築している。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
偏微分に関する形式化は概ね計画通りにするんでいるものの、直積測度の形式化が遅れている。具体的には直積測度の構成として、集合上のsemi-algebraを起点にpre測度を構成し測度への拡張を試みた。しかしながら、その過程において２重級数の収束に関する各種定理が必要となるが、Ｍｉｚａｒシステムにはこれらの定理が組み込まれていないことが原因である。そのため平成２３年度は偏微分と２重級数さらに直積測度の形式化を主に研究を行い、可積分空間、ソボレフ空間の理論までは形式化を進めることができなかった。
|
| 今後の研究の推進方策 |
早急に２重級数の問題を解決し、直積測度およびｎ次ルベーグ測度の形式化を進める。さらに２重級数の形式化に関連しPringsheim型の収束理論の形式化について考察し、Orlitz空間への一般化についても形式化の可能性を探る。またフビニの定理等、直積空間上のルベーグ式積分論の重要な定理群の形式化、ソボレフ空間の形式化を推進する。
|
| 次年度の研究費の使用計画 |
次年度における研究費は主として旅費を計上している。国内旅費として資料収集、研究打ち合わせ、成果発表を計画し、外国旅費として国際会議での成果発表を計画している。その他は参考図書等の消耗品である。なお、次年度への研究費の繰り越しについては、今年度東北で行われる予定であった学会が震災の影響で開催されなかった等の事由による旅費の繰り越し分が大半である。
|
