お問い合わせ 交通・キャンパス案内 信州大学HOME
信州大学工学部 電子情報システム工学科

師玉 康成

形式化数学記述言語と計算機検証

師玉研究室では数学定理と証明を計算機のプログラムのような形式化言語で書いてその論理的・数学的正しさを計算機で検査する研究をしていますこの検査で正しいことが確かめられた定理と証明を辞書のようにライブラリにする国際共同研究プロジェクトに海外の研究者達とともに参加しています例えばインターネットのデータ通信に使われる暗号は高度な代数学を用います現代の科学・工学技術は数学なしには成り立ちません株式の売買その他経済活動も高度な数学を利用したコンピュータシステムが主役になっています数学の研究成果の正しさを誤りを犯しやすい人手によらず計算機によって厳密に瞬時に検査できる手段は大変重要ですその使い道は定理の正しさを検査するだけではなく将棋やチェスのルールのように複数の規則に従って様々な要素や手続き機能を論理的に組み合わせて作られる工学的なシステムの開発やその動作の検査にも応用できます例えば計算機のプログラムは入力データから出力データを作る論理的な手続きを形式的な言語で表現したものであり、その動作は数学的な命題として表すことができますこれにより今までのように多くのテストデータを入力して処理結果を検査したり誤りを犯しやすい人手によって動作を一行一行解析したりといった不完全な方法ではなく計算機によって数学的に厳密に検査することができるようになりますそれが正しいと確認されればその形式的な記述をそのまま計算機プログラムに変換して使えばその動作の正しさが数学的に裏付けされたプログラムを作ることができます

研究から広がる未来

形式化数学記述言語によって、現行数学の全ての定理とその証明をライブラリ化するという壮大な目標をもった国際共同研究プロジェクトに参加しながら、形式化数学と計算機ソフトウエア開発の融合を目指しています。人手による解析や、全ての場合を尽くせるとは限らないテストデータによる試行に頼ることなく、その動作の正しさが数学的に裏付けされたプログラムを開発できる手法の構築を目指しています。

卒業後の未来像

先生は、論理的思考能力、数理的思考能力を身に付けた情報工学技術者となるように学生たちに指導しているそうです。

プロフィール

工学博士(慶応義塾大学)。1987年防衛大学校理工学研究科研究員、1990年信州大学助手、助教授を経て1995年より同大学教授。形式化数学記述言語とそれを用いた計算機検証の研究に従事。 主に、数学基礎一般の形式化と検証・ライブラリ編纂、アルゴリズムの動作検証、形式化数学記述言語を用いた論理思考訓練教材の構築に取り組む。

電子メールアドレス
研究者総覧(SOAR) 詳細を見る
オフィスアワー 部屋:3F 308室

常時 MSN Messenger こちらをID:shidama@cs.shinshu-ua.c.jpで開いていますので、随時呼び出してください。音声チャット、ビデオチャットでも結構です。MAC用のMSN Messengerはこちらから入手できます。
席を外していたり手が空かず応対できない場合がありますが、可能な限り、応対します。
ブログを設置している学生さんはこちらのURLにトラックバックを張って頂いても結構です。また、研究室のホームページ やwiki版にもお気軽にどうぞ。