We study the guarded negation fragment of transitive closure logic (GNTC). We show that the satisfiability problem for GNTC is 2ExpTime-complete, by establishing the following reductions: (i) a polynomial-time reduction from the satisfiability problem for GNTC to the satisfiability problem for the unary negation fragment UNTC of GNTC, and (ii) a direct exponential-time reduction from the satisfiability problem for UNTC to the non-emptiness problem for 2-way alternating parity tree automata. Furthermore, we show that the model checking problem for GNTC is $\mathsf{P}^{\mathsf{NP}[\mathcal{O}(\log^2 n)]}$-complete in combined complexity. Our result implies $\mathsf{P}^{\mathsf{NP}[\mathcal{O}(\log^2 n)]}$-completeness for both UNTC and $\mathrm{UNFO}^{\mathrm{reg}}$, which were left open in previous works.

翻译：我们研究了传递闭包逻辑的带保护否定片段（GNTC）。通过建立以下归约，我们证明了GNTC的可满足性问题是2ExpTime完全的：(i) 从GNTC的可满足性问题到其一元否定片段UNTC的多项式时间归约，以及(ii) 从UNTC的可满足性问题到双向交替奇偶树自动机非空性问题的直接指数时间归约。此外，我们证明了GNTC的模型检验问题在联合复杂度下是$\mathsf{P}^{\mathsf{NP}[\mathcal{O}(\log^2 n)]}$完全的。我们的结果意味着UNTC和$\mathrm{UNFO}^{\mathrm{reg}}$均为$\mathsf{P}^{\mathsf{NP}[\mathcal{O}(\log^2 n)]}$完全，这填补了先前工作中遗留的空白。