項書き換えシステムは，関数型プログラムの計算モデルや 等式論理の定理自動証明の基礎として広く知られています． 項書き換えシステムの理論の基礎となっているのは， 停止性と合流性という2つの性質です． 停止性はプログラムが(どんな入力にもかかわらずに)計算が止まるという性質です． 合流性は途中にどのような計算過程を経ても同じ結果に到達できるという性質です． プログラムの停止性は，自分の書いたプログラムが暴走してしまった経験があれば馴染みがあるかもしれません． 合流性の方はあまり馴染みがないかとも思いますが， 項書き換えシステムの計算は非決定的(分岐がある場合がある)なので合流性が必ずしも成立するとは限りません．
停止性も合流性も抽象的な性質ですが，この2つの性質は 項書き換えシステムのさまざまな性質の保証や検証に役立つとても有用な性質です． このため，項書き換えシステムについての研究の黎明期から現在に至るまで， この2つの性質についてさまざまな証明法が研究されてきました．
停止性に関しては，停止性判定システムのコンペティッションが行われるほど， 数々の停止性自動判定システムが開発されています． 一方，合流性については，多くの理論的成果が知られているにもかかわらず， 自動判定システムの開発はほとんど試みられていませんでした．
そこで，われわれの研究室では， さまざまな判定方法を組み合わせた 合流性自動判定システムACPを 世界にさきがけて開発しました． ACPの特徴は，判定条件が直接適用できない複雑な項書き換えシステムに対しても， 直和分解や可換分解といった分解法を適用し，分解により得られた部分 システムに対して合流性判定法を適用することによって， 全体の合流性を自動判定する点です． また，さまざまな論文から例題を収集して合流性テスト集を作り，実験を進めています．
より強力/効率的な合流性判定システムを実現するために， 新しい合流性証明法や実装法の研究を行なっています． 合流性証明法の1つとして減少ダイアグラム法が知られています． SMTソルバを利用した減少ダイアグラム法による合流性自動証明の実現法を明らかにしました． また，減少ダイアグラム法の重み付けに用いるルールラベリング法にさまざまな改良を加えることで， 減少ダイアグラム法による自動証明の能力を高めることにも成功しました．
まで．