2013 Fiscal Year Research-status Report
| Project/Area Number |
23500029
|
|---|
| Research Institution | Gifu National College of Technology |
|---|
Principal Investigator |
遠藤 登 岐阜工業高等専門学校, その他部局等, 准教授 (30342497)
|
|---|
| Keywords | 証明検証システム / 数理論理学 / 形式化数学 |
|---|
| Research Abstract |
証明検証システムとは、数理工学的対象をコンピュータプログラムのように形式化することで、コンピュータが認識できる対象に変換し、さらにその証明部分までも同様の形式化を行うことでコンピュータによる証明の正当性検証を可能にし、さらには既に形式化された推論データベースをもとに、新たな理論の形式化を行うシステムのことである。近年の数理科学、工学技術の急速な発展によって、より複雑な理論の展開やシステム開発がなされており、これらの正当性を一つ一つ人間が検証することは難しくなりつつあるのが現状である。そこでこのような複雑な理論の検証、あるいはシステムの解析等をコンピュータにより正確かつ迅速に行うシステムの構築が必要である。これに対し、本研究では形式化を行うシステムとしてMizar（ミザール）システムを取り上げ、このシステム上でいくつかの数学的対象（微分積分学、関数解析学）の形式化を行うことを主たる目的とし、数理論理学を基礎としたコンピュータによる自動証明、自動推論を実行するシステムの構築に向けた基礎的研究を行った。
平成２５年度はノルム空間上の微分であるFrechet微分の形式化、Riemann積分の拡張、級数論などについて形式化を行い、海外論文誌に６通の論文を発表し推論データベースへ追加した。さらに、「日本Mizar学会2013冬季総会」（信州大）、「第９回定理証明および定理証明系ミーティング」（信州大）に参加し、Mizarシステム以外の証明検証システムであるCoqの研究者との意見交換を行った。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
前年度からの継続課題である微積分の形式化については、微分に関する形式化は概ね計画通りに進行しており、今年度はFrechet微分の定義と基本命題の形式化が終了した。積分論に関しては形式化が遅れている。理由としてはMizarシステムでは無限大を扱うライブラリが存在してはいるが、関連する命題の形式化が進んでいないことが挙げられる。また、前年度の問題点であった２重級数についても、一部を形式化しライブラリへの登録を完了しているが、直積測度を形式化するにはまだ不十分な状況である。これに対しては現在関連学会へ論文を投稿しており査読中である。
今年度の新規に形式化に取り組んだ課題としては微分方程式論であり、これまでに１通の論文を関連学会に報告している。
|
| Strategy for Future Research Activity |
現在投稿中である級数論の論文採録を待ち、その後測度論の形式化を進める。またこれまでは、ライブラリ登録後の修正の手間を考慮し、測度論の形式化では明示的にσ有限の概念を組み込むことはせず、できる限り弱い条件での形式化に努めてきたが、無限大についての困難さを回避するため今後はσ有限性を付加した測度への方針転換も選択肢として形式化を試みる。また符号付き測度の形式化についても研究を行う。
また、Frechet微分および今年度新規に形式化を行った微分方程式論についても順次形式化の研究を行う予定である。
|
| Expenditure Plans for the Next FY Research Funding |
次年度使用額が発生した主たる理由としては旅費の未使用が挙げられる。これについては当初予定に比べ研究の進捗が遅れていることと、校務等により出張の機会がなかなか得られないことによる。
旅費相当分については関連学会の資料収集等に充てることを予定し、学会参加と同等の結果を得られるような対応を検討している。
|
