HOME >  組織・研究分野 >  外山研究室

組織・研究分野

情報論理学 [外山] 研究室

教員・職員

photo 教授 外山 芳人 (電気通信研究所)
助教 菊池 健太郎

等式による推論は、定理自動証明、数式処理、仕様記述、関数型言語、論理型言語など計算機科学のさまざまな分野で広く使われている。これらの等式推論をリダクションによって効率的に実現するための基礎が書き換えシステムの理論である。

本研究室では、書き換えシステムの停止性、チャーチ・ロッサ性、モジュラ性などの解析を通じて、新しい計算・論理・代数融合システムの基礎理論の確立を目指す。また、書き換えシステムに基づく関数型言語を対象に、与えられたプログラムを効率の良い等価なプログラムに自動変換したり、与えられた仕様からプログラムを自動合成するための基礎研究を行っている。さらに、高階書き換えシステム、プログラムの帰納的性質の自動証明法、関数・論理型言語の効率的な実行メカニズムと定理自動証明システムの柔軟な実行メカニズムの融合など、書き換えシステムに基づく計算・証明パラダイムの理論的および実験的研究を進めている。

研究テーマ

  1. 書き換えシステムの基礎理論
  2. プログラム言語の基礎研究
  3. 定理自動証明システムの研究
東北大学 電気・情報系
〒980-8579 仙台市青葉区荒巻字青葉 6-6-05
TEL : 022-795-7186(教務係)
Email :

mail