|
Mizarシステ厶用に証明検証用計算機を設置し、Mizarシステム及び現在までのライブラリを同計算機に導入した。単純関数のルベーグ積分論の定義、関連命題の証明をMizarシステ厶により行うと共にファジィ位相空間に関する基礎的研究及びMizarライブラリ検索システム構築へ向けての基礎研究を行った。以下に各研究内容について概要を述べる。
ルベーグ積分論に関しては、現在までに導入が終了しているルベーグ測度、可測関数の定義、定理をもとに単純関数をドメインとレンジの組として再定義を行うことで単純関数のルベーグ積分を定義した。現在は可積分関数の定義と関連命題の証明を行っている。またこの結果を元に関連学会へ1通の学術報告を行った。
ファジィ理論に関しては、Mizar開発者の一人であるポーランド国Bialystok大学のGrzegorz Bancerek氏とミーティングを行い、ファジィ位相空間及びファジィラティスに関する情報交換を行った。その際、形式化における幾つかの問題点について有用な指摘を頂いた。
Mizarライブラリ検証システム構築については、まだ基礎研究の段階であり、証明ファイル(命題とその証明を記述したファイル)から得られる検証結果に対する中間ファイルを解析しているところである。また、これについてもGrzegorz Bancerek氏に有益な情報を頂いた。
|
