Document Open Access Logo

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

Author Yoshiki Nakamura

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2023.69.pdf
  • Filesize: 1.16 MB
  • 15 pages

Document Identifiers

Related Versions

Subject Classification

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

Metrics

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

Abstract

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.

Cite As Get 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) https://doi.org/10.4230/LIPIcs.MFCS.2023.69

Author Details

Yoshiki Nakamura
  • Tokyo Institute of Technology, Japan

Funding

  • Nakamura, Yoshiki: This work was supported by JSPS KAKENHI Grant Number JP21K13828.

Acknowledgements

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

Supplementary Materials

References

  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.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact