項書換え系（ＴＲＳ）は、項の書換えの繰り返しにより計算を進 める計算モデルであり、関数型言語の計算モデルや定理自動証明な どに利用されている。停止性は、計算がその過程に依らず必ず停止 し値を返すことを保証する性質であり、応用上重要である。 これまでに、単純化順序によるＴＲＳの停止性の十分条件が知ら れている。最近、Artsらにより依存対と呼ばれる手法が研究され、 停止性の証明できるＴＲＳのクラスが広がった。この方法は、ＴＲ Ｓ上で依存対と依存対列を定義し、無限な依存対列が存在しないと き停止性を持つことを利用して、依存対に順序がつくことを示すこ とによってＴＲＳの停止性を証明する手法である。 本論文では、依存対に基づいてＴＲＳの停止性を証明するシステ ムを試作したので、その概要について述べる。また、作成したシス テムによる実験から得られた、依存対に基づく停止性判定手法の評 価を与える。