|
証明検証システムとは数理工学的対象を、コンピュータプログラムのように形式化することで、コンピュータが認識できる対象に変換し、さらにその証明部分までも同様の形式化を行うことでコンピュータによる証明の正当性検証を可能にし、さらには既に形式化された推論データベースをもとに、新たな理論の形式化を行うシステムのことである。近年の数理科学、工学技術の急速な発展によって、より複雑な理論の展開やシステム開発がなされており、これらの正当性を一つ一つ人間が検証することは難しくなりつつあるのが現状である。そこで、このような複雑な理論の検証、あるいはシステムの解析等をコンピュータにより正確かつ迅速に行うシステムの構築が必要とされている。この問題に対し、本研究では形式化を行うシステムとしてMizarシステムを取り上げ、このシステム上で関数解析学を中心とした周辺理論の形式化を主たる目的とし、数理論理学を基礎としたコンピュータによる自動証明、自動推論を実行するシステム構築の基礎的研究を行った。
最終年度である平成２６年度は線形汎関数の双対空間を扱い、弱収束，弱＊収束の導入及びRieszの表現定理に関するライブラリを構築し海外論文誌に３通の論文を発表し、２通の論文を投稿中である。また測度論についても２重級数、集合半群など関連する定理群の証明を行い測度の構成を行った。これらについて海外論文誌に２通の論文を発表し、２通の論文を投稿中である。
|
