プルーフチェッカー(Mizar)を用いた数理工学理論の形式化

点击翻译按钮获取中文摘要

Mizarシステムを用いて既存の数理工学理論の形式化を行い、計算機証明検証システムの構築を目指し研究を行った。平成18年度は特にファジィ理論とルベーグ積分論に焦点を絞って形式化を行う予定であったが,予想以上にルベーグ積分論を構築するための予備定理が不足しており,これらの形式化に多くの労力を費やした。結果として,ファジィ理論の形式化については十分な成果を挙げることが出来なかったが,平成18年9月に開催された日本Mizar学会秋季総会に参加の折,国内研究者より多くの有益な助言を頂き,これをもとに現在,ファジィ位相空間の形式化の実現に向け研究を行っている。ルベーグ積分論については1変数可測関数の理論が本研究により,ほぼ形式化された。また,これに関連して多次元のノルム線形空間の形式化を行い,多変数関数の積分論に対する基礎理論の形式化を行った。具体的な研究実績として,前年度までに得られたルベーグ積分の適用範囲を,単純関数から可測関数まで拡張すると共に,Mizarシステムが内包していた実数と拡張実数の互換性について問題提起を行い,通常の実数値を取る可測関数のルベーグ積分論の形式化を行った。さらに,これらの結果を纏め,2件の国際論文誌と1件の国内発表を行った。関連した実績として,リーマン積分論の精微化を行い1件の国際論文誌に発表,実ノルム空間を中心とした形式化を行い1件の国際論文誌と1件の国内発表を行った。