項書換え系に関する20年来の難問を解決 (1999～2001)

項書換え系は、等式系を用いた数理的な推論を計算機で効率良く行うための体系です。2つの項が等式系のもとで同値であることの証明は、一般には探索問題になりますが、項書換え系を用いると、計算結果の一致に帰着することができ計算機で効率よく実現できます。そのためには、項書換え系による計算結果が一意に定まることが必要です。私たちは2001年の研究成果として、1981年以来未解決だった一意性に関する十分条件を、肯定的に解決しました。