pith. sign in

arxiv: 2501.15303 · v3 · pith:7DVSBIQDnew · submitted 2025-01-25 · 💻 cs.LO · cs.DB

Guarded Negation Transitive Closure Logic

Diego Figueira , Santiago Figueira , Yoshiki Nakamura This is my paper

Pith reviewed 2026-05-23 04:50 UTC · model grok-4.3

classification 💻 cs.LO cs.DB
keywords guarded negationtransitive closure logicsatisfiabilitymodel checking2ExpTimetree automataUNTC
0
0 comments X

The pith

The satisfiability problem for guarded negation transitive closure logic is 2ExpTime-complete.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes that satisfiability for GNTC, the guarded negation fragment of transitive closure logic, is 2ExpTime-complete. It reaches this by a polynomial-time reduction from GNTC satisfiability to satisfiability of the unary negation fragment UNTC, followed by an exponential-time reduction from UNTC satisfiability to the non-emptiness problem for 2-way alternating parity tree automata. It further shows that model checking for GNTC is complete for P^NP with O(log squared n) oracle calls in combined complexity. These bounds transfer directly to UNTC and to UNFO^reg, resolving questions left open by earlier work.

Core claim

Satisfiability for GNTC is 2ExpTime-complete by a polynomial-time reduction to UNTC satisfiability and an exponential-time reduction from UNTC to non-emptiness of 2-way alternating parity tree automata. Model checking for GNTC is P^NP[O(log² n)]-complete in combined complexity, and the same bound holds for UNTC and UNFO^reg.

What carries the argument

The polynomial-time reduction from GNTC satisfiability to UNTC satisfiability together with the exponential-time reduction from UNTC satisfiability to emptiness of 2-way alternating parity tree automata.

If this is right

  • Satisfiability for UNTC is 2ExpTime-complete.
  • Satisfiability for UNFO^reg is 2ExpTime-complete.
  • Model checking for UNTC is P^NP[O(log² n)]-complete in combined complexity.
  • Model checking for UNFO^reg is P^NP[O(log² n)]-complete in combined complexity.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The reduction chain supplies an explicit decision procedure for GNTC formulas that runs in double-exponential time.
  • The same automata construction yields an algorithm for checking whether a given structure satisfies a GNTC sentence within the stated complexity bound.

Load-bearing premise

The reductions preserve satisfiability exactly in both directions and the target automata emptiness problem is already known to be 2ExpTime-complete.

What would settle it

A specific GNTC sentence whose satisfiability status differs from the emptiness status of the tree automaton produced by the reduction chain.

Figures

Figures reproduced from arXiv: 2501.15303 by Diego Figueira, Santiago Figueira, Yoshiki Nakamura.

Figure 1
Figure 1. Figure 1: Illustration of directions from g and the operator ⋄. A (relational) signature σ is a finite set of relation symbols with a map ar: σ → N; each ar(P) is the arity of a relation symbol P. A structure A over σ is a tuple ⟨|A|, {P A}P ∈σ⟩, where the universe |A| is a non-empty set of vertices and each P A ⊆ |A| ar(P ) is an ar(P)-ary relation on |A|. A structure A is finite [countable] if its universe |A| is … view at source ↗
Figure 3
Figure 3. Figure 3: Illustration for the abstraction map on bag [PITH_FULL_IMAGE:figures/full_fig_p004_3.png] view at source ↗
Figure 2
Figure 2. Figure 2: Example of the gluing operator ⊙A¯. By definition, for every structure A and every tree decom￾position B¯ of A, the structure ⊙B¯ is isomorphic to A. B. Abstract semantics on tree decompositions Inspired by abstract interpretation [28], we consider ab￾stracting vertices based on directions from a bag on tree decompositions. Let A¯ be an STR-labeled binary non-empty tree. Let U A¯ = ∆ ([92, 2] \ {0}) ⊎ [ g∈… view at source ↗
Figure 5
Figure 5. Figure 5: depicts this evaluation, where Γ = (Ax91v, Cx91 ∧ ¬∃wDx91w) and ∆ = (By1 ). Here, dashed lines indicate I (FV(Γ)) and I (FV(∆)). v0 direction 91 v0 g v0 direction 1 1 1 (Γ, ∆)p,A¯ I ,g ⇝ Γ p,A¯ I ,g ∧· p ∆ p,A¯ I ,g [PITH_FULL_IMAGE:figures/full_fig_p006_5.png] view at source ↗
Figure 4
Figure 4. Figure 4: The transition rules in the local model checker (Sect. IV-A) for GNFO. [PITH_FULL_IMAGE:figures/full_fig_p007_4.png] view at source ↗
Figure 6
Figure 6. Figure 6: Illustration of the rule (move). From the evaluation strategy above, we can show that the local model checker is sound and complete w.r.t. the semantics on tree decompositions. (See Appendix A, for a detailed proof.) Theorem 10 (Appendix A). For all Γ p,A¯ I ,g ∈ QGNFO, we have: |= Γp,A¯ I ,g ⇐⇒ ⊢ Γ p,A¯ I ,g. We give some toy examples of the local model checker. Example 11. Let A¯ be the STR-labeled tree … view at source ↗
Figure 7
Figure 7. Figure 7: The transition rules in the local model checker for GNTC, where [PITH_FULL_IMAGE:figures/full_fig_p009_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Intuition of the rule (TC-split). Here, d ′′ is some in [92, 2] \ {d}. Thus, (TC-split) is a sound rule. After that, the condition 3) holds for all ψi . Thus, we can apply (split)(move) in the same strategy as Sect. IV-B. From the evaluation strategy above, we can show that the local model checker is sound and complete w.r.t. the semantics on tree decompositions, as follows. (See Appendix C, for a detailed… view at source ↗
Figure 9
Figure 9. Figure 9: 2APTA transition rules from the local model checker for GNFO (Fig. 4). Here, we just write [PITH_FULL_IMAGE:figures/full_fig_p015_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: 2APTA transition rules from the local model checker for GNTC (Fig. 7), where [PITH_FULL_IMAGE:figures/full_fig_p019_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: A model checker for EPTC. • I ′ (x) = f(I(x)) for each x. Every EPTC formulas is preserved under homomorphisms, i.e., A, I ⊢ φ implies B, I′ ⊢ φ (This can be shown by straightforward induction on the structure of formulas). By using Prop. 49, we can show Prop. 45 as follows: Proof of Prop. 45. Suppose that A, I0 |= φ∧¬ψ. By Prop. 49, A, I0 ⊢cl′ (φ) φ. Let τ be its run and let τ (1i ) = (A, Ii ⊢cl′ (φ) Γi)… view at source ↗
Figure 12
Figure 12. Figure 12: z1 z2 · · · zk χ1 χ2 · · · χk y (1) 1 · · · y (1) k y (2) 1 · · · y (2) k . . . y (n) 1 · · · y (n) k · · · · · · · · · · · · [PITH_FULL_IMAGE:figures/full_fig_p027_12.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 1 minor

Summary. The paper studies the guarded negation fragment of transitive closure logic (GNTC). It claims that satisfiability for GNTC is 2ExpTime-complete via a polynomial-time reduction from GNTC to the unary negation fragment UNTC, followed by a direct exponential-time reduction from UNTC to non-emptiness of 2-way alternating parity tree automata (known to be 2ExpTime-complete). It further claims that model checking for GNTC is P^NP[O(log² n)]-complete in combined complexity, implying the same for UNTC and UNFO^reg.

Significance. Resolving the complexity of these fragments would be a solid contribution to the field of guarded logics and automata-based decision procedures, particularly if the reductions are tight and the model-checking result holds. The automata connection is a standard strength when it yields precise bounds.

major comments (1)
  1. [Abstract] Abstract: the claimed 2ExpTime upper bound for UNTC (and thus GNTC) does not follow from the stated reductions. An exponential-time reduction produces a 2-way alternating parity tree automaton whose size is exponential in the UNTC formula size n. The emptiness problem, even if 2ExpTime-complete in the size of the automaton, then requires time 2^{2^{poly(2^n)}}, which is outside 2ExpTime. This is load-bearing for the central satisfiability claim.
minor comments (1)
  1. [Abstract] The abstract and introduction should clarify whether the automata construction admits an implicit representation or on-the-fly emptiness check that avoids materializing the full exponential-size automaton.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the detailed review and for identifying an important issue in the complexity argument for satisfiability. We address the comment below and will make the necessary revisions to the manuscript.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the claimed 2ExpTime upper bound for UNTC (and thus GNTC) does not follow from the stated reductions. An exponential-time reduction produces a 2-way alternating parity tree automaton whose size is exponential in the UNTC formula size n. The emptiness problem, even if 2ExpTime-complete in the size of the automaton, then requires time 2^{2^{poly(2^n)}}, which is outside 2ExpTime. This is load-bearing for the central satisfiability claim.

    Authors: The referee is correct that the stated chain of reductions does not establish a 2ExpTime upper bound. The direct exponential-time reduction from UNTC satisfiability to 2APTA non-emptiness produces an automaton whose size is exponential in the input formula, and the known 2ExpTime-completeness of 2APTA emptiness is measured in the size of the automaton. Composing the two therefore yields a higher complexity class. We acknowledge this as an error in the current proof sketch. In the revised version we will either supply a corrected reduction (for example by constructing a 2APTA of size polynomial in the UNTC formula or by using an alternative decision procedure) that genuinely yields 2ExpTime, or we will adjust the complexity claim if no such reduction exists. We are currently reworking this section of the paper. revision: yes

Circularity Check

0 steps flagged

Reductions to externally known automata emptiness; derivation self-contained

full rationale

The paper derives 2ExpTime-completeness for GNTC satisfiability via a polynomial-time reduction to UNTC satisfiability followed by an exponential-time reduction to non-emptiness of 2-way alternating parity tree automata, whose 2ExpTime-completeness is invoked from prior literature. Model-checking complexity is likewise reduced to a standard class. No step equates a derived quantity to its input by definition, renames a fitted parameter as a prediction, or relies on a load-bearing self-citation whose justification collapses inside the paper. The chain is externally anchored and therefore exhibits no circularity.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The work rests on standard definitions of guarded negation, transitive closure, and 2-way alternating parity tree automata whose emptiness problem is already known to be 2ExpTime-complete; no new free parameters, invented entities, or ad-hoc axioms are introduced beyond the usual background of automata theory and logic.

axioms (2)
  • standard math Emptiness of 2-way alternating parity tree automata is 2ExpTime-complete
    Invoked when transferring the exponential-time reduction bound to UNTC and GNTC satisfiability.
  • domain assumption Polynomial-time reduction from GNTC to UNTC preserves satisfiability
    Stated as part (i) of the main result; correctness of this reduction is load-bearing for the 2ExpTime upper bound.

pith-pipeline@v0.9.0 · 5684 in / 1529 out tokens · 40697 ms · 2026-05-23T04:50:02.399577+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

100 extracted references · 100 canonical work pages · 3 internal anchors

  1. [1]

    Guarded nega- tion

    Vince B ´ar´any, Balder Ten Cate, and Luc Segoufin. Guarded nega- tion. Journal of the ACM , 62(3):22:1–22:26, 2015. doi:10.1145/ 2701414

    work page 2015

  2. [2]

    Guarded negation

    Vince B ´ar´any, Balder ten Cate, and Luc Segoufin. Guarded negation. In ICALP, volume 6756 of LNTCS, pages 356–367. Springer, 2011. doi:10.1007/978-3-642-22012-8_28

    work page doi:10.1007/978-3-642-22012-8_28 2011

  3. [3]

    UCQ-shaped

    Hajnal Andr ´eka, Istv ´an N ´emeti, and Johan van Benthem. Modal languages and bounded fragments of predicate logic. Journal of Philosophical Logic , 27(3):217–274, 1998. doi:10.1023/A: 1004275029985. 6As in [5, Proposition 6], the treewidth of the unraveled structure has a bound by the width of ψ (the maximal number of free variables occurring in the “U...

    work page doi:10.1023/a: 1998

  4. [4]

    Unary negation

    Luc Segoufin and Balder Ten Cate. Unary negation. Logical Methods in Computer Science , 9(3), 2013. doi:10.2168/LMCS-9(3:25) 2013

    work page doi:10.2168/lmcs-9(3:25 2013

  5. [5]

    A step up in expressiveness of decidable fixpoint logics

    Michael Benedikt, Pierre Bourhis, and Michael Vanden Boom. A step up in expressiveness of decidable fixpoint logics. In LICS, page 817–826. ACM, 2016. doi:10.1145/2933575.2933592

    work page doi:10.1145/2933575.2933592 2016

  6. [6]

    A step up in expressiveness of decidable fixpoint logics (extended version of [5])

    Michael Benedikt, Pierre Bourhis, and Michael Vanden Boom. A step up in expressiveness of decidable fixpoint logics (extended version of [5]). 2016. URL: https://hal.science/hal-01413890

    work page 2016

  7. [7]

    Gr ¨adel and I

    E. Gr ¨adel and I. Walukiewicz. Guarded fixed point logic. In LICS, pages 45–54. IEEE, 1999. doi:10.1109/LICS.1999.782585

    work page doi:10.1109/lics.1999.782585 1999

  8. [8]

    Moshe Y . Vardi. Reasoning about the past with two-way automata. In ICALP, volume 1443 of LNCS, pages 628–641. Springer, 1998. doi: 10.1007/BFb0055090

    work page doi:10.1007/bfb0055090 1998

  9. [9]

    Languages that capture complexity classes

    Neil Immerman. Languages that capture complexity classes. SIAM Jour- nal on Computing , 16(4):760–778, 1987. doi:10.1137/0216051

    work page doi:10.1137/0216051 1987

  10. [10]

    Undecidability results on two-variable logics

    Erich Gr ¨adel, Martin Otto, and Eric Rosen. Undecidability results on two-variable logics. Archive for Mathematical Logic , 38(4-5):313–354,

    work page

  11. [11]

    doi:10.1007/s001530050130

    work page doi:10.1007/s001530050130

  12. [12]

    The boundary between decidability and undecidability for transitive-closure logics

    Neil Immerman, Alex Rabinovich, Tom Reps, Mooly Sagiv, and Greta Yorsh. The boundary between decidability and undecidability for transitive-closure logics. In CSL, volume 3210 of LNCS, pages 160–

    work page

  13. [13]

    doi:10.1007/978-3-540-30124-0_15

    Springer, 2004. doi:10.1007/978-3-540-30124-0_15

    work page doi:10.1007/978-3-540-30124-0_15 2004

  14. [14]

    A Common Ancestor of PDL, Conjunctive Queries, and Unary Negation First-order

    Diego Figueira and Santiago Figueira. A common ancestor of PDL, conjunctive queries, and unary negation first-order, 2025. doi:10. 48550/arXiv.2501.11641

    work page internal anchor Pith review Pith/arXiv arXiv 2025

  15. [15]

    Querying the unary negation fragment with regular path expressions

    Jean Christoph Jung, Carsten Lutz, Mauricio Martel, and Thomas Schneider. Querying the unary negation fragment with regular path expressions. In ICDT, volume 98 of LIPIcs. Schloss Dagstuhl, 2018. doi:10.4230/LIPIcs.ICDT.2018.15

    work page doi:10.4230/lipics.icdt.2018.15 2018

  16. [16]

    PDL on steroids: on expressive extensions of PDL with intersection and converse

    Diego Figueira, Santiago Figueira, and Edwin Pin. PDL on steroids: on expressive extensions of PDL with intersection and converse. In LICS, pages 1–13. IEEE, 2023. doi:10.1109/LICS56636.2023. 10175813

    work page doi:10.1109/lics56636.2023 2023

  17. [17]

    PDL with intersection and converse: satisfiability and infinite-state model checking

    Stefan G ¨oller, Markus Lohrey, and Carsten Lutz. PDL with intersection and converse: satisfiability and infinite-state model checking. The Journal of Symbolic Logic , 74(1):279–314, 2009. doi:10.2178/ jsl/1231082313

    work page arXiv 2009

  18. [18]

    Reutter, Miguel Romero, and Moshe Y

    Juan L. Reutter, Miguel Romero, and Moshe Y . Vardi. Regular queries on graph databases. Theory of Computing Systems , 61(1):31–83, 2017. doi:10.1007/s00224-016-9676-2

    work page doi:10.1007/s00224-016-9676-2 2017

  19. [19]

    On the positive calculus of relations with transitive closure

    Damien Pous. On the positive calculus of relations with transitive closure. In STACS, volume 96 of LIPIcs, pages 3:1–3:16. Schloss Dagstuhl, 2018. doi:10.4230/LIPICS.STACS.2018.3

    work page doi:10.4230/lipics.stacs.2018.3 2018

  20. [20]

    Partial derivatives on graphs for Kleene allegories

    Yoshiki Nakamura. Partial derivatives on graphs for Kleene allegories. In LICS, pages 1–12. IEEE, 2017. doi:10.1109/LICS.2017. 8005132

    work page doi:10.1109/lics.2017 2017

  21. [21]

    Mapping Public Perception of Artificial Intelligence: Expectations, Risk-Benefit Tradeoffs, and Value as Determinants for Societal Acceptance

    Yoshiki Nakamura. Derivatives on graphs for the positive calculus of relations with transitive closure, 2024. doi:10.48550/arXiv. 2408.08236

    work page internal anchor Pith review doi:10.48550/arxiv 2024

  22. [22]

    On the (infinite) model theory of fixed-point logics

    J ¨org Flum. On the (infinite) model theory of fixed-point logics. In Models, Algebras, and Proofs . CRC Press, 1998

    work page 1998

  23. [23]

    Guarded fixed point logics and the monadic theory of countable trees

    Erich Gr ¨adel. Guarded fixed point logics and the monadic theory of countable trees. Theoretical Computer Science , 288(1):129–152, 2002. doi:10.1016/S0304-3975(01)00151-7

    work page doi:10.1016/s0304-3975(01)00151-7 2002

  24. [24]

    Neil Robertson and Paul D. Seymour. Graph minors. II. algorithmic aspects of tree-width. Journal of Algorithms, 7(3):309–322, 1986. doi: 10.1016/0196-6774(86)90023-4

    work page doi:10.1016/0196-6774(86)90023-4 1986

  25. [25]

    Graph Structure and Monadic Second-Order Logic

    Bruno Courcelle and Joost Engelfriet. Graph Structure and Monadic Second-Order Logic. Number 138 in Encyclopedia of Mathematics and its Applications. Cambridge University Press, 2012. doi:10.1017/ CBO9780511977619

    work page 2012

  26. [26]

    Neil Robertson and Paul D. Seymour. Graph minors. I. excluding a forest. Journal of Combinatorial Theory, Series B , 35(1):39–61, 1983. doi:10.1016/0095-8956(83)90079-5

    work page doi:10.1016/0095-8956(83)90079-5 1983

  27. [27]

    Muller, Ahmed Saoudi, and Paul E

    David E. Muller, Ahmed Saoudi, and Paul E. Schupp. Alternating automata, the weak monadic theory of the tree, and its complexity. In ICALP, volume 6 of LNCS, pages 275–283. Springer, 1986. doi: 10.1007/3-540-16761-7_77

    work page doi:10.1007/3-540-16761-7_77 1986

  28. [28]

    Muller, Ahmed Saoudi, and Paul E

    David E. Muller, Ahmed Saoudi, and Paul E. Schupp. Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In LICS, pages 422–427. IEEE,

    work page

  29. [29]

    doi:10.1109/LICS.1988.5139

    work page doi:10.1109/lics.1988.5139 1988

  30. [30]

    PDL inside the µ-calculus: A syntactic and an automata-theoretic characterization

    Facundo Carreiro and Yde Venema. PDL inside the µ-calculus: A syntactic and an automata-theoretic characterization. In AIML, pages 74–93. College Publications, 2014. URL: http://www.aiml.net/volumes/ volume10/Carreiro-Venema.pdf

    work page 2014

  31. [31]

    Abstract interpretation: a uni- fied lattice model for static analysis of programs by construction or approximation of fixpoints

    Patrick Cousot and Radhia Cousot. Abstract interpretation: a uni- fied lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL, page 238–252. ACM, 1977. doi:10.1145/512950.512973

    work page doi:10.1145/512950.512973 1977

  32. [32]

    Querying the guarded fragment

    Vince B ´ar´any, Georg Gottlob, and Martin Otto. Querying the guarded fragment. Logical Methods in Computer Science , V olume 10, Issue 2,

    work page

  33. [33]

    doi:10.2168/LMCS-10(2:3)2014

    work page doi:10.2168/lmcs-10(2:3)2014 2014

  34. [34]

    Brzozowski

    Janusz A. Brzozowski. Derivatives of regular expressions. Journal of the ACM, 11(4):481–494, 1964. doi:10.1145/321239.321249

    work page doi:10.1145/321239.321249 1964

  35. [35]

    Partial derivatives of regular expressions and finite automaton constructions

    Valentin Antimirov. Partial derivatives of regular expressions and finite automaton constructions. Theoretical Computer Science , 155(2):291– 319, 1996. doi:10.1016/0304-3975(95)00182-4

    work page doi:10.1016/0304-3975(95)00182-4 1996

  36. [36]

    Fischer and Richard E

    Michael J. Fischer and Richard E. Ladner. Propositional dynamic logic of regular programs. Journal of Computer and System Sciences , 18(2):194–211, 1979. doi:10.1016/0022-0000(79)90046-1

    work page doi:10.1016/0022-0000(79)90046-1 1979

  37. [37]

    2-ExpTime lower bounds for proposi- tional dynamic logics with intersection

    Martin Lange and Carsten Lutz. 2-ExpTime lower bounds for proposi- tional dynamic logics with intersection. The Journal of Symbolic Logic , 70(04):1072–1086, 2005. doi:10.2178/jsl/1129642115

    work page doi:10.2178/jsl/1129642115 2005

  38. [38]

    Two-way alternating automata and finite models

    Mikołaj Bojar ´nczyk. Two-way alternating automata and finite models. In ICALP, volume 2380 of LNCS, pages 833–844. Springer, 2002. doi: 10.1007/3-540-45465-9_71

    work page doi:10.1007/3-540-45465-9_71 2002

  39. [39]

    Finite satisfiability for guarded fixpoint logic

    Vince B ´ar´any and Mikołaj Boja ´nczyk. Finite satisfiability for guarded fixpoint logic. Information Processing Letters , 112(10):371–375, 2012. doi:10.1016/j.ipl.2012.02.005

    work page doi:10.1016/j.ipl.2012.02.005 2012

  40. [40]

    Finite satisfiability of unary negation fragment with transitivity

    Daniel Danielski and Emanuel Kiero ´nski. Finite satisfiability of unary negation fragment with transitivity. In MFCS, volume 138 of LIPIcs, page 17:1–17:15. Schloss Dagstuhl, 2019. doi:10.4230/LIPIcs. MFCS.2019.17

    work page doi:10.4230/lipics 2019

  41. [41]

    Donald E. Knuth. Two notes on notation, 1992. doi:10.48550/ arXiv.math/9205211

    work page internal anchor Pith review Pith/arXiv arXiv 1992

  42. [42]

    Parity games played on transition graphs of one-counter processes

    Olivier Serre. Parity games played on transition graphs of one-counter processes. In FoSSaCS, volume 3921 of LNTCS, pages 337–351. Springer, 2006. doi:10.1007/11690634_23

    work page doi:10.1007/11690634_23 2006

  43. [43]

    Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, and Moshe Y . Vardi. Containment of conjunctive regular path queries with inverse. In KR, page 176–185. Morgan Kaufmann Publishers Inc., 2000

    work page 2000

  44. [44]

    Petri automata

    Paul Brunet and Damien Pous. Petri automata. Logical Methods in Computer Science, 13(3), 2017. doi:10.23638/LMCS-13(3:33) 2017

    work page doi:10.23638/lmcs-13(3:33 2017

  45. [45]

    On the restraining power of guards

    Erich Gr ¨adel. On the restraining power of guards. The Journal of Symbolic Logic, 64(04):1719–1742, 1999. doi:10.2307/2586808

    work page doi:10.2307/2586808 1999

  46. [46]

    Emil L. Post. Recursive unsolvability of a problem of Thue. The Journal of Symbolic Logic , 12(1):1–11, 1947. doi:10.2307/2267170

    work page doi:10.2307/2267170 1947

  47. [47]

    Equivalences among relational expressions with the union and difference operators

    Yehoshua Sagiv and Mihalis Yannakakis. Equivalences among relational expressions with the union and difference operators. Journal of the ACM, 27(4):633–655, 1980. doi:10.1145/322217.322221

    work page doi:10.1145/322217.322221 1980

  48. [48]

    The complexity of equivalence, en- tailment, and minimization in existential positive logic

    Simone Bova and Hubie Chen. The complexity of equivalence, en- tailment, and minimization in existential positive logic. Journal of Computer and System Sciences, 81(2):443–457, 2015. doi:10.1016/ J.JCSS.2014.10.002

    work page 2015

  49. [49]

    On logics with two variables

    Erich Gr ¨adel and Martin Otto. On logics with two variables. The- oretical Computer Science , 224(1):73–113, 1999. doi:10.1016/ S0304-3975(98)00308-9

    work page 1999

  50. [50]

    Games and model checking for guarded logics

    Dietmar Berwanger and Erich Gr ¨adel. Games and model checking for guarded logics. In LPAR, volume 2250 of LNAI, pages 70–84. Springer,

    work page

  51. [51]

    doi:10.1007/3-540-45653-8_5

    work page doi:10.1007/3-540-45653-8_5

  52. [52]

    Chandra and Philip M

    Ashok K. Chandra and Philip M. Merlin. Optimal implementation of conjunctive queries in relational data bases. In STOC, pages 77–90. ACM, 1977. doi:10.1145/800105.803397

    work page doi:10.1145/800105.803397 1977

  53. [53]

    Moshe Y . Vardi. The complexity of relational query languages (extended abstract). In STOC, pages 137–146. ACM, 1982. doi:10.1145/ 800070.802186

    work page arXiv 1982

  54. [54]

    Oracle circuits for branching-time model check- ing

    Philippe Schnoebelen. Oracle circuits for branching-time model check- ing. In ICALP, volume 2719 of LNCS, pages 790–801. Springer, 2003. doi:10.1007/3-540-45061-0_62

    work page doi:10.1007/3-540-45061-0_62 2003

  55. [55]

    Fixed-point logics and solitaire games

    Dietmar Berwanger and Erich Gr ¨adel. Fixed-point logics and solitaire games. Theory of Computing Systems , 37(6):675–694, 2004. doi: 10.1007/s00224-004-1147-5 . 12

    work page doi:10.1007/s00224-004-1147-5 2004

  56. [56]

    Relationships between nondeterministic and determin- istic tape complexities

    Walter Savitch. Relationships between nondeterministic and determin- istic tape complexities. Journal of Computer and System Sciences , 4(2):177–192, 1970. doi:10.1016/S0022-0000(70)80006-X

    work page doi:10.1016/s0022-0000(70)80006-x 1970

  57. [57]

    Lower bounds for natural proof systems

    Dexter Kozen. Lower bounds for natural proof systems. In FOCS, pages 254–266. IEEE, 1977. doi:10.1109/SFCS.1977.16

    work page doi:10.1109/sfcs.1977.16 1977

  58. [58]

    Finite Model Theory

    Heinz-Dieter Ebbinghaus and J ¨org Flum. Finite Model Theory. Springer Monographs in Mathematics. Springer, 2 edition, 1995. doi:10. 1007/3-540-28788-4

    work page 1995

  59. [59]

    On the calculus of relations

    Alfred Tarski. On the calculus of relations. The Journal of Symbolic Logic, 6(3):73–89, 1941. doi:10.2307/2268577

    work page doi:10.2307/2268577 1941

  60. [60]

    Modal Correspondence Theory

    Johan Van Benthem. Modal Correspondence Theory . doctoral, Univer- sity of Amsterdam, 1976. URL: https://eprints.illc.uva.nl/id/eprint/1838/

    work page 1976

  61. [61]

    Correspondence theory

    Johan Van Benthem. Correspondence theory. In Handbook of Philosoph- ical Logic: Volume II: Extensions of Classical Logic , pages 167–247. Springer, 1984. doi:10.1007/978-94-009-6259-0_4

    work page doi:10.1007/978-94-009-6259-0_4 1984

  62. [62]

    How to best nest regular path queries

    Pierre Bourhis, Markus Kr ¨otzsch, and Sebastian Rudolph. How to best nest regular path queries. In DL, volume 1193 of CEUR Workshop Proceedings , page 404–415. CEUR-WS.org, 2014. URL: https://ceur-ws.org/V ol-1193/paper 80.pdf

    work page 2014

  63. [63]

    Foundations of Databases: The Logical Level

    Serge Abiteboul, Richard Hull, and Victor Vianu. Foundations of Databases: The Logical Level . Addison-Wesley Longman Publishing Co., Inc., 1st edition, 1995

    work page 1995

  64. [64]

    Relation algebras with transitive closure

    Kan Ching Ng. Relation algebras with transitive closure . PhD thesis, University of California, 1984

    work page 1984

  65. [65]

    A completeness theorem for Kleene algebras and the algebra of regular events

    Dexter Kozen. A completeness theorem for Kleene algebras and the algebra of regular events. In LICS, pages 214–225. IEEE, 1991. doi: 10.1109/LICS.1991.151646

    work page doi:10.1109/lics.1991.151646 1991

  66. [66]

    Freyd and Andre Scedrov

    Peter J. Freyd and Andre Scedrov. Categories, Allegories, volume 39. North-Holland, 1990. doi:10.1016/S0924-6509(08)70049-7

    work page doi:10.1016/s0924-6509(08)70049-7 1990

  67. [67]

    Petri automata for Kleene allegories

    Paul Brunet and Damien Pous. Petri automata for Kleene allegories. In LICS, pages 68–79. IEEE, 2015. doi:10.1109/LICS.2015.17

    work page doi:10.1109/lics.2015.17 2015

  68. [68]

    Expressive power and succinctness of the positive calculus of binary relations

    Yoshiki Nakamura. Expressive power and succinctness of the positive calculus of binary relations. Journal of Logical and Algebraic Meth- ods in Programming , 127:100760, 2022. doi:10.1016/j.jlamp. 2022.100760

    work page doi:10.1016/j.jlamp 2022

  69. [69]

    Results on the guarded fragment with equivalence or transitive relations

    Emanuel Kiero ´nski. Results on the guarded fragment with equivalence or transitive relations. In CSL, volume 3634 of LNTCS, pages 309–324. Springer, 2005. doi:10.1007/11538363_22. APPENDIX A PROOF OF THMS . 10, 14: SOUND - AND COMPLETENESS OF THE LOCAL MODEL CHECKER FOR GNFO In this section, we give a proof of Thms. 10, 14. We recall the local model chec...

    work page doi:10.1007/11538363_22 2005

  70. [70]

    If Γ contains a free variable x with #I (x) ≥ 2: By applying the rule (conc), this case is shown

    work page

  71. [71]

    For the condition w.r.t

    Else if Γ contains a formula of the form ψ ∨ ρ, ψ ∧ ρ, or ∃xψ: By applying the corresponding rules ( ∨), (∧), or (∃), this case is shown. For the condition w.r.t. cl, this is shown by straightfor- wardly transforming the derivation tree of cl(φ), e.g., (∆, ψ1 ∨ ψ2) ∈ cl(φ) implies (∆, ψi) ∈ cl(φ) by the following transformation: . . . (ψ1 ∨ψ2) ∈cl(ψ1 ∨ψ2)...

    work page

  72. [72]

    If #Γ ≥ 2, then by applying (split), this case is proved

    Else if Γ contains some formula φ such that I (FV(φ)) ⊆ U¯A g,0: By 2), φ is of the form α or α ∧ ¬ψ. If #Γ ≥ 2, then by applying (split), this case is proved. Otherwise, by |= Γp,¯A I ,g and I (FV(φ)) ⊆ U¯A g,0, we have ⟨¯A(g), I ⟩ |= α. Then by applying (a1)(GN1), this case is shown

    work page

  73. [73]

    Since FV(α) = FV(φ), α is also split

    Else if Γ contains some split formula φ: By 2), φ is of the form α or α ∧ ¬ψ. Since FV(α) = FV(φ), α is also split. Then by applying (a2)(GN2), this case is shown

    work page

  74. [74]

    As Γ is split, we can let Γ = (∆ , Λ) where ∆ ̸= ∅, Λ ̸= ∅, and I (FV(∆)) ⊆ U¯A g,d for some d ∈ [92, 2] \ {0}

    Else if Γ is split: By 3) 4), for each φ ∈ Γ, there is some d ∈ [92, 2] \ {0} such that I (FV(φ)) ⊆ U¯A g,d. As Γ is split, we can let Γ = (∆ , Λ) where ∆ ̸= ∅, Λ ̸= ∅, and I (FV(∆)) ⊆ U¯A g,d for some d ∈ [92, 2] \ {0}. Then by applying the rule (split), this case is shown

    work page

  75. [75]

    By 3) with Γ ̸= ∅, d ∈ I (FV(Γ)) also holds

    Else if Γ ̸= ∅: By 5), there is some d ∈ [92, 2] \ {0} such that I (FV(Γ)) ⊆ U¯A g,d. By 3) with Γ ̸= ∅, d ∈ I (FV(Γ)) also holds. Then by applying the rule (move), this case is shown. After applying (move), the distance is decreased by d ∈ I (FV(Γ)) ⊆ U¯A g,d

    work page

  76. [76]

    U¯A g ”, “U¯A d,g

    Else: By 6), we have Γ = ∅. Thus by applying the rule (emp), this case is shown. Note that, on the parameter p(Γp,¯A I ,g), if p is odd, then the first argument is decreased in 3) for ¬ and 7), the second argument is decreased in 2), 3), and 5), the third argument is decreased in 1) and 6), and the case 4) does not occur. Hence, this completes the proof. ...

    work page

  77. [77]

    For a GNTC formula set Γ, we write Unf(Γ) for the set of GNTC formula sets obtained from Γ by replacing each φ ∈ Γ with some φ′ ∈ Unf(φ)

    More precisely, Unf(φ) is inductively defined as follows: Unf(α) = ∆ {α}, Unf(α ∧ ¬ψ) = ∆ {α ∧ ¬ψ}, Unf(ψ ∨ ρ) = ∆ {ψ′ ∨ ρ′ | ψ′ ∈ Unf(ψ) and ρ′ ∈ Unf(ρ)}, Unf(ψ ∧ ρ) = ∆ {ψ′ ∧ ρ′ | ψ′ ∈ Unf(ψ) and ρ′ ∈ Unf(ρ)}, Unf(∃xψ) = ∆ {∃xψ′ | ψ′ ∈ Unf(ψ)}, Unf([ψ]∗ ¯v ¯w¯x¯y) = ∆ [ n≥0 Unf([ψ]n ¯v ¯w¯x¯y). For a GNTC formula set Γ, we write Unf(Γ) for the set of GN...

    work page

  78. [78]

    If Γ contains a free variable x with #I (x) ≥ 2: In the same way as 1) of Lem. 27

    work page

  79. [79]

    Else if Γ contains a formula of the form ψ ∨ ρ, ψ ∧ ρ, or ∃xψ: In the same way as 2) of Lem. 27

    work page

  80. [80]

    Else if Γ contains some formula φ such that I (FV(φ)) ⊆ U¯A g,0 and φ is of the form α or α ∧ ¬ψ: In the same way as 3) of Lem. 27

    work page

Showing first 80 references.