Motivated by an application where we try to make proofs for Description Logic inferences smaller by rewriting, we consider the following decision problem, which we call the small term reachability problem: given a term rewriting system $R$, a term $s$, and a natural number $n$, decide whether there is a term $t$ of size $\leq n$ reachable from $s$ using the rules of $R$. We investigate the complexity of this problem depending on how termination of $R$ can be established. We show that the problem is in general NP-complete for length-reducing term rewriting systems. Its complexity increases to N2ExpTime-complete (NExpTime-complete) if termination is proved using a (linear) polynomial order and to PSpace-complete for systems whose termination can be shown using a restricted class of Knuth-Bendix orders. Confluence reduces the complexity to P for the length-reducing case, but has no effect on the worst-case complexity in the other two cases. Finally, we consider the large term reachability problem, a variant of the problem where we are interested in reachability of a term of size $\geq n$. It turns out that this seemingly innocuous modification in some cases changes the complexity of the problem, which may also become dependent on whether the number $n$ is is represented in unary or binary encoding, whereas this makes no difference for the complexity of the small term reachability problem.

翻译：受一项旨在通过重写缩小描述逻辑推理证明规模的应用程序启发，我们考虑以下决策问题，称之为小项可达性问题：给定一个项重写系统 $R$、一个项 $s$ 和一个自然数 $n$，判断是否存在一个规模 $\leq n$ 的项 $t$，可通过 $R$ 的规则从 $s$ 可达。我们研究了该问题的复杂度如何依赖于 $R$ 终止性的证明方式。结果表明，对于长度缩减项重写系统，该问题在一般情况下是 NP 完全的。若终止性通过（线性）多项式序证明，其复杂度上升至 N2ExpTime 完全（NExpTime 完全）；而对于可通过受限类 Knuth-Bendix 序证明终止性的系统，其复杂度为 PSpace 完全。合流性在长度缩减情形下将复杂度降低至 P，但在其他两种情形下对最坏情况复杂度无影响。最后，我们考虑了大项可达性问题，即关注规模 $\geq n$ 的项的可达性的变体。结果表明，这一看似微小的修改在某些情况下改变了问题的复杂度，且复杂度可能还依赖于数字 $n$ 是以一元编码还是二进制编码表示，而这对小项可达性问题的复杂度无影响。