Бинарный предикат, транзитивное замыкание, две-три переменные: сыграем в домино?
Article Sidebar
Опубликован:
27.05.2023
Ключевые слова:
логика предикатов, бинарный предикат, неразрешимость
Main Article Content
Аннотация
Проблемы укладки домино являются удобным инструментом оценки алгоритмической сложности задач, возникающих в различных разделах математики, в том числе в логике. В работе описывается моделирование проблем домино с помощью средств языка логики предикатов, а также с помощью некоторых дополнительных средств, в том числе не выразимых элементарно. Это дает возможность получить как простые доказательства уже известных фактов о неразрешимости проблемы выполнимости формул различных фрагментов логики предикатов, так и некоторые новые результаты. Так, известно, что проблема выполнимости формул логики предикатов, содержащих не более двух предметных переменных, алгоритмически разрешима; известно также, что свойство транзитивности бинарного отношения и операция композиции двух бинарных отношений могут быть выражены в языке первого порядка с использованием трех переменных. В работе показано, что если добавить к языку первого порядка оператор проверки транзитивности бинарного отношения (или более сильное средство – оператор транзитивного замыкания) и оператор композиции, то получим язык с сильно неразрешимой проблемой выполнимости формул от двух переменных, построенных в сигнатуре с одной бинарной предикатной буквой и равенством.
Скачивания
Данные скачивания пока не доступны.
Article Details
Как цитировать
Рыбаков М. Н. Бинарный предикат, транзитивное замыкание, две-три переменные: сыграем в домино? // Логические исследования / Logical Investigations. 2023. Т. 29. № 1. C. 114-146.
Выпуск
Раздел
Символическая логика
Copyright (c) 2023 Михаил Николаевич Рыбаков
Это произведение доступно по лицензии Creative Commons «Attribution-NonCommercial» («Атрибуция — Некоммерческое использование») 4.0 Всемирная.
Данные о финансировании
-
Russian Science Foundation
Номер гранта 21-18-00195
Литература
Агаджанян, Рыбаков, 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.