項書換え系(TRS)は、定理の自動証明や代数的仕様記述などに広く利用されている計 算モデルである。項書換え系の研究において停止性は最も重要なテーマの１つであ る。
依存対(dependency pair)法、並びに、切り落とし法(argument filtering)がArtsら によって考案された。これにより従来の手法では示すことのできなかった、TRSの停 止性を示すことができる。
本研究では依存対と切り落とし法に基づく停止性判定モジュールを実装する。
切り落とし法では基本的に全ての関数の引数の減らし方ついて試す必要があるため、 組合せ的爆発を引き起こす。そこで、探索の枝刈りの一手法を考案しこれを実装し た。これにより実行時間と使用メモリを大幅に削減することができた。