Guarded Negation Transitive Closure Logic

Abstract

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.

LICS 2026