2012 Fiscal Year Research-status Report
| Project/Area Number |
23500029
|
|---|
| Research Institution | Gifu National College of Technology |
|---|
Principal Investigator |
遠藤 登 岐阜工業高等専門学校, その他部局等, 准教授 (30342497)
|
|---|
| Keywords | 証明検証システム / 数理論理学 / 形式化数学 |
|---|
| Research Abstract |
証明検証システムとは、数学的対象をコンピュータプログラムのように形式化することで、コンピュータが認識できる対象に変換し、さらにその証明部分までも同様の形式化を行うことでコンピュータにより証明の正当性の検証を実現し、理論全体が形式化された推論データベースをもとに、新たな理論の形式化を行うシステムのことである。近年の数理科学、工学技術の急速な発展によって、より複雑な理論の展開やシステム開発がなされており、これらの正当性を一つ一つ人間が検証することは難しくなりつつあるのが現状である。そこでこのような複雑な理論の検証、あるいはシステムの解析等をコンピュータにより正確かつ迅速に行うシステムの構築が必要になると考えられる。このような要求に対し、本研究では形式化を行うシステムとしてMizar（ミザール）システムを取り上げ、その上でいくつかの数学的対象（微分積分学、関数解析学）の形式化を行うことを主たる目的とし、数理論理学を基礎としたコンピュータによる自動証明、自動推論を実行するシステムの確立に向けた基礎的研究を行った。
平成２４年度は複素数値ルベーグ可積分関数の空間を取り上げ形式化を行い、海外論文誌に１通の論文を発表、合わせて推論データベースへ追加した。またn次元実数空間上のルベーグ測度に関連した形式化について論文を投稿中であり、バナッハ空間上に値をとる関数の積分に関連した形式化についても研究の進展が得られている。さらに、「第８回定理証明および定理証明系ミーティング」（千葉大）に参加しMizarシステム以外の証明検証システムであるCoqの研究者との交流を行った。
|
| Current Status of Research Progress |
Current Status of Research Progress
4: Progress in research has been delayed.
Reason
偏微分に関する形式化は概ね計画通りにするんでいるが、ルベーグ測度論の形式化が遅れている。昨年度の課題にあった２重級数については一通り基礎的な研究を終了し論文として投稿しているが、いまだ採録には至っていない。そのため２重級数について正式なライブラリとして登録ができていないことが研究が停滞している大きな原因である。また、他の要因としてシステムのライブラリ仕様の変更が挙げられる。Mizarシステムではライブラリの更新に伴いライブラリ引用に関する内部処理がいくらか変更されるため、以前の仕様で作成した証明を受け付けないことが起きる。特に平成２４年度はライブラリのメジャーアップデートとともに大きな仕様変更が行われ、従来の結果を新仕様のライブラリに対応させなければならなかったことも原因の一つである。
|
| Strategy for Future Research Activity |
２重級数の形式化に関する論文が採録され、ライブラリに登録されることを第一とし、その後測度論の形式化を順次進め、各種関数空間の形式化に着手する。さらに今年度の研究成果により微分方程式論の形式化への足掛かりを得たため、来年度は微分方程式論の形式化についても研究を行う予定である。
|
| Expenditure Plans for the Next FY Research Funding |
次年度における研究費は主として旅費および消耗品費を計上している。旅費は資料収集、研究打ち合わせ、成果発表のための国内旅費である。消耗品費については参考図書等の消耗品である。
|
Research Products
(1 results)
