|
項書き換えシステムの理論は定理自動証明や計算モデルで広く利用されている。近年、項書き換えシステムの合流性自動証明システムがいくつか開発されているが、合流性自動証明システムの応用ついてはほとんど研究されていない。本研究では、項書き換えシステムの合流性自動証明システムに基づくプログラム自動検証法を研究する。研究成果としては、永続性と型情報に基づく合流性判定、プログラム変換に基づく定理自動証明、名目書き換えシステムの合流性条件、木オートマトン完備化の停止条件、基底合流性の自動判定、整礎順序をもつモノイド上の抽象リダクションシステムなどがある。
|
