外山研究室の研究紹介

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

本研究室では、書き換えシステムの基礎研究、および、プログラム自動検証やプログラム自動変換、プログラム自動生成、 定理自動証明などへの応用研究を通じて、計算の世界と証明の世界を融合した新しい計算・証明パラダイムの確立を目指しています。