工学部 研究紹介2018

53/148

製品設計や仕様書の正しさをチェックする（ものづくりへの応用）証明問題のインタラククティブ教材（教育への応用）(数学以外への形式化数学の応用例) 師⽟研究室研究から広がる未来卒業後の未来像形式化数学記述言語によって、現行数学の全ての定理とその証明をライブラリ化するという壮大な目標をもった国際共同研究プロジェクトに参加しながら、形式化数学と計算機ソフトウエア開発の融合を目指しています。人手による解析や、全ての場合を尽くせるとは限らないテストデータによる試行に頼ることなく、その動作の正しさが数学的に裏付けされたプログラムを開発できる手法の構築を目指しています。学生たちには、論理的思考能力、数理的思考能力を身に付けた情報工学技術者となるように指導しています。師玉康成教授工学博士(慶応義塾大学）1987年防衛大学校理工学研究科研究員、1990年信州大学助手、助教授を経て1995年より同大学教授形式化数学記述言語とそれを用いた計算機検証の研究に従事。主に•数学基礎一般の形式化と検証･ライブラリ編纂•アルゴリズムの動作検証•形式化数学記述言語を用いた論理思考訓練教材の構築に取り組む。師玉研究室では数学定理と証明を計算機のプログラムのような形式化言語で書いてその論理的･数学的正しさを計算機で検査する研究をしています。この検査で正しいことが確かめられた定理と証明を辞書のようにライブラリにする国際共同研究プロジェクトに海外の研究者達とともに参加しています。例えばインターネットのデータ通信に使われる暗号は高度な代数学を用います。現代の科学･工学技術は数学なしには成り立ちません。株式の売買その他、経済活動も高度な数学を利用したコンピュータシステムが主役になっています。数学の研究成果の正しさを、誤りを犯しやすい人手によらず、計算機によって、厳密に、瞬時に検査できる手段は大変重要です。その使い道は定理の正しさを検査するだけではなく、将棋やチェスのルールのように複数の規則に従って、様々な要素や手続き、機能を論理的に組み合わせて作られる工学的なシステムの開発やその動作の検査にも応用できます。例えば計算機のプログラムは入力データから出力データを作る論理的な手続きを形式的な言語で表現したものであり、その動作は数学的な命題として表すことができます。これにより、今までのように、多くのテストデータを入力して処理結果を検査したり、誤りを犯しやすい人手によって動作を一行一行解析したりといった、不完全な方法ではなく計算機によって数学的に厳密に検査することができるようになります。それが正しいと確認されれば、その形式的な記述をそのまま、計算機プログラムに変換して使えば、その動作の正しさが数学的に裏付けされたプログラムを作ることができます。形式化数学記述⾔語と計算機検証電⼦情報システム⼯学科研究シーズ共同研究・外部資⾦獲得実績社会貢献実績研究キーワード形式⼿法・定理証明⽀援系・数理論理【先生の学問へのきっかけ】学部１年生の時に偶々、図書館で形式化数学と基礎数学の教科書シリーズを手に取ったがきっかけです。数学の定理や証明を全て記号列で表してその正しさを機械的に厳密にチェックすることができるという事が新鮮な驚きでした。それから図書館に籠ってその教科書や関連の文献を夢中になって読み漁る日々を続iけたことが研究活動の始まりです。入学した学部は工学部で専門が違っていたので全くの独学で「下手の横好き」が今日まで続いています。9０年代には計算機科学者達によってそのような機械的な検証を計算機システムで実現しょうとするQ.E.Dマニュフェストが提唱され、各国の計算機科学者、数理科学者がその実現に向けて研究活動を行っています。•定理証明支援系の応用計算機プログラムの動作検証アルゴリズムの形式化定理証明の形式化•定理証明支援系を用いた論理思考訓練e-Learning教材の開発•科研費、基盤（B）、ＭＩＺＡＲ数学ライブラリの構築と⼤学数学向け⾼度遠隔教育⽤コンテンツ開発、(代表)、平成22年-25年•科研費、基盤（B）、信州大学インターネット大学院におけるマルチメディア利用CAIシステムの高度化研究、(代表)、平成15年-18年•JSPSPostdoctoralFellowshipforForeignResearchersSupervisor,2000-2002AMU会員インターネット大学院の運営定理証明支援系MizarによるHUFFMAN符号木の構成アルゴリズムの形式化記述コード（一部抜粋）51