近年の計算機の発展には目覚ましいものがあり，人間には到底行えないような『計算』を簡単に行えるようになってきています．一方計算機は，少し数学的素養がある人なら簡単に行えるような『証明』すら行うことができません．これは，証明なるものを実行するには，単純な計算力だけではなく，なんらかの感性が要求されるためです．本研究室では，この『計算』と『証明』の間を繋ぐ理論，すなわち，定理自動証明の研究を行っています．また，その応用としてプログラム自動検証法の研究を行っています．この応用が可能なのは，プログラムを検証する際に必要となる様々な概念がある種の数学的な定理として定式化できるからです．さらに，これらの研究の土台となる計算モデル(項書換え系やλ算法など)の研究を行っています．

研究キーワード

詳細ページ

• 情報コースの概要
• 先輩からのメッセージ
• スタッフの紹介