Guarded Negation Transitive Closure Logic
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910233315508224 |
|---|---|
| author | Figueira, Diego Figueira, Santiago Nakamura, Yoshiki |
| author_facet | Figueira, Diego Figueira, Santiago Nakamura, Yoshiki |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_15303 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Guarded Negation Transitive Closure Logic Figueira, Diego Figueira, Santiago Nakamura, Yoshiki Logic in Computer Science Databases 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. |
| title | Guarded Negation Transitive Closure Logic |
| topic | Logic in Computer Science Databases |
| url | https://arxiv.org/abs/2501.15303 |