On the Finite Variable-Occurrence Fragment of the Calculus of Relations with Bounded Dot-Dagger Alternation

Author Yoshiki Nakamura

Thumbnail PDF


  • Filesize: 1.16 MB
  • 15 pages

Document Identifiers

Author Details

Yoshiki Nakamura
  • Tokyo Institute of Technology, Japan


We would like to thank the anonymous reviewers for their useful comments.

Cite AsGet BibTex

Yoshiki Nakamura. On the Finite Variable-Occurrence Fragment of the Calculus of Relations with Bounded Dot-Dagger Alternation. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 69:1-69:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


We introduce the k-variable-occurrence fragment, which is the set of terms having at most k occurrences of variables. We give a sufficient condition for the decidability of the equational theory of the k-variable-occurrence fragment using the finiteness of a monoid. As a case study, we prove that for Tarski’s calculus of relations with bounded dot-dagger alternation (an analogy of quantifier alternation in first-order logic), the equational theory of the k-variable-occurrence fragment is decidable for each k.

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
  • Relation algebra
  • First-order logic
  • Decidable fragment
  • Monoid


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Alfred V. Aho and Margaret J. Corasick. Efficient string matching: an aid to bibliographic search. Communications of the ACM, 18(6):333-340, 1975. URL: https://doi.org/10.1145/360825.360855.
  2. Hajnal Andréka and D. A. Bredikhin. The equational theory of union-free algebras of relations. Algebra Universalis, 33(4):516-532, 1995. URL: https://doi.org/10.1007/BF01225472.
  3. Paul Bernays and Moses Schönfinkel. Zum Entscheidungsproblem der mathematischen Logik. Mathematische Annalen, 99(1):342-372, 1928. URL: https://doi.org/10.1007/BF01459101.
  4. Ronald V. Book and Friedrich Otto. String-Rewriting Systems. Springer, 1993. URL: https://doi.org/10.1007/978-1-4613-9771-7.
  5. Samuel R. Buss. The boolean formula value problem is in ALOGTIME. In STOC, pages 123-131. ACM, 1987. URL: https://doi.org/10.1145/28395.28409.
  6. Samuel R. Buss, Stepane A. Cook, Anshul Gupta, and Vijaya Ramachandran. An optimal parallel algorithm for formula evaluation. SIAM Journal on Computing, 21(4):755-780, 1992. URL: https://doi.org/10.1137/0221046.
  7. Egon Börger, Erich Grädel, and Yuri Gurevich. The Classical Decision Problem. Springer, 1997. URL: https://link.springer.com/9783540423249.
  8. Alonzo Church. A note on the Entscheidungsproblem. The Journal of Symbolic Logic, 1(01):40-41, 1936. URL: https://doi.org/10.2307/2269326.
  9. Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In TACAS, volume 13243 of LNCS, pages 337-340. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78800-3_24.
  10. Jules Desharnais, Peter Jipsen, and Georg Struth. Domain and antidomain semigroups. In RelMiCS, volume 5827 of LNCS, pages 73-87. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-04639-1_6.
  11. Steven Givant. The calculus of relations as a foundation for mathematics. Journal of Automated Reasoning, 37(4):277-322, 2007. URL: https://doi.org/10.1007/s10817-006-9062-x.
  12. David Harel, Dexter Kozen, and Jerzy Tiuryn. Dynamic Logic. The MIT Press, 2000. URL: https://doi.org/10.7551/mitpress/2516.001.0001.
  13. Marco Hollenberg. An equational axiomatization of dynamic negation and relational composition. Journal of Logic, Language and Information, 6(4):381-401, 1997. URL: https://doi.org/10.1023/A:1008271805106.
  14. A. S. Kahr, Edward F. Moore, and Hao Wang. Entscheidungsproblem reduced to the AEA case. Proceedings of the National Academy of Sciences, 48(3):365-377, 1962. URL: https://doi.org/10.1073/pnas.48.3.365.
  15. Markus Lohrey. On the parallel complexity of tree automata. In RTA, volume 2051 of LNCS, pages 201-215. Springer, 2001. URL: https://doi.org/10.1007/3-540-45127-7_16.
  16. Roger D. Maddux. Undecidable semiassociative relation algebras. The Journal of Symbolic Logic, 59(02):398-418, 1994. URL: https://doi.org/10.2307/2275397.
  17. A. A. Markov. On the impossibility of certain algorithms in the theory of associative systems. Doklady Akademii Nauk SSSR 55, 58, pages 587-590, 353-356, 1947. Google Scholar
  18. David A. Mix Barrington, Neil Immerman, and Howard Straubing. On uniformity within NC¹. Journal of Computer and System Sciences, 41(3):274-306, 1990. URL: https://doi.org/10.1016/0022-0000(90)90022-D.
  19. Yoshiki Nakamura. The undecidability of FO3 and the calculus of relations with just one binary relation. In ICLA, volume 11600 of LNCS, pages 108-120. Springer, 2019. URL: https://doi.org/10.1007/978-3-662-58771-3_11.
  20. Yoshiki Nakamura. Expressive power and succinctness of the positive calculus of relations. In RAMiCS, volume 12062 of LNCS, pages 204-220. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-43520-2_13.
  21. Yoshiki Nakamura. Expressive power and succinctness of the positive calculus of binary relations. Journal of Logical and Algebraic Methods in Programming, 127:100760, 2022. URL: https://doi.org/10.1016/j.jlamp.2022.100760.
  22. Yoshiki Nakamura. Existential calculi of relations with transitive closure: Complexity and edge saturations. In LICS, pages 1-13. IEEE, 2023. URL: https://doi.org/10.1109/LICS56636.2023.10175811.
  23. Yoshiki Nakamura. On the finite variable-occurrence fragment of the calculus of relations with bounded dot-dagger alternation, 2023. URL: https://doi.org/10.48550/arXiv.2307.05046.
  24. Yoshiki Nakamura. Repository for "on the finite variable-occurrence fragment of the calculus of relations with bounded dot-dagger alternation", 2023. URL: https://bitbucket.org/yoshikinakamura/k-vo_cor_with_bounded_dot_dagger/.
  25. Emil L. Post. Recursive unsolvability of a problem of Thue. The Journal of Symbolic Logic, 12(1):1-11, 1947. URL: https://doi.org/10.2307/2267170.
  26. 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. URL: https://doi.org/10.4230/LIPICS.STACS.2018.3.
  27. F. P. Ramsey. On a problem of formal logic. Proceedings of the London Mathematical Society, s2-30(1):264-286, 1930. URL: https://doi.org/10.1112/plms/s2-30.1.264.
  28. Alfred Tarski. On the calculus of relations. The Journal of Symbolic Logic, 6(3):73-89, 1941. URL: https://doi.org/10.2307/2268577.
  29. Alfred Tarski and Steven Givant. A Formalization of Set Theory without Variables, volume 41. American Mathematical Society, 1987. URL: https://doi.org/10.1090/coll/041.
  30. Alan M. Turing. On computable numbers, with an application to the entscheidungsproblem. Proceedings of the London Mathematical Society, s2-42(1):230-265, 1937. URL: https://doi.org/10.1112/plms/s2-42.1.230.