2004 Fiscal Year Annual Research Report
プルーフチェッカー(Mizar)を用いた数理工学理論の形式化
| Project/Area Number |
16700156
|
|---|
| Research Institution | Gifu National College of Technology |
|---|
Principal Investigator |
遠藤 登 岐阜工業高等専門学校, 電子制御工学科, 助教授 (30342497)
|
|---|
| Keywords | 形式化理論 / ルベーグ積分 / ファジィ位相空間 |
|---|
| Research Abstract |
Mizarシステ厶用に証明検証用計算機を設置し、Mizarシステム及び現在までのライブラリを同計算機に導入した。単純関数のルベーグ積分論の定義、関連命題の証明をMizarシステ厶により行うと共にファジィ位相空間に関する基礎的研究及びMizarライブラリ検索システム構築へ向けての基礎研究を行った。以下に各研究内容について概要を述べる。
ルベーグ積分論に関しては、現在までに導入が終了しているルベーグ測度、可測関数の定義、定理をもとに単純関数をドメインとレンジの組として再定義を行うことで単純関数のルベーグ積分を定義した。現在は可積分関数の定義と関連命題の証明を行っている。またこの結果を元に関連学会へ1通の学術報告を行った。
ファジィ理論に関しては、Mizar開発者の一人であるポーランド国Bialystok大学のGrzegorz Bancerek氏とミーティングを行い、ファジィ位相空間及びファジィラティスに関する情報交換を行った。その際、形式化における幾つかの問題点について有用な指摘を頂いた。
Mizarライブラリ検証システム構築については、まだ基礎研究の段階であり、証明ファイル(命題とその証明を記述したファイル)から得られる検証結果に対する中間ファイルを解析しているところである。また、これについてもGrzegorz Bancerek氏に有益な情報を頂いた。
|
Research Products
(1 results)
