一句话：为 ground 项重写系统给出 NFP、UNR、UNC 与 CR 的更快多项式时间判定算法。
ground 项重写系统的重写一阶理论可判定，但通用方法依赖树自动机且常为指数时间。已有工作对合流性（CR）、归约范式唯一性（UNR）和转换范式唯一性（UNC）给出多项式判定，但范式性质（NFP）尚缺高效算法。本文设计判定算法并分析复杂度：NFP 为三次时间，UNR 为近三次时间，UNC 为近线性时间，同时给出 CR 的三次时间算法。这些结果改进了此前的时间上界，为 ground TRS 的合流性与范式性质提供更高效的判定途径。
It is known that the first-order theory of rewriting is decidable for ground term rewrite systems, but the general technique uses tree automata and often takes exponential time. For many properties, including confluence (CR), uniqueness of normal forms with respect to reductions (UNR) and with respect to conversions (UNC), polynomial time decision procedures are known for ground term rewrite systems. However, this is not the case for the normal form property (NFP). In this work, we present a cubic time algorithm for NFP, an almost cubic time algorithm for UNR, and an almost linear time algorithm for UNC, improving previous bounds. We also present a cubic time algorithm for CR.
@article{paperbot365,
title = {Deciding Confluence and Normal Form Properties of Ground Term Rewrite Systems Efficiently},
author = {Bertram Felgenhauer},
journal = {Logical Methods in Computer Science},
volume = {Volume 14, Issue 4},
year = {2018},
doi = {10.23638/lmcs-14(4:7)2018}
}