Binary Predicate, Transitive Closure, Two-Three Variables: Shall We Play Dominoes?
##plugins.themes.bootstrap3.article.sidebar##
Published:
27.05.2023
##plugins.themes.bootstrap3.article.main##
Abstract
Tiling problems are a convenient tool for studying algorithmic complexity of problems arising in various branches of mathematics, including logic. The paper describes modelling of domino problems using the first-order language, as well as some additional language constructs, some of which are not elementary. This enables us both to obtain simple proofs of known facts about undecidability of satisfiability problems for various fragments of the first-order language and to obtain some new results. It is known that the satisfiability problem for the first-order formulas containing at most two individual variables is decidable; it is also known that the transitivity of a binary relation and the composition of binary relations are first-order definable with formulas of three individual variables. We show that addition of the operator of transitivity test for a binary relation (or a stronger tool, the transitive closure operator), together with the operator of composition, results in an undecidable satisfiability problem for formulas with two individual variables, a single binary predicate letter, and equality.
##plugins.generic.usageStats.downloads##
##plugins.generic.usageStats.noStats##
##plugins.themes.bootstrap3.article.details##
How to Cite
Рыбаков М. Н. Binary Predicate, Transitive Closure, Two-Three Variables: Shall We Play Dominoes? // Logicheskie Issledovaniya / Logical Investigations. 2023. VOL. 29. № 1. C. 114-146.
Issue
Section
Symbolic Logic
Copyright (c) 2023 Михаил Николаевич Рыбаков
This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License.
##plugins.generic.funding.fundingData##
-
Russian Science Foundation
##plugins.generic.funding.funderGrants## 21-18-00195
References
Агаджанян, Рыбаков, 2022 – Агаджанян И.А., Рыбаков М.Н. Сложность константного фрагмента слабой логики Гжегорчика. 2022. URL: arXiv: 2211.14571 (дата обращения: 11.03.2023).
Александров и др., 2021 – Александров К.И., Рыбаков М.Н., Шкатов Д.П. Сложность фрагментов произведений с логикой Т в языке с одной переменной. 2021. URL: arXiv: 2112.03833 (дата обращения: 10.04.2023).
Булос, Джеффри, 1994 – Булос Дж., Джеффри Р. Вычислимость и логика. М.: Мир, 1994. (Перевод книги: Boolos G.S., Jeffrey R.C. Computability and Logic. Cambridge University Press, third edition, 1989.)
Котикова, Рыбаков, 2016 – Котикова Е.А., Рыбаков М.Н. Моделирование арифметики в языке первого порядка, обогащенном темпоральными кванторами // Вестник ТвГУ. Серия: Прикладная математика. 2016. № 4. С. 5–19.
Маслов и др., 1965 – Маслов С.Ю., Минц Г.Е., Оревков В.П. Неразрешимость в конструктивном исчислении предикатов некоторых классов формул, содержащих только одноместные предикатные переменные // Доклады АН СССР. 1965. Т. 163. № 2. С. 295–297.
Рыбаков, 2001 – Рыбаков М.Н. Перечислимость модальных предикатных логик и условия обрыва возрастающих цепей // Логические исследования. 2001. Вып. 8. С. 155–167.
Рыбаков, 2002 – Рыбаков М.Н. Об алгоритмической выразительности модального языка с одной лишь одноместной предикатной буквой // Логические исследования. 2002. Вып. 9. С. 179–201.
Рыбаков, 2007 – Рыбаков М.Н. Сложность константного фрагмента пропозициональной динамической логики // Вестник ТвГУ. Серия: Прикладная математика. 2007. № 5. С. 5–17.
Рыбаков, 2014 – Рыбаков М.Н. Неразрешимость логики квазиарных предикатов // Вестник ТвГУ. Серия: Прикладная математика. 2014. № 4. С. 17–32.
Рыбаков, 2017 – Рыбаков М.Н. Неразрешимость модальных логик одноместного предиката // Логические исследования. 2017. Т. 23. № 2. С. 60–75.
Рыбаков, 2018a – Рыбаков М.Н. Аксиоматизируемость ненормальных и квазинормальных модальных предикатных логик первопорядково определимых классов шкал Крипке // Вестник ТвГУ. Серия: Прикладная математика. 2018. № 3. С. 81–94.
Рыбаков, 2018b – Рыбаков М.Н. Алгоритмические свойства линейно аппроксимируемых квазинормальных модальных логик // Вестник ТвГУ. Серия: Прикладная математика. 2018. № 4. С. 87–97.
Рыбаков, 2021 – Рыбаков М.Н. Сложность проблемы равенства слов в многообразиях модальных алгебр // Вестник ТвГУ. Серия: Прикладная математика. 2021. № 3. С. 5–17.
Рыбаков, 2022 – Рыбаков М.Н. Алгоритмическая сложность теорий бинарного предиката в языках с малым числом переменных // Доклады Российской академии наук. Математика, информатика, процессы управления. 2022. Т. 507. № 6. С. 61–65.
Рыбаков, 2023 – Рыбаков М.Н. Деревья как средство моделирования неразрешимых проблем // Вестник ТвГУ. Серия: Прикладная математика. 2023. № 1. С. 5–23.
Рыбаков, Чагров, 2000 – Рыбаков М.Н., Чагров А.В. Стандартные переводы неклассических формул и относительная разрешимость логик // Труды научно-исследовательского семинара Логического центра Института философии РАН, XIV. М.: Институт философии РАН, 2000. С. 81–98.
Трахтенброт, 1950 – Трахтенброт Б.А. Невозможность алгорифма для проблемы разрешимости на конечных классах // Доклады АН СССР. 1950. Т. 70. № 4. С. 569–572.
Трахтенброт, 1953 – Трахтенброт Б.А. О рекурсивной отделимости // Доклады АН СССР. 1953. Т. 88. № 6. С. 953–956.
Balbiani, Tinchev, 2014 – Balbiani P., Tinchev T. Definability and computability for PRSPDL // In Advances in Modal Logic. 2014. Vol. 10. P. 16–33.
Berger, 1966 – Berger R. The Undecidability of the Domino Problem // Volume 66 of Memoirs of AMS. AMS, 1966.
Bianchi, Montagna, 2015 – Bianchi M., Montagna F. Trakhtenbrot theorem and first-order axiomatic extensions of MTL // Studia Logica. 2015. Vol. 103. P. 1163–1181.
Boolos et al., 2007 – Boolos G.S., Burgess J.P., Jeffrey R.C. Computability and Logic. Cambridge University Press, fifth edition, 2007.
Börger et al., 1997 – Börger E., Grädel E., Gurevich Y. The Classical Decision Problem. Springer, 1997.
Chagrov, Rybakov, 2003 – Chagrov A., Rybakov M. How many variables does one need to prove PSPACE-hardness of modal logics? // P. Balbiani, N.-Y. Suzuki, F. Wolter, M. Zakharyaschev (eds.). Advances in Modal Logic. 2003. Vol. 4. P. 71–82.
Chagrov, Zakharyaschev, 1997 – Chagrov A., Zakharyaschev M. Modal Logic. Oxford University Press, 1997.
Church, 1936 – Church A. A note on the “Entscheidungsproblem” // The Journal of Symbolic Logic. 1936. Vol. 1. P. 40–41.
Gabbay, Shehtman, 1993 – Gabbay D., Shehtman V. Undecidability of modal and intermediate first-order logics with two individual variables // The Journal of Symbolic Logic. 1993. Vol. 58. No. 3. P. 800–823.
Gabbay et al., 2009 – Gabbay D., Shehtman V., Skvortsov D. Quantification in Nonclassical Logic. Vol. 1. Series: Studies in Logic and the Foundations of Mathematics. Vol. 153. Elsevier, 2009. 640 p.
Gabelaia et al., 2005 – Gabelaia D., Kurucz A., Wolter F., Zakharyaschev M. Products of “transitive” modal logics // The Journal of Symbolic Logic. 2005. Vol. 70. No. 3. P. 993–1021.
Grädel, 1999 – Grädel E. On the restraining power of guards // Journal of Symbolic Logic. 1999. Vol. 64. No. 4. P. 1719–1742.
Grädel et al., 1997 – Grädel E., Kolaitis P.G., Vardi M.Y. On the decision problem for two-variable first-order logic // Bulletin of Symbolic Logic. 1997. Vol. 3. No. 1. P. 53–69.
Grädel et al., 1999 – Grädel E., Otto M., Rosen E. Undecidability results on twovariable logics // Archive for Mathematical Logic. 1999. Vol. 38. P. 313–354.
Hájek, 1998 – Hájek P. Trakhtenbrot theorem and fuzzy logic // G. Gottlob, E. Grandjean, and K. Seyr (eds.). International Workshop on Computer Science Logic. CSL98. Vol. 1584 of Lecture Notes in Computer Science. 1998. P. 1–8.
Halpern, 1995 – Halpern J.Y. The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic // Artificial Intelligence. 1995. Vol. 75. No. 2. P. 361–372.
Harel, 1986 – Harel D. Effective transformations on infinite trees, with applications to high undecidability, dominoes, and fairness // Journal of the ACM. 1986. Vol. 33. P. 224–248.
Hirsch et al., 2002 – Hirsch R., Hodkinson I., Kurucz A. On modal logics between K × K × K and S5 × S5 × S5 // The Journal of Symbolic Logic. 2002. Vol. 67. No. 1. P. 221–234.
Hodkinson et al., 2000 – Hodkinson I., Wolter F., Zakharyaschev M. Decidable fragments of first-order temporal logics // Annals of Pure and Applied Logic. 2000. Vol. 106. P. 85–134.
Hodkinson et al., 2001 – Hodkinson I., Wolter F., Zakharyaschev M. Monodic fragments of first-order temporal logics: 2000–2001 A.D. // R. Nieuwenhuis and A. Voronkov (eds.). Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2001. Vol. 2250 of Lecture Notes in Computer Science. Springer, 2001. P. 1–23.
Kontchakov et al., 2005 – Kontchakov R., Kurucz A., Zakharyaschev M. Undecidability of first-order intuitionistic and modal logics with two variables // Bulletin of Symbolic Logic. 2005. Vol. 11. No. 3. P. 428–438.
Kotikova, Rybakov, 2013 – Kotikova E., Rybakov M. First-order logics of branching time: on expressive power of temporal operators // Logical Investigations. 2013. Vol. 19. P. 68–99.
Kremer, 1997 – Kremer P. On the complexity of propositional quantification in intuitionistic logic // The Journal of Symbolic Logic. 1997. Vol. 62. No. 2. P. 529–544.
Kripke, 1962 – Kripke S. The undecidability of monadic modal quantification theory // Zeitschrift f¨ur Matematische Logik und Grundlagen der Mathematik. 1962. Vol. 8. P. 113–116.
Libkin, 2004 – Libkin L. Elements of Finite Model Theory. Springer, 2004.
Mortimer, 1975 – Mortimer M. On languages with two variables // Zeitschrift f¨ur Mathematische Logik und Grundlagen der Mathematik. 1975. P. 135–140.
Motohashi, 1990 – Motohashi N. A decision method for a set of first order classical formulas and its applications to decision problem for non-classical propositional logics // J. Math. Soc. Japan. 1990. Vol. 42. No. 1. P. 127–132.
Nerode, Shore, 1980 – Nerode A., Shore R. A. Second order logic and first order theories of reducibility ordering // J. Barwise, H.J. Keisler, and K. Kunen (eds.). The Kleene Symposium. 1980. P. 181–200.
Nies, 1996 – Nies A. Undecidable fragments of elementary theories // Algebra Universalis. 1996. Vol. 35. P. 8–33.
Papadimitriou, 1994 – Papadimitriou C.H.Computational Complexity. Addison-Wesley, 1994. 523 p.
Reynolds, Zakharyaschev, 2001 – Reynolds M., Zakharyaschev M. On the products of linear modal logics // Journal of Logic and Computation. 2011. Vol. 11. No. 6. P. 909–931.
Rogers, 1967 – Rogers H. Theory of Recursive Functions and Effective Computability. McGraw-Hill, 1967.
Rybakov, 2006 – Rybakov M. Complexity of intuitionistic and Visser’s basic and formal logics in finitely many variables // G. Governatori, I.M. Hodkinson, and Y. Venema (eds.). Advances in Modal Logic 6. 2006. P. 393–411.
Rybakov, 2007 – Rybakov M. Complexity of finite-variable fragments of EXPTIMEcomplete logics // Journal of Applied Non-classical Logics. 2007. Vol. 17. No. 3. P. 359–382.
Rybakov, 2008 – Rybakov M. Complexity of intuitionistic propositional logic and its fragments // Journal of Applied Non-Classical Logics. 2008. Vol. 18. No. 2–3. P. 267–292.
Rybakov, 2023 – Rybakov M. Predicate counterparts of modal logics of provability:иHigh undecidability and Kripke incompleteness // To appear in Logic Journal of the IGPL (DOI: 10.1093/jigpal/jzad002).
Rybakov, Shkatov, 2019a – Rybakov M., Shkatov D. Trakhtenbrot theorem for classical languages with three individual variables // Proceedings of SAICSIT2019. ACM, 2019. Article No. 19.
Rybakov, Shkatov, 2019b – Rybakov M., Shkatov D. Undecidability of first-order modal and intuitionistic logics with two variables and one monadic predicate letter // Studia Logica. 2019. Vol. 107. No. 4. P. 695–717.
Rybakov, Shkatov, 2020 – Rybakov M., Shkatov D. Algorithmic properties of first-order modal logics of finite Kripke frames in restricted languages // Journal of Logic and Computation. 2020. Vol. 30. No. 7. P. 1305–1329.
Rybakov, Shkatov, 2021a – Rybakov M., Shkatov D. Algorithmic properties of first-order superintuitionistic logics of finite Kripke frames in restricted languages // Journal of Logic and Computation. 2021. Vol. 31. No. 2. P. 494–522.
Rybakov, Shkatov, 2021b – Rybakov M., Shkatov D. Complexity of finite-variable fragments of products with K // Journal of Logic and Computation. 2021. Vol. 31. No. 2. P. 426–443.
Rybakov, Shkatov, 2021c – Rybakov M., Shkatov D. Undecidability of QLTL and QCTL with two variables and one monadic predicate letter // Logical Investigations. 2021. Vol. 27. No. 2. P. 93–120.
Rybakov, Shkatov, 2021d – Rybakov M., Shkatov D. Algorithmic properties of first-order modal logics of linear Kripke frames in restricted languages // Journal of Logic and Computation. 2021. Vol. 31. No. 5. P. 1266–1288.
Rybakov, Shkatov, 2022a – Rybakov M., Shkatov D. Complexity of finite-variable fragments of products with non-transitive modal logics // Journal of Logic and Computation. 2022. Vol. 32. No. 5. P. 853–870.
Rybakov, Shkatov, 2022b – Rybakov M., Shkatov D. Undecidability of the logic of partial quasiary predicates // Logic Journal of the IGPL. 2022. Vol. 30. No. 3. P. 519–533.
Sipser, 2013 – Sipser M. Introduction to the Theory of Computation. Cengage Learning, 3rd edition, 2013. 504 p.
Spaan, 1993 – Spaan E. Complexity of Modal Logics. PhD Thesis. Amsterdam, 1993. Speranski, 2016 – Speranski S. A note on hereditarily Π 1 0 - and Σ 1 0 -complete sets of sentences // Journal of Logic and Computation. 2016. Vol. 26. No. 5. P. 1729–1741.
Surányi, 1943 – Surányi J. Zur Reduktion des Entscheidungsproblems des logischen Funktioskalk¨uls // Mathematikai ´es Fizikai Lapok. 1943. Vol. 50. P. 51–74.
Tarski, Givant, 1987 – Tarski A., Givant S. A Formalization of Set Theory without Variables. American Mathematical Society, 1987. 318 p.
Turing, 1936 – Turing A.M. On computable numbers, with an application to the “Entscheidungsproblem” // Proceedings of the London Mathematical Society, 2 series, 1936. Vol. 42. P. 230–265.
Urquhart, 1984 – Urquhart A. The undecidability of entailment and relevant implication // Journal of Symbolic Logic. 1984. Vol. 49. No. 4. P. 1059–1073.
Urquhart, 2007 – Urquhart A. Four variables suffice // The Australasian Journal of Logic. 2007. Vol. 5. P. 66–73.
Wolter, Zakharyaschev, 2001 – Wolter F., Zakharyaschev M. Decidable fragments of first-order modal logics // The Journal of Symbolic Logic. 2001. Vol. 66. P. 1415–1438.
Александров и др., 2021 – Александров К.И., Рыбаков М.Н., Шкатов Д.П. Сложность фрагментов произведений с логикой Т в языке с одной переменной. 2021. URL: arXiv: 2112.03833 (дата обращения: 10.04.2023).
Булос, Джеффри, 1994 – Булос Дж., Джеффри Р. Вычислимость и логика. М.: Мир, 1994. (Перевод книги: Boolos G.S., Jeffrey R.C. Computability and Logic. Cambridge University Press, third edition, 1989.)
Котикова, Рыбаков, 2016 – Котикова Е.А., Рыбаков М.Н. Моделирование арифметики в языке первого порядка, обогащенном темпоральными кванторами // Вестник ТвГУ. Серия: Прикладная математика. 2016. № 4. С. 5–19.
Маслов и др., 1965 – Маслов С.Ю., Минц Г.Е., Оревков В.П. Неразрешимость в конструктивном исчислении предикатов некоторых классов формул, содержащих только одноместные предикатные переменные // Доклады АН СССР. 1965. Т. 163. № 2. С. 295–297.
Рыбаков, 2001 – Рыбаков М.Н. Перечислимость модальных предикатных логик и условия обрыва возрастающих цепей // Логические исследования. 2001. Вып. 8. С. 155–167.
Рыбаков, 2002 – Рыбаков М.Н. Об алгоритмической выразительности модального языка с одной лишь одноместной предикатной буквой // Логические исследования. 2002. Вып. 9. С. 179–201.
Рыбаков, 2007 – Рыбаков М.Н. Сложность константного фрагмента пропозициональной динамической логики // Вестник ТвГУ. Серия: Прикладная математика. 2007. № 5. С. 5–17.
Рыбаков, 2014 – Рыбаков М.Н. Неразрешимость логики квазиарных предикатов // Вестник ТвГУ. Серия: Прикладная математика. 2014. № 4. С. 17–32.
Рыбаков, 2017 – Рыбаков М.Н. Неразрешимость модальных логик одноместного предиката // Логические исследования. 2017. Т. 23. № 2. С. 60–75.
Рыбаков, 2018a – Рыбаков М.Н. Аксиоматизируемость ненормальных и квазинормальных модальных предикатных логик первопорядково определимых классов шкал Крипке // Вестник ТвГУ. Серия: Прикладная математика. 2018. № 3. С. 81–94.
Рыбаков, 2018b – Рыбаков М.Н. Алгоритмические свойства линейно аппроксимируемых квазинормальных модальных логик // Вестник ТвГУ. Серия: Прикладная математика. 2018. № 4. С. 87–97.
Рыбаков, 2021 – Рыбаков М.Н. Сложность проблемы равенства слов в многообразиях модальных алгебр // Вестник ТвГУ. Серия: Прикладная математика. 2021. № 3. С. 5–17.
Рыбаков, 2022 – Рыбаков М.Н. Алгоритмическая сложность теорий бинарного предиката в языках с малым числом переменных // Доклады Российской академии наук. Математика, информатика, процессы управления. 2022. Т. 507. № 6. С. 61–65.
Рыбаков, 2023 – Рыбаков М.Н. Деревья как средство моделирования неразрешимых проблем // Вестник ТвГУ. Серия: Прикладная математика. 2023. № 1. С. 5–23.
Рыбаков, Чагров, 2000 – Рыбаков М.Н., Чагров А.В. Стандартные переводы неклассических формул и относительная разрешимость логик // Труды научно-исследовательского семинара Логического центра Института философии РАН, XIV. М.: Институт философии РАН, 2000. С. 81–98.
Трахтенброт, 1950 – Трахтенброт Б.А. Невозможность алгорифма для проблемы разрешимости на конечных классах // Доклады АН СССР. 1950. Т. 70. № 4. С. 569–572.
Трахтенброт, 1953 – Трахтенброт Б.А. О рекурсивной отделимости // Доклады АН СССР. 1953. Т. 88. № 6. С. 953–956.
Balbiani, Tinchev, 2014 – Balbiani P., Tinchev T. Definability and computability for PRSPDL // In Advances in Modal Logic. 2014. Vol. 10. P. 16–33.
Berger, 1966 – Berger R. The Undecidability of the Domino Problem // Volume 66 of Memoirs of AMS. AMS, 1966.
Bianchi, Montagna, 2015 – Bianchi M., Montagna F. Trakhtenbrot theorem and first-order axiomatic extensions of MTL // Studia Logica. 2015. Vol. 103. P. 1163–1181.
Boolos et al., 2007 – Boolos G.S., Burgess J.P., Jeffrey R.C. Computability and Logic. Cambridge University Press, fifth edition, 2007.
Börger et al., 1997 – Börger E., Grädel E., Gurevich Y. The Classical Decision Problem. Springer, 1997.
Chagrov, Rybakov, 2003 – Chagrov A., Rybakov M. How many variables does one need to prove PSPACE-hardness of modal logics? // P. Balbiani, N.-Y. Suzuki, F. Wolter, M. Zakharyaschev (eds.). Advances in Modal Logic. 2003. Vol. 4. P. 71–82.
Chagrov, Zakharyaschev, 1997 – Chagrov A., Zakharyaschev M. Modal Logic. Oxford University Press, 1997.
Church, 1936 – Church A. A note on the “Entscheidungsproblem” // The Journal of Symbolic Logic. 1936. Vol. 1. P. 40–41.
Gabbay, Shehtman, 1993 – Gabbay D., Shehtman V. Undecidability of modal and intermediate first-order logics with two individual variables // The Journal of Symbolic Logic. 1993. Vol. 58. No. 3. P. 800–823.
Gabbay et al., 2009 – Gabbay D., Shehtman V., Skvortsov D. Quantification in Nonclassical Logic. Vol. 1. Series: Studies in Logic and the Foundations of Mathematics. Vol. 153. Elsevier, 2009. 640 p.
Gabelaia et al., 2005 – Gabelaia D., Kurucz A., Wolter F., Zakharyaschev M. Products of “transitive” modal logics // The Journal of Symbolic Logic. 2005. Vol. 70. No. 3. P. 993–1021.
Grädel, 1999 – Grädel E. On the restraining power of guards // Journal of Symbolic Logic. 1999. Vol. 64. No. 4. P. 1719–1742.
Grädel et al., 1997 – Grädel E., Kolaitis P.G., Vardi M.Y. On the decision problem for two-variable first-order logic // Bulletin of Symbolic Logic. 1997. Vol. 3. No. 1. P. 53–69.
Grädel et al., 1999 – Grädel E., Otto M., Rosen E. Undecidability results on twovariable logics // Archive for Mathematical Logic. 1999. Vol. 38. P. 313–354.
Hájek, 1998 – Hájek P. Trakhtenbrot theorem and fuzzy logic // G. Gottlob, E. Grandjean, and K. Seyr (eds.). International Workshop on Computer Science Logic. CSL98. Vol. 1584 of Lecture Notes in Computer Science. 1998. P. 1–8.
Halpern, 1995 – Halpern J.Y. The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic // Artificial Intelligence. 1995. Vol. 75. No. 2. P. 361–372.
Harel, 1986 – Harel D. Effective transformations on infinite trees, with applications to high undecidability, dominoes, and fairness // Journal of the ACM. 1986. Vol. 33. P. 224–248.
Hirsch et al., 2002 – Hirsch R., Hodkinson I., Kurucz A. On modal logics between K × K × K and S5 × S5 × S5 // The Journal of Symbolic Logic. 2002. Vol. 67. No. 1. P. 221–234.
Hodkinson et al., 2000 – Hodkinson I., Wolter F., Zakharyaschev M. Decidable fragments of first-order temporal logics // Annals of Pure and Applied Logic. 2000. Vol. 106. P. 85–134.
Hodkinson et al., 2001 – Hodkinson I., Wolter F., Zakharyaschev M. Monodic fragments of first-order temporal logics: 2000–2001 A.D. // R. Nieuwenhuis and A. Voronkov (eds.). Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2001. Vol. 2250 of Lecture Notes in Computer Science. Springer, 2001. P. 1–23.
Kontchakov et al., 2005 – Kontchakov R., Kurucz A., Zakharyaschev M. Undecidability of first-order intuitionistic and modal logics with two variables // Bulletin of Symbolic Logic. 2005. Vol. 11. No. 3. P. 428–438.
Kotikova, Rybakov, 2013 – Kotikova E., Rybakov M. First-order logics of branching time: on expressive power of temporal operators // Logical Investigations. 2013. Vol. 19. P. 68–99.
Kremer, 1997 – Kremer P. On the complexity of propositional quantification in intuitionistic logic // The Journal of Symbolic Logic. 1997. Vol. 62. No. 2. P. 529–544.
Kripke, 1962 – Kripke S. The undecidability of monadic modal quantification theory // Zeitschrift f¨ur Matematische Logik und Grundlagen der Mathematik. 1962. Vol. 8. P. 113–116.
Libkin, 2004 – Libkin L. Elements of Finite Model Theory. Springer, 2004.
Mortimer, 1975 – Mortimer M. On languages with two variables // Zeitschrift f¨ur Mathematische Logik und Grundlagen der Mathematik. 1975. P. 135–140.
Motohashi, 1990 – Motohashi N. A decision method for a set of first order classical formulas and its applications to decision problem for non-classical propositional logics // J. Math. Soc. Japan. 1990. Vol. 42. No. 1. P. 127–132.
Nerode, Shore, 1980 – Nerode A., Shore R. A. Second order logic and first order theories of reducibility ordering // J. Barwise, H.J. Keisler, and K. Kunen (eds.). The Kleene Symposium. 1980. P. 181–200.
Nies, 1996 – Nies A. Undecidable fragments of elementary theories // Algebra Universalis. 1996. Vol. 35. P. 8–33.
Papadimitriou, 1994 – Papadimitriou C.H.Computational Complexity. Addison-Wesley, 1994. 523 p.
Reynolds, Zakharyaschev, 2001 – Reynolds M., Zakharyaschev M. On the products of linear modal logics // Journal of Logic and Computation. 2011. Vol. 11. No. 6. P. 909–931.
Rogers, 1967 – Rogers H. Theory of Recursive Functions and Effective Computability. McGraw-Hill, 1967.
Rybakov, 2006 – Rybakov M. Complexity of intuitionistic and Visser’s basic and formal logics in finitely many variables // G. Governatori, I.M. Hodkinson, and Y. Venema (eds.). Advances in Modal Logic 6. 2006. P. 393–411.
Rybakov, 2007 – Rybakov M. Complexity of finite-variable fragments of EXPTIMEcomplete logics // Journal of Applied Non-classical Logics. 2007. Vol. 17. No. 3. P. 359–382.
Rybakov, 2008 – Rybakov M. Complexity of intuitionistic propositional logic and its fragments // Journal of Applied Non-Classical Logics. 2008. Vol. 18. No. 2–3. P. 267–292.
Rybakov, 2023 – Rybakov M. Predicate counterparts of modal logics of provability:иHigh undecidability and Kripke incompleteness // To appear in Logic Journal of the IGPL (DOI: 10.1093/jigpal/jzad002).
Rybakov, Shkatov, 2019a – Rybakov M., Shkatov D. Trakhtenbrot theorem for classical languages with three individual variables // Proceedings of SAICSIT2019. ACM, 2019. Article No. 19.
Rybakov, Shkatov, 2019b – Rybakov M., Shkatov D. Undecidability of first-order modal and intuitionistic logics with two variables and one monadic predicate letter // Studia Logica. 2019. Vol. 107. No. 4. P. 695–717.
Rybakov, Shkatov, 2020 – Rybakov M., Shkatov D. Algorithmic properties of first-order modal logics of finite Kripke frames in restricted languages // Journal of Logic and Computation. 2020. Vol. 30. No. 7. P. 1305–1329.
Rybakov, Shkatov, 2021a – Rybakov M., Shkatov D. Algorithmic properties of first-order superintuitionistic logics of finite Kripke frames in restricted languages // Journal of Logic and Computation. 2021. Vol. 31. No. 2. P. 494–522.
Rybakov, Shkatov, 2021b – Rybakov M., Shkatov D. Complexity of finite-variable fragments of products with K // Journal of Logic and Computation. 2021. Vol. 31. No. 2. P. 426–443.
Rybakov, Shkatov, 2021c – Rybakov M., Shkatov D. Undecidability of QLTL and QCTL with two variables and one monadic predicate letter // Logical Investigations. 2021. Vol. 27. No. 2. P. 93–120.
Rybakov, Shkatov, 2021d – Rybakov M., Shkatov D. Algorithmic properties of first-order modal logics of linear Kripke frames in restricted languages // Journal of Logic and Computation. 2021. Vol. 31. No. 5. P. 1266–1288.
Rybakov, Shkatov, 2022a – Rybakov M., Shkatov D. Complexity of finite-variable fragments of products with non-transitive modal logics // Journal of Logic and Computation. 2022. Vol. 32. No. 5. P. 853–870.
Rybakov, Shkatov, 2022b – Rybakov M., Shkatov D. Undecidability of the logic of partial quasiary predicates // Logic Journal of the IGPL. 2022. Vol. 30. No. 3. P. 519–533.
Sipser, 2013 – Sipser M. Introduction to the Theory of Computation. Cengage Learning, 3rd edition, 2013. 504 p.
Spaan, 1993 – Spaan E. Complexity of Modal Logics. PhD Thesis. Amsterdam, 1993. Speranski, 2016 – Speranski S. A note on hereditarily Π 1 0 - and Σ 1 0 -complete sets of sentences // Journal of Logic and Computation. 2016. Vol. 26. No. 5. P. 1729–1741.
Surányi, 1943 – Surányi J. Zur Reduktion des Entscheidungsproblems des logischen Funktioskalk¨uls // Mathematikai ´es Fizikai Lapok. 1943. Vol. 50. P. 51–74.
Tarski, Givant, 1987 – Tarski A., Givant S. A Formalization of Set Theory without Variables. American Mathematical Society, 1987. 318 p.
Turing, 1936 – Turing A.M. On computable numbers, with an application to the “Entscheidungsproblem” // Proceedings of the London Mathematical Society, 2 series, 1936. Vol. 42. P. 230–265.
Urquhart, 1984 – Urquhart A. The undecidability of entailment and relevant implication // Journal of Symbolic Logic. 1984. Vol. 49. No. 4. P. 1059–1073.
Urquhart, 2007 – Urquhart A. Four variables suffice // The Australasian Journal of Logic. 2007. Vol. 5. P. 66–73.
Wolter, Zakharyaschev, 2001 – Wolter F., Zakharyaschev M. Decidable fragments of first-order modal logics // The Journal of Symbolic Logic. 2001. Vol. 66. P. 1415–1438.