教授外山 芳人

助教菊池 健太郎

菊池健太郎 外山芳人

研究室紹介動画

研究活動

等式による推論は、定理自動証明、数式処理、仕様記述、関数型言語、論理型言語など計算機科学のさまざまな分野で広く使われている。等式推論にもとづいて、計算システムと証明システムを自然に接続するための基礎が書き換えシステムの理論である。書き換えシステムに基づく計算・証明パラダイムの理論的および実験的研究を進め、新しい計算・論理・代数融合システムの基礎理論の確立を目指す。

研究室Webページ

東北大学電気情報系Webページ

コンピューティング情報理論研究分野|外山教授

本分野では、書き換えシステムのさまざまな基礎的な性質、停止性、チャーチ・ロッサ性、モジュラ性などの解析を通じて、書き換えシステムの基盤理論の確立を目指している。また、書き換えシステムに基づく関数型言語を対象に、書き換えシステムの関数型プログラムの効率的な実行メカニズムと定理自動証明システムの柔軟な実行メカニズムの融合や、定理自動証明に基づくプログラムの自動検証法や自動変換法に取り組んでいる。

研究テーマ

  • 書き換えシステムの基礎理論
  • ソフトウェアの基礎研究
  • 定理自動証明法の基礎理論

等式推論による証明→書き換えシステムによる計算