コンピューティング科学研究領域の廣川直准教授が、平成15年に開催されたThe 19th International Conference on Automated Deduction（CADE-19）において発表した論文が高く評価され、CADE-30にてスコーレム賞（Thoralf Skolem Award）を受賞しました。

　CADEは、自動推論分野の主要な国際会議であり、CADE-30は、令和7年7月28日～8月2日まで、ドイツのシュトゥットガルト（Stuttgart）で開催されました。
　スコーレム賞は、CADEで過去に発表された論文のうち、「長年にわたって自動推論分野に大きな影響を与えた研究」を顕彰する賞です。平成26年に創設され、発表からおよそ10年後の論文を選考対象としていますが、今回の受賞論文のように平成16年以前のものに対しては20年・30年・40年経過した時点で選考される制度になっています。
　今回の受賞は、項書換えの停止性証明における探索空間を削減する手法が、依存対による項書換えの停止性解析の効率的な自動化を可能にし、分野を超えて大きな影響を与えたことが評価されたものです。

※参考：CADE

■受賞年月日
　令和7年7月29日

■研究題目、論文タイトル等
Automating the Dependency Pair Method
（Proceedings of the 19th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence 2741, pp. 32-46, 2003.）

■研究者、著者
Nao Hirokawa and Aart Middeldorp

■受賞対象となった研究の内容
　プログラミング言語の数学的なモデルである項書換えの停止性自動証明技法において指数時間要していた依存グラフの循環解析に線形時間アルゴリズムを与え、また指数的な大きさの探索空間から適切な引数切り落としを特定する効率的な手続きを与えた。

■受賞にあたって一言
　停止性自動証明のための技法は過去二十年間、目覚ましい発展を遂げました。現在、それらの成果は定理証明支援系やソフトウェア検証ツールに取り込まれつつあり、続く十年間においては、プログラミング言語の処理系など、さらに身近なところで使用されると思います。その基盤理論の一端を担えたことを光栄に思います。

令和7年10月27日