本研究では計算機検証システムMizarに対する推論データベースの拡充について研究を行った。数学における各種の理論を形式化することで、将来的には自動証明、自動推論の実現を目的とし、人工知能の実現へ向けた一つのアプローチである。本研究の成果は主に測度論、微分積分学、関数解析学の3つの分野にまたがる。測度論では具体的な測度の構成について形式化を行った。微分積分学については高階偏微分、微分方程式の形式化を行った。関数解析学では可積分関数の空間、共役空間の形式化を行った。これらの研究成果について関連学会に13本の論文を発表した。
|