教授中野 圭介

菊池健太郎 外山芳人

研究室紹介動画

研究活動

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

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