权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

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

使用证明检查器将数学工程理论形式化 (Mizar)

基本信息

批准号：
16700156
负责人：
遠藤登
金额：
$ 1.28万
依托单位：
Gifu National College of Technology
依托单位国家：
日本
项目类别：
Grant-in-Aid for Young Scientists (B)
财政年份：
2004
资助国家：
日本
起止时间：
2004 至 2006
项目状态：
已结题

项目摘要

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

Mizar systems are used to formalize existing mathematical theories, and computer proofs are used to construct models. In 2018, the theory of integration was formalized, and the preparation theorem of integration theory was insufficient. The results showed that the formalization of the theory was very fruitful, and in September 2018, the Japanese Mizar Society participated in the symposium, and domestic researchers began to study the formalization of the phase space. In this paper, we study the theory of measurable numbers in integral theory, and formalize it. The formalization of linear space for multiple correlation and the formalization of basic theory for multiple correlation are discussed. Specific research results have been obtained in the previous year, and the application range of integral theory has been studied. The pure correlation number has been changed from measurable correlation number to total correlation number. Mizar's problem has been raised in the middle of the problem, and the formalization of integral theory has been carried out in the usual way. 2 international papers and 1 domestic paper. 1 international paper on the development of the theory of integration, 1 international paper on the development of the theory of integration, 1 domestic paper on the development of the theory of integration

项目成果

期刊论文数量（10）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

Uniform Continuity of Functions on Normed Complex Linear Spaces

赋范复线性空间上函数的一致连续性

DOI：
发表时间：
2005
期刊：
Formalized Mathematics 13・1
影响因子：
0
作者：
佐々木明夫;張山昌論;亀山充隆;Noboru Endou;Yasunari Shidama;Noboru Endou;Noboru Endou;宮島啓一;鈴木康正;Noboru Endou
通讯作者：
Noboru Endou

ルベーグ積分の形式化について

关于勒贝格积分的形式化