|
等式による推論は、定理自動証明、数式処理、代数的仕様記述、関数型言語、論理型言語など、計算機科学のさまざまな分野で広く使われている。これらの等式推論をリダクションによって効率的に実現するための基礎が書き換えシステムの理論である。
本研究室では、書き換えシステムの停止性、チャーチ・ロッサ性、モジュラ性などの理論解析を通して、新しい計算・論理・代数融合システムの基礎理論の確立を目指す。また、書き換えシステムに基づく関数型言語を対象に、与えられたプログラムを効率の良い等価なプログラムに自動変換したり、プログラムが与えられた仕様を満たすかどうかを検証するための基礎研究を行っている。さらに、高階書き換えシステム、プログラムの帰納的性質の自動証明、関数・論理型言語の効率的な実行メカニズムと自動証明システムの柔軟な実行メカニズムの融合など、書き換えシステムに基づく計算・証明パラダイムの理論的および実験的研究を進めている。
研究テーマ
- 書き換え理論： 合流性、停止性、到達可能性、高階システム
- ソフトウェア基礎： 自動検証のためのプログラム変換
- 定理自動証明： 合流性検証、書き換え帰納法、帰納的定理の決定可能性
|
