Undecidability of QLTL and QCTL with two variables and one monadic predicate letter
Article Sidebar
Опубликован:
19.12.2021
Main Article Content
Аннотация
We study the algorithmic properties of the quantified linear-time temporal logic QLTL in languages with restrictions on the number of individual variables as well as the number and arity of predicate letters. We prove that the satisfiability problem for QLTL in languages with two individual variables and one monadic predicate letter in Σ 11 -hard. Thus, QLTL is Π 11 -hard, and so not recursively enumerable, in such languages. The result
holds both for the increasing domain and the constant domain semantics and is obtained by reduction from a Σ 11 -hard N×N recurrent tiling problem. It follows from the proof for QLTL that similar results hold for the quantified branching-time temporal logic QCTL, and hence for the quantified alternating-time temporal logic QATL. The result presented in this paper strengthens a result by I. Hodkinson, F. Wolter, and M. Zakharyaschev, who have shown that the satisfiability problem for QLTL is Σ 11 -hard in languages with two individual variables
and an unlimited supply of monadic predicate letters.
Скачивания
Данные скачивания пока не доступны.
Article Details
Как цитировать
Rybakov M., Shkatov D. Undecidability of QLTL and QCTL with two variables and one monadic predicate letter // Логические исследования / Logical Investigations. 2021. Т. 27. № 2. C. 93-120.
Выпуск
Раздел
Неклассические логики
Copyright (c) 2021 Dmitry Shkatov, Mikhail Rybakov
Это произведение доступно по лицензии Creative Commons «Attribution-NonCommercial» («Атрибуция — Некоммерческое использование») 4.0 Всемирная.
Литература
Abadi, 1989 – Abadi, M. “The power of temporal proofs”, Theoretical Computer Science, 1989, Vol. 65, No. 1, pp. 35–83.
Abiteboul, 1996 – Abiteboul, S., Herr, L., Van den Bussche, J. “Temporal versus first-order logic to query temporal databases”, in: Proceedings of the 15th International Conference on Principles of Databases (PODS ’96), 1996.
Ajspur et al., 2013 – Ajspur, M., Goranko, V., Shkatov, D. “Tableau-based decision procedure for the multiagent epistemic logic with all coalitional operators for common and distributed knowledge”, Logic Journal of the IGPL, 2013, Vol. 21, No. 3, pp. 407–437.
Alechina, Shkatov, 2006 – Alechina, N., Shkatov, D. “A general method for proving decidability of intuitionistic modal logics”, Journal of Applied Logic, 2006, Vol. 4, No. 3, pp. 219–230.
Alur et al., 2002 – Alur, R., Henzinger, T.A., Kuperman, O. “Alternating-Time temporal logic”, Journal of ACM, 2002, Vol. 49, No. 5, pp. 672–713.
Andr´eka et al., 1979 – Andr´eka, H., N´emeti, I., Sain, I. “Completeness problems in verification of programs and program schemes”, in: Mathematical Foundations of Computer Science 1979. MFCS 1979, ed. by J. Beˇcv´aˇr, Vol. 74 of Lecture Notes in Computer Science. Springer, 1979.
Artale, Franconi, 2000 – Artale, A., Franconi, E. “A survey of temporal extensions of description logics”, Annals of Mathematics and Artificial Intelligence, 2000, Vol. 30, pp. 171–210.
Artale et al., 2004 – Artale, A., Kontchakov, R., Kovtunova, A., Ryzhikov, V., Wolter, F., Zakharyaschev, M. “First-order rewritability of ontologymediated queries in linear temporal logic”, 2020. Preprint available at https://arxiv.org/abs/2004.07221
Artemov, Dzhaparidze, 1990 – Artemov, S., Dzhaparidze, G. “Finite Kripke models and predicate logics of provability”, The Journal of Symbolic Logic, 1990, Vol. 55, No. 3, pp. 1090–1098.
Baader et al., 2015 – Baader, F., Borgwardt, S., Lippmann, M. “Temporal query entailment in the description logic SHQ”, Journal of Web Semantics, 2015, Vol. 33, pp. 71–93.
Baader et al., 2012 – Baader, F., Ghilardi, S., Lutz, C. “Ltl over description logic axioms”, ACM Transactions on Computational Logic, 2012, Vol. 13, No. 3, Article 21.
Balbiani et al., 2019 – Balbiani, P., Boudou, J., Di´eguez, M., Fern´andez-Duque, D. “Intuitionistic linear temporal logics”, 2019, ACM Transactions on Computational Logic, Vol. 21, Article 14.
B¨orger et al., 1997 – B¨orger, E., Gr¨adel, E., Gurevich, Y. The Classical Decision Problem. Springer, 1997.
Borgwardt et al., 2015 – Borgwardt, S., Lippmann, M., Thost, V. “Temporalizing rewritable query languages over knowledge bases”, Journal of Web Semantics, 2015, Vol. 33, pp. 50–70.
Boudou et al., 2017 – Boudou, J., Di´eguez, M., Fern´andez-Duque D. “A decidable intuitionistic temporal logic”, in: Proceedings of the 26th EACSL Annual Conference on Computer Science Logic (CSL’17), 2017, Vol. 82, pp. 14:1–14:17.
Boudou et al., 2019 – Boudou, J., Di´eguez, M., Fern´andez-Duque, D., Romero F. “Axiomatic systems and topological semantics for intuitionistic temporal logic”, in: F. Calimeri, N. Leone, M. Manna (eds.), Logics in Artificial Intelligence. JELIA 2019, Vol. 11468 of Lecture Notes in Computer Science. Springer, 2019, pp. 763–777.
Bourgaux et al., 2019 – Bourgaux, C., Koopmann, P., Turhan, A.-Y. “Ontologymediated query answering over temporal and inconsistent data”, Semantic Web Journal, 2019, Vol. 10, pp. 475–521.
Bra¨uner, Ghilardi, 2007 – Bra¨uner, T., Ghilardi, S. “First-order modal logic”, in:
P. Blackburn, J. Van Benthem, F. Wolter (eds.), Handbook of Modal Logic, Vol. 3 of Studies in Logic and Practical Reasoning. Elsevier, 2007, pp. 549–620.
Brewka et al., 2011 – Brewka, G., Eiter, T., Truszczy´nski, M. “Answer set programming at a glance”, Communications of the ACM, 2011, Vol. 54, No. 12, pp. 92–103.
Cerrito et al., 1999 – Cerrito, S., Mayer, M.C., Praud, S. “First order linear temporal logic over finite time structures”, in: H. Ganzinger, D. McAllester, A. Voronkov (eds.), Logic for Programming and Automated Reasoning. LPAR 1999, Vol. 1705 of Lecture Notes in Computer Science. Springer, 1999.
Chagrov, Rybakov, 2003 – Chagrov, A., Rybakov, M. “How many variables does one need to prove PSPACE-hardness of modal logics?” in: P. Balbiani, N.-Y. Suzuki, F. Wolter, M. Zakharyaschev (eds.), Advances in Modal Logic, Vol. 4. London: King’s College Publications, 2003, pp. 71–82.
Chomicki, 1994 – Chomicki, J. “Temporal query languages: A survey”, in: D.M. Gabbay and H.J. Ohlbach (eds.), Temporal Logic. ICTL 1994, Vol. 827 of Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence). Springer, 1994.
Chomicki, Niwinski, 1993 – Chomicki, J., Niwinski, D. “On the feasibility of checking temporal integrity constraints”, Journal of Computer and System Sciences, 1995, Vol. 51, No. 3, pp. 523–535.
Church, 1936 – Church, A. “A note on the ‘Entscheidungsproblem’”, The Journal of Symbolic Logic, 1936, Vol. 1, pp. 40–41.
Clarke et al., 2000 – Clarke, E.M., Grumberg, O., Peled, D.A. Model Checking. Cambridge: MIT Press, 2000.
Davies, Pfenning, 2001 – Davies, R., Pfenning, F. “A modal analysis of staged computation”, Journal of the ACM, 2001, Vol. 48, No. 3, pp. 555–604.
Davies, 2017 – Davies, R. “A temporal logic approach to binding-time analysis”, Journal of the ACM, 2017, Vol. 64, No. 1, pp. 1–45.
Davoren, 2009 – Davoren, J.M. “On intuitionistic modal and tense logics and their classical companion logics: Topological semantics and bisimulations”, Annals of Pure and Applied Logic, 2009, Vol. 161, No. 3, pp. 349–367.
de Paiva et al., 2004 – de Paiva, V., Gor´e, R., Mendler, M. “Modalities in constructive logics and type theories”, Journal of Logic and Computation, 2004, Vol. 14, pp. 439–446.
Demri et al., 2016 – Demri, S., Goranko, V., Lange, M. Temporal Logics in Computer Science: Finite-state systems, Vol. 58 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016.
Di´eguez et al., 2018 – Di´eguez, M., Fern´andez-Duque, D. “An intuitionistic axiomatization of ‘eventually’” in: G. Metcalfe, G. Bezhanishvili, G. D’Agostino and T. Studer (eds.), Advances in Modal Logic, Vol. 12, College Publications, 2018, pp. 199–218.
Emerson, 1990 – Emerson, E.A. “Temporal and modal logic”, in: J. van Leeuwen (ed.), Handbook of Theoretical Computer Science, 1990, Vol. B, pp. 995–1072.
Emerson, Halpern, 1985 – Emerson, E.A., Halpern, J. “Decision procedures and expressiveness in temporal logic of branching time”, Journal of Computer and System Sciences, 1985, Vol. 30, No. 1, pp. 1–24.
Enderton, 2011 – Enderton, H.B. Computatbility Theory: An Introduction to Recursion Theory. New York: Academic Press, 2011.
Fagin et al., 1995 – Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y. Reasoning About Knowledge. Cambridge: MIT Press, 1995.
Fern´andez-Duque, 2018 – Fern´andez-Duque, D. “The intuitionistic temporal logic of dynamical systems”, Logical Methods in Computer Science, 2018, Vol. 14, No. 3, pp. 1–35.
Fischer, Ladner, 1979 – Fischer, M., Ladner, R.E. “Propositional dynamic logic of regular programs”, Journal of Computer and System Sciences, 1979, Vol. 18, pp. 194–211.
Fischer Servi, 1977 – Fischer Servi, G. “On modal logic with an intuitionistic base”, Studia Logica, 1977, Vol. 36, No. 3, pp. 141–149.
Fischer Servi, 1980 – Fischer Servi, G. “Semantics for a class of intuitionistic modal calculi”, in: M.L. Dalla Chiara (ed.), Italian Studies in the Philosophy of Science, pp. 59–72. Reidel; Dordrecht, 1980.
Fischer Servi, 1984 – Fischer Servi, G. “Axiomatizations for some intuitionistic modal logics”, Rendiconti del Seminario Matematico della Universit`a di Padova, 1984, Vol. 42, pp. 179–194.
Fitting, Mendelsohn, 1998 – Fitting, M., Mendelsohn, R.L. First-Order Modal Logic, Vol. 277 of Synthese Library. Dordrecht: Kluwer Academic Publishers, 1998. Gabbay, 1981 – Gabbay, D. Semantical Investigations in Heyting’s Intuitionistic Logic. Netherlands: D. Reidel, 1981.
Gabbay et al., 1994 – Gabbay, D., Hodkinson, I., Reynolds, M. Temporal Logic: Mathematical Foundations and Computational Aspects, Volume 1, Vol. 28 of Oxford Logic Guides. New York: Oxford University Press, 1994.
Gabbay et al., 2003 – Gabbay, D., Kurucz, A., Wolter, F., Zakharyaschev, M. ManyDimensional Modal Logics: Theory and Applications, Vol. 148 of Studies in Logic and the Foundations of Mathematics. Elsevier, 2003.
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, pp. 800–823.
Gabbay et al., 2009 – Gabbay, D., Shehtman, V., Skvortsov, D. Quantification in Nonclassical Logic, Volume 1, Vol. 153 of Studies in Logic and the Foundations of Mathematics. Elsevier, 2009.
Garson, 2001 – Garson, J.W. Quantification in modal logic. in: D.M. Gabbay and F. Guenthner (eds.), Handbook of Philosophical Logic, Vol. 3, pp. 267–323. Springer; Dordrecht, 2001.
Goldblatt, 1992 – Goldblatt, R. Logics of Time and Computation, Vol. 7 of CSLI Lecture Notes. Second edition. Stanford: Center for the Study of Language and Information, 1992.
Goldblatt, 2011 – Goldblatt, R. Quantifiers, Propositions and Identity: Admissible Semantics for Quantified Modal and Substructural Logics. Lecture Notes in Logic. Cambridge: Cambridge University Press, 2011.
Goranko, Shkatov, 2008 – Goranko, V., Shkatov, D. “Tableau-based decision procedures for the multi-agent epistemic logic with operators of common and distributed knowledge”, in: Proceedings of the Sixth International Conference on Software Engineering and Formal Methods, IEEE Press, 2008, pp. 237–246.
Goranko, Shkatov, 2009a – Goranko, V., Shkatov, D. “Tableau-based decision procedure for full coalitional multiagent temporal-epistemic logic of linear time”, in: S. Artemov and A. Nerode (eds.), International Symposium on Logical Foundations of Computer Science, 2009, pp. 197–213.
Goranko, Shkatov, 2009b – Goranko, V., Shkatov, D. “Tableau-based procedure for deciding satisfiability in the full coalitional multiagent epistemic logic”, in: C. Sierra, C. Castelfranchi, K.S. Decker, J. Sichman (eds.), Proceedings of 8th International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 09), 2009, pp. 969–976.
Goranko, Shkatov, 2009c – Goranko, V., Shkatov, D. “Tableau-based decision procedure for the full coalitional multiagent temporal-epistemic logic of branching time”, in: Proceedings of Formal Approaches to Multi-Agent Systems 2009, 2009.
Goranko, Shkatov, 2009d – Goranko, V., Shkatov, D. “Tableau-based decision procedures for logics of strategic ability in multiagent systems”, ACM Transactions on Computational Logic, 2009, Vol. 11, No. 1, pp. 3–51.
Goranko, van Drimmelen, 2006 – Goranko, V., Shkatov, D. “Complete axiomatization and decidability of the alternating-time temporal logic”, Theoretical Computer Science, 2006, Vol. 353, No. 1–3, pp. 93–117.
Gr¨adel et al., 1997 – Gr¨adel 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, pp. 53–69.
Grefe, 1998 – Grefe, C. “Fischer Servi’s intuitionistic modal logic has the finite model property”, in: M. Kracht, M. de Rijke, H. Wansing, M. Zakharyaschev (eds.), Advances in Modal Logic, Vol. 1, CSLI Publications, 1998, pp. 85–98.
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, pp. 361–372.
Halpern, Vardi, 1998 – Halpern, J.Y., Vardi, M.Y. “The complexity of reasoning about knowledge and time I: Lower bounds”, Journal of Computer and System Sciences,1989, Vol. 38, No. 1, pp. 195–237.
Harel, 1986 – Harel, D. “Effective transformations on infinite trees, with applications to high undecidability, dominoes, and fairness”, Journal of the ACM, 1986, Vol. 33, pp. 224–248.
Hodkinson et al., 2003 – Hodkinson, I., Kontchakov, R., Kurucz, A., Wolter, F., Zakharyaschev, M. “On the computational complexity of decidable fragments of first-order linear temporal logics”, in: 10th International Symposium on Temporal Representation and Reasoning 2003 and Fourth International Conference on Temporal Logic. Proceedings. IEEE, 2003, pp. 91–98.
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, pp. 85–134.
Hodkinson et al., 2001 – Hodkinson, I., Wolter, F., Zakharyaschev, M. “Monodic fragments of first-order temporal logics: 2000–2001 A.D.”, in: 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, pp. 1–23.
Hughes, Cresswell, 1996 – Hughes, G.E., Cresswell, M.J. A New Introduction to Modal Logic. Routledge, 1996.
Huth, Ryan, 2004 – Huth, M., Ryan, M. Logic in Computer Science: Modelling and Reasoning about Systems, second edition. Cambridge: Cambridge University Press, 2004.
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, pp. 428–438.
Kripke, 1962 – Kripke, S. “The undecidability of monadic modal quantification theory”, Zeitschrift f¨ur Matematische Logik und Grundlagen der Mathematik, 1962, Vol. 8, pp. 113–116.
Libkin, 2004 – Libkin, L. Elements of Finite Model Theory. Springer, 2004.
Maier, 2004 – Maier, P. “Intuitionistic LTL and a new characterization of safety and liveness”, in: J. Marcinkowski, A. Tarlecki (eds.), Proceedings of the Computer Science Logic 18th International Workshop (CSL’04), Vol. 3210 of Lecture Notes in Computer Science, Springer, 2004, pp. 295–309.
Manna, Pnueli, 1992 – Manna, Z., Pnueli, A. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, 1992.
Manna, Pnueli, 1995 – Manna, Z., Pnueli, A. Temporal Verification of Reactive Systems: Safety. Springer, 1995.
Marx, 1999 – Marx, M. “Complexity of products of modal logics”, Journal of Logic and Computation, 1999, Vol. 9, No. 2, pp. 197–214.
Maslov et al., 1965 – Maslov, S., Mints, G., Orevkov, V. “Unsolvability in the constructive predicate calculus of certain classes of formulas containing only monadic predicate variables”, Soviet Mathematics Doklady, 1965, Vol. 6, pp. 918–920. Merz, 1992 – Merz, S. “Decidability and incompleteness results for first-order temporal logics of linear time”, Journal of Applied Non-Classical Logics, 1992, Vol. 2, No. 2, pp. 139–156.
Mints, 1968 – Mints, G. “Some calculi of modal logic”, Trudy Matematicheskogo Instituta imeni V.A. Steklova, 1968, Vol. 98, No. 88–111. (In Russian) Mints, 2000 – Mints, G. A Short Introduction to Intuitionistic Logic. New York: Kluwer Academic Publishers, 2000.
Mortimer, 1975 – Mortimer, M. “On languages with two variables”, Zeitschrift f¨ur Mathematische Logik und Grundlagen der Mathematik, 1975, pp. 135–140.
Nishimura, 1960 – Nishimura, I. “On formulas of one variable in intuitionistic propositional calculus”, The Journal of Symbolic Logic, 1960, Vol. 25, No. 4, pp. 327–331.
Ono, 1977 – Ono, H. “On some intuitionistic modal logics”, Publications of the Research Institute for Mathematical Sciences, 1977, Vol. 13, No. 3, pp. 687–722.
Pnueli, 1986 – Pnueli, A. “Applications of temporal logic to the specification and verification of reactive systems: A survey of current trends”, in: J.W. de Bakker, W.P. de Roever, G. Rozenberg (eds.), Current Trends in Concurrency, Vol. 224 of Lecture Notes in Computer Science. Springer, 1986.
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”, in: G. Governatori, I.M. Hodkinson, Y. Venema (eds.), Advances in Modal Logic 6. Stanford: College Publications, 2006, pp. 393–411.
Rybakov, 2008 – Rybakov, M. “Complexity of intuitionistic propositional logic and its fragments”, Journal of Applied Non-Classical Logics, 2008, Vol. 18, No. 2–3, pp. 267–292.
Rybakov, Shkatov, 2018a – Rybakov, M., Shkatov, D. “Complexity and expressivity of propositional dynamic logics with finitely many variables”, Logic Journal of the IGPL, 2018, Vol. 26, No. 5, pp. 539–547.
Rybakov, Shkatov, 2018b – Rybakov, M., Shkatov, D. “Complexity and expressivity of branching- and alternating-time temporal logics with finitely many variables”, in: B. Fischer, T. Uustalu (eds.), Theoretical Aspects of Computing–ICTAC 2018, Vol. 11187 of Lecture Notes in Computer Science. Springer, 2018, pp. 396–414.
Rybakov, Shkatov, 2018c – Rybakov, M., Shkatov, D. “A recursively enumerable Kripke complete first-order logic not complete with respect to a first-order definable class of frames”, in: G. Metcalfe, G. Bezhanishvili, G. D’Agostino, T. Studer (eds.), Advances in Modal Logic, Vol. 12. Stanford: College Publications, 2018, pp. 531–540.
Rybakov, Shkatov, 2019a – Rybakov, M., Shkatov, D. “Complexity of finite-variable fragments of propositional modal logics of symmetric frames”, Logic Journal of the IGPL, 2019, Vol. 27, No. 1, pp. 60–68.
Rybakov, Shkatov, 2019b – Rybakov, M., Shkatov, D. “Trakhtenbrot theorem for in: Proceedings of SAIC-classical languages with three individual variables”, SIT2019. Article No. 19. ACM, 2019.
Rybakov, Shkatov, 2019c – 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, pp. 695–717.
Rybakov, Shkatov, 2020a – Rybakov, M., Shkatov, D. “Recursive enumerability and elementary frame definability in predicate modal logic”, Journal of Logic and Computation, 2020, Vol. 30, No. 2, pp. 549–560.
Rybakov, Shkatov, 2020b – Rybakov, M., Shkatov, D. “Algorithmic properties of first-order modal logics of the natural number line in restricted languages”, in: S. Negri, N. Olivetti, R. Verbrugge, G. Sandu (eds.), Advances in Modal Logic, Vol. 13. Stanford: College Publications, 2020, pp. 523–539.
Rybakov, Shkatov, 2020c – 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, pp. 1305–1329.
Rybakov, Shkatov, 2021a – Rybakov, M., Shkatov, D. “Complexity of finite-variable fragments of products with K”, Journal of Logic and Computation, 2021, Vol. 31, No. 2, pp. 426–443.
Rybakov, Shkatov, 2021b – 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, pp. 494–522.
Rybakov, Shkatov, 2021c – 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, pp. 1266–1288.
Rybakov, Shkatov, 2021d – Rybakov, M., Shkatov, D. “Algorithmic properties of QK4.3 and QS4.3”, Smirnov Readings on Logic 2021, 2021, pp. 50–54.
Rybakov, Shkatov, 2021e – Rybakov, M., Shkatov, D. “Undecidability of the logic of partial quasiary predicates”. To appear in Logic Journal of the IGPL, doi 10.1093/jigpal/jzab018.
Schewe, 2008 – Schewe, S. “ATL ∗ satisfiability is 2EXPTIME-complete”, in: Automata, Languages and Programming. ICALP 2008, Vol. 5126 of Lecture Notes in Computer Science. Springer-Verlag Berlin Heidelberg, 2008, pp. 373–385.
Shehtman, Shkatov, 2019 – Shehtman, V., Shkatov, D. “On one-variable fragments of modal predicate logics”, in: Proceedings of SYSMICS2019. Amsterdam: Institute for Logic, Language and Computation; University of Amsterdam, 2019, pp. 129–132.
Shehtman, Shkatov, 2020 – Shehtman, V., Shkatov, D. “Some prospects for semiproducts and products of modal logics”, in: Short papers. AiML2020. Helsinki: University of Helsinki, 2020, pp. 107–111.
Simpson, 1994 – Simpson, A. The Proof Theory and Semantics of Intuitionistic Modal Logic. PhD thesis. Edinburgh: University of Edinburgh, 1995.
Sistla, Clarke, 1985 – Sistla, A.P., Clarke, E.M. “The complexity of propositional linear temporal logics”, Journal of ACM, 1985, Vol. 32, No. 3, pp. 733–749.
Spaan, 1993 – Spaan, E. Complexity of Modal Logics. PhD thesis. Amsterdam: University of Amsterdam, 1993.
Szalas, 1986 – Szalas, A. “Concerning the semantic consequence relation in first-order temporal logic”, Theoretical Computer Science, 1086, Vol. 47, pp. 329–334.
Szalas, Holenderski, 1988 – Szalas, A., Holenderski, L. “Incompleteness of first-order temporal logic with until”, Theoretical Computer Science, 1988, Vol. 57, pp. 317–325.
Trakhtenbrot, 1953 – Trakhtenbrot, B.A. “On recursive separability”, Doklady AN SSSR, 1953, Vol. 88, pp. 953–956. (In Russian)
Turing, 1936 – Turing, A.M. “On computable numbers, with an application to the ‘Entscheidungsproblem’”, Proceedings of the London Mathematical Society, 2 series, 1936/1937, Vol. 42, pp. 230–265.
van der Hoek, Wooldridge, 2003 – van der Hoek, W., Wooldridge, M. “Cooperation, knowledge, and time: Alternating-time temporal epistemic logic and its applications”, Studia Logica, 2003, Vol. 75, No. 1, pp. 125–157.
Vardi, Stockmeyer, 1985 – Vardi, M.Y., Stockmeyer, L. “Improved upper and lower bounds for modal logics of programs”, in: Proceedings of the seventeenth annual ACM symposium on Theory of computing, 1985, pp. 240–251.
Wolter, Zakharyaschev, 1997 – Wolter, F., Zakharyaschev, M. “On the relation between intuitionistic and classical modal logics”, Algebra and Logic, 1997, Vol. 36, pp. 121–155.
Wolter, Zakharyaschev, 1999 – Wolter, F., Zakharyaschev, M. “Intuitionistic modal logics as fragments of classical bimodal logics”, in: E. Orlowska (ed.), Logic at Work. Springer; Berlin, 1999, pp. 168–186.
Wolter, Zakharyaschev, 2000 – Wolter, F., Zakharyaschev, M. “Temporalizing description logics”, in: D. Gabbay and M. de Rijke (eds.), Frontiers of Combining Systems II. London: Studies Press/Wiley, 2000, pp. 379–401.
Wolter, Zakharyaschev, 1997 – Wolter, F., Zakharyaschev, M. “On the relation between intuitionistic and classical modal logics”, Algebra and Logic, 1997, Vol. 36, pp. 121–155.
Wolter, Zakharyaschev, 1999 – Wolter, F., Zakharyaschev, M. “Intuitionistic modal logics as fragments of classical bimodal logics”, in: E. Orlowska (ed.), Logic at Work. Springer; Berlin, 1999, pp. 168–186.
Wolter, Zakharyaschev, 2000 – Wolter, F., Zakharyaschev, M. “Temporalizing description logics”, in: D. Gabbay and M. de Rijke (eds.), Frontiers of Combining Systems II. London: Studies Press/Wiley, 2000, pp. 379–401.
Abiteboul, 1996 – Abiteboul, S., Herr, L., Van den Bussche, J. “Temporal versus first-order logic to query temporal databases”, in: Proceedings of the 15th International Conference on Principles of Databases (PODS ’96), 1996.
Ajspur et al., 2013 – Ajspur, M., Goranko, V., Shkatov, D. “Tableau-based decision procedure for the multiagent epistemic logic with all coalitional operators for common and distributed knowledge”, Logic Journal of the IGPL, 2013, Vol. 21, No. 3, pp. 407–437.
Alechina, Shkatov, 2006 – Alechina, N., Shkatov, D. “A general method for proving decidability of intuitionistic modal logics”, Journal of Applied Logic, 2006, Vol. 4, No. 3, pp. 219–230.
Alur et al., 2002 – Alur, R., Henzinger, T.A., Kuperman, O. “Alternating-Time temporal logic”, Journal of ACM, 2002, Vol. 49, No. 5, pp. 672–713.
Andr´eka et al., 1979 – Andr´eka, H., N´emeti, I., Sain, I. “Completeness problems in verification of programs and program schemes”, in: Mathematical Foundations of Computer Science 1979. MFCS 1979, ed. by J. Beˇcv´aˇr, Vol. 74 of Lecture Notes in Computer Science. Springer, 1979.
Artale, Franconi, 2000 – Artale, A., Franconi, E. “A survey of temporal extensions of description logics”, Annals of Mathematics and Artificial Intelligence, 2000, Vol. 30, pp. 171–210.
Artale et al., 2004 – Artale, A., Kontchakov, R., Kovtunova, A., Ryzhikov, V., Wolter, F., Zakharyaschev, M. “First-order rewritability of ontologymediated queries in linear temporal logic”, 2020. Preprint available at https://arxiv.org/abs/2004.07221
Artemov, Dzhaparidze, 1990 – Artemov, S., Dzhaparidze, G. “Finite Kripke models and predicate logics of provability”, The Journal of Symbolic Logic, 1990, Vol. 55, No. 3, pp. 1090–1098.
Baader et al., 2015 – Baader, F., Borgwardt, S., Lippmann, M. “Temporal query entailment in the description logic SHQ”, Journal of Web Semantics, 2015, Vol. 33, pp. 71–93.
Baader et al., 2012 – Baader, F., Ghilardi, S., Lutz, C. “Ltl over description logic axioms”, ACM Transactions on Computational Logic, 2012, Vol. 13, No. 3, Article 21.
Balbiani et al., 2019 – Balbiani, P., Boudou, J., Di´eguez, M., Fern´andez-Duque, D. “Intuitionistic linear temporal logics”, 2019, ACM Transactions on Computational Logic, Vol. 21, Article 14.
B¨orger et al., 1997 – B¨orger, E., Gr¨adel, E., Gurevich, Y. The Classical Decision Problem. Springer, 1997.
Borgwardt et al., 2015 – Borgwardt, S., Lippmann, M., Thost, V. “Temporalizing rewritable query languages over knowledge bases”, Journal of Web Semantics, 2015, Vol. 33, pp. 50–70.
Boudou et al., 2017 – Boudou, J., Di´eguez, M., Fern´andez-Duque D. “A decidable intuitionistic temporal logic”, in: Proceedings of the 26th EACSL Annual Conference on Computer Science Logic (CSL’17), 2017, Vol. 82, pp. 14:1–14:17.
Boudou et al., 2019 – Boudou, J., Di´eguez, M., Fern´andez-Duque, D., Romero F. “Axiomatic systems and topological semantics for intuitionistic temporal logic”, in: F. Calimeri, N. Leone, M. Manna (eds.), Logics in Artificial Intelligence. JELIA 2019, Vol. 11468 of Lecture Notes in Computer Science. Springer, 2019, pp. 763–777.
Bourgaux et al., 2019 – Bourgaux, C., Koopmann, P., Turhan, A.-Y. “Ontologymediated query answering over temporal and inconsistent data”, Semantic Web Journal, 2019, Vol. 10, pp. 475–521.
Bra¨uner, Ghilardi, 2007 – Bra¨uner, T., Ghilardi, S. “First-order modal logic”, in:
P. Blackburn, J. Van Benthem, F. Wolter (eds.), Handbook of Modal Logic, Vol. 3 of Studies in Logic and Practical Reasoning. Elsevier, 2007, pp. 549–620.
Brewka et al., 2011 – Brewka, G., Eiter, T., Truszczy´nski, M. “Answer set programming at a glance”, Communications of the ACM, 2011, Vol. 54, No. 12, pp. 92–103.
Cerrito et al., 1999 – Cerrito, S., Mayer, M.C., Praud, S. “First order linear temporal logic over finite time structures”, in: H. Ganzinger, D. McAllester, A. Voronkov (eds.), Logic for Programming and Automated Reasoning. LPAR 1999, Vol. 1705 of Lecture Notes in Computer Science. Springer, 1999.
Chagrov, Rybakov, 2003 – Chagrov, A., Rybakov, M. “How many variables does one need to prove PSPACE-hardness of modal logics?” in: P. Balbiani, N.-Y. Suzuki, F. Wolter, M. Zakharyaschev (eds.), Advances in Modal Logic, Vol. 4. London: King’s College Publications, 2003, pp. 71–82.
Chomicki, 1994 – Chomicki, J. “Temporal query languages: A survey”, in: D.M. Gabbay and H.J. Ohlbach (eds.), Temporal Logic. ICTL 1994, Vol. 827 of Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence). Springer, 1994.
Chomicki, Niwinski, 1993 – Chomicki, J., Niwinski, D. “On the feasibility of checking temporal integrity constraints”, Journal of Computer and System Sciences, 1995, Vol. 51, No. 3, pp. 523–535.
Church, 1936 – Church, A. “A note on the ‘Entscheidungsproblem’”, The Journal of Symbolic Logic, 1936, Vol. 1, pp. 40–41.
Clarke et al., 2000 – Clarke, E.M., Grumberg, O., Peled, D.A. Model Checking. Cambridge: MIT Press, 2000.
Davies, Pfenning, 2001 – Davies, R., Pfenning, F. “A modal analysis of staged computation”, Journal of the ACM, 2001, Vol. 48, No. 3, pp. 555–604.
Davies, 2017 – Davies, R. “A temporal logic approach to binding-time analysis”, Journal of the ACM, 2017, Vol. 64, No. 1, pp. 1–45.
Davoren, 2009 – Davoren, J.M. “On intuitionistic modal and tense logics and their classical companion logics: Topological semantics and bisimulations”, Annals of Pure and Applied Logic, 2009, Vol. 161, No. 3, pp. 349–367.
de Paiva et al., 2004 – de Paiva, V., Gor´e, R., Mendler, M. “Modalities in constructive logics and type theories”, Journal of Logic and Computation, 2004, Vol. 14, pp. 439–446.
Demri et al., 2016 – Demri, S., Goranko, V., Lange, M. Temporal Logics in Computer Science: Finite-state systems, Vol. 58 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016.
Di´eguez et al., 2018 – Di´eguez, M., Fern´andez-Duque, D. “An intuitionistic axiomatization of ‘eventually’” in: G. Metcalfe, G. Bezhanishvili, G. D’Agostino and T. Studer (eds.), Advances in Modal Logic, Vol. 12, College Publications, 2018, pp. 199–218.
Emerson, 1990 – Emerson, E.A. “Temporal and modal logic”, in: J. van Leeuwen (ed.), Handbook of Theoretical Computer Science, 1990, Vol. B, pp. 995–1072.
Emerson, Halpern, 1985 – Emerson, E.A., Halpern, J. “Decision procedures and expressiveness in temporal logic of branching time”, Journal of Computer and System Sciences, 1985, Vol. 30, No. 1, pp. 1–24.
Enderton, 2011 – Enderton, H.B. Computatbility Theory: An Introduction to Recursion Theory. New York: Academic Press, 2011.
Fagin et al., 1995 – Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y. Reasoning About Knowledge. Cambridge: MIT Press, 1995.
Fern´andez-Duque, 2018 – Fern´andez-Duque, D. “The intuitionistic temporal logic of dynamical systems”, Logical Methods in Computer Science, 2018, Vol. 14, No. 3, pp. 1–35.
Fischer, Ladner, 1979 – Fischer, M., Ladner, R.E. “Propositional dynamic logic of regular programs”, Journal of Computer and System Sciences, 1979, Vol. 18, pp. 194–211.
Fischer Servi, 1977 – Fischer Servi, G. “On modal logic with an intuitionistic base”, Studia Logica, 1977, Vol. 36, No. 3, pp. 141–149.
Fischer Servi, 1980 – Fischer Servi, G. “Semantics for a class of intuitionistic modal calculi”, in: M.L. Dalla Chiara (ed.), Italian Studies in the Philosophy of Science, pp. 59–72. Reidel; Dordrecht, 1980.
Fischer Servi, 1984 – Fischer Servi, G. “Axiomatizations for some intuitionistic modal logics”, Rendiconti del Seminario Matematico della Universit`a di Padova, 1984, Vol. 42, pp. 179–194.
Fitting, Mendelsohn, 1998 – Fitting, M., Mendelsohn, R.L. First-Order Modal Logic, Vol. 277 of Synthese Library. Dordrecht: Kluwer Academic Publishers, 1998. Gabbay, 1981 – Gabbay, D. Semantical Investigations in Heyting’s Intuitionistic Logic. Netherlands: D. Reidel, 1981.
Gabbay et al., 1994 – Gabbay, D., Hodkinson, I., Reynolds, M. Temporal Logic: Mathematical Foundations and Computational Aspects, Volume 1, Vol. 28 of Oxford Logic Guides. New York: Oxford University Press, 1994.
Gabbay et al., 2003 – Gabbay, D., Kurucz, A., Wolter, F., Zakharyaschev, M. ManyDimensional Modal Logics: Theory and Applications, Vol. 148 of Studies in Logic and the Foundations of Mathematics. Elsevier, 2003.
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, pp. 800–823.
Gabbay et al., 2009 – Gabbay, D., Shehtman, V., Skvortsov, D. Quantification in Nonclassical Logic, Volume 1, Vol. 153 of Studies in Logic and the Foundations of Mathematics. Elsevier, 2009.
Garson, 2001 – Garson, J.W. Quantification in modal logic. in: D.M. Gabbay and F. Guenthner (eds.), Handbook of Philosophical Logic, Vol. 3, pp. 267–323. Springer; Dordrecht, 2001.
Goldblatt, 1992 – Goldblatt, R. Logics of Time and Computation, Vol. 7 of CSLI Lecture Notes. Second edition. Stanford: Center for the Study of Language and Information, 1992.
Goldblatt, 2011 – Goldblatt, R. Quantifiers, Propositions and Identity: Admissible Semantics for Quantified Modal and Substructural Logics. Lecture Notes in Logic. Cambridge: Cambridge University Press, 2011.
Goranko, Shkatov, 2008 – Goranko, V., Shkatov, D. “Tableau-based decision procedures for the multi-agent epistemic logic with operators of common and distributed knowledge”, in: Proceedings of the Sixth International Conference on Software Engineering and Formal Methods, IEEE Press, 2008, pp. 237–246.
Goranko, Shkatov, 2009a – Goranko, V., Shkatov, D. “Tableau-based decision procedure for full coalitional multiagent temporal-epistemic logic of linear time”, in: S. Artemov and A. Nerode (eds.), International Symposium on Logical Foundations of Computer Science, 2009, pp. 197–213.
Goranko, Shkatov, 2009b – Goranko, V., Shkatov, D. “Tableau-based procedure for deciding satisfiability in the full coalitional multiagent epistemic logic”, in: C. Sierra, C. Castelfranchi, K.S. Decker, J. Sichman (eds.), Proceedings of 8th International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 09), 2009, pp. 969–976.
Goranko, Shkatov, 2009c – Goranko, V., Shkatov, D. “Tableau-based decision procedure for the full coalitional multiagent temporal-epistemic logic of branching time”, in: Proceedings of Formal Approaches to Multi-Agent Systems 2009, 2009.
Goranko, Shkatov, 2009d – Goranko, V., Shkatov, D. “Tableau-based decision procedures for logics of strategic ability in multiagent systems”, ACM Transactions on Computational Logic, 2009, Vol. 11, No. 1, pp. 3–51.
Goranko, van Drimmelen, 2006 – Goranko, V., Shkatov, D. “Complete axiomatization and decidability of the alternating-time temporal logic”, Theoretical Computer Science, 2006, Vol. 353, No. 1–3, pp. 93–117.
Gr¨adel et al., 1997 – Gr¨adel 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, pp. 53–69.
Grefe, 1998 – Grefe, C. “Fischer Servi’s intuitionistic modal logic has the finite model property”, in: M. Kracht, M. de Rijke, H. Wansing, M. Zakharyaschev (eds.), Advances in Modal Logic, Vol. 1, CSLI Publications, 1998, pp. 85–98.
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, pp. 361–372.
Halpern, Vardi, 1998 – Halpern, J.Y., Vardi, M.Y. “The complexity of reasoning about knowledge and time I: Lower bounds”, Journal of Computer and System Sciences,1989, Vol. 38, No. 1, pp. 195–237.
Harel, 1986 – Harel, D. “Effective transformations on infinite trees, with applications to high undecidability, dominoes, and fairness”, Journal of the ACM, 1986, Vol. 33, pp. 224–248.
Hodkinson et al., 2003 – Hodkinson, I., Kontchakov, R., Kurucz, A., Wolter, F., Zakharyaschev, M. “On the computational complexity of decidable fragments of first-order linear temporal logics”, in: 10th International Symposium on Temporal Representation and Reasoning 2003 and Fourth International Conference on Temporal Logic. Proceedings. IEEE, 2003, pp. 91–98.
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, pp. 85–134.
Hodkinson et al., 2001 – Hodkinson, I., Wolter, F., Zakharyaschev, M. “Monodic fragments of first-order temporal logics: 2000–2001 A.D.”, in: 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, pp. 1–23.
Hughes, Cresswell, 1996 – Hughes, G.E., Cresswell, M.J. A New Introduction to Modal Logic. Routledge, 1996.
Huth, Ryan, 2004 – Huth, M., Ryan, M. Logic in Computer Science: Modelling and Reasoning about Systems, second edition. Cambridge: Cambridge University Press, 2004.
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, pp. 428–438.
Kripke, 1962 – Kripke, S. “The undecidability of monadic modal quantification theory”, Zeitschrift f¨ur Matematische Logik und Grundlagen der Mathematik, 1962, Vol. 8, pp. 113–116.
Libkin, 2004 – Libkin, L. Elements of Finite Model Theory. Springer, 2004.
Maier, 2004 – Maier, P. “Intuitionistic LTL and a new characterization of safety and liveness”, in: J. Marcinkowski, A. Tarlecki (eds.), Proceedings of the Computer Science Logic 18th International Workshop (CSL’04), Vol. 3210 of Lecture Notes in Computer Science, Springer, 2004, pp. 295–309.
Manna, Pnueli, 1992 – Manna, Z., Pnueli, A. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, 1992.
Manna, Pnueli, 1995 – Manna, Z., Pnueli, A. Temporal Verification of Reactive Systems: Safety. Springer, 1995.
Marx, 1999 – Marx, M. “Complexity of products of modal logics”, Journal of Logic and Computation, 1999, Vol. 9, No. 2, pp. 197–214.
Maslov et al., 1965 – Maslov, S., Mints, G., Orevkov, V. “Unsolvability in the constructive predicate calculus of certain classes of formulas containing only monadic predicate variables”, Soviet Mathematics Doklady, 1965, Vol. 6, pp. 918–920. Merz, 1992 – Merz, S. “Decidability and incompleteness results for first-order temporal logics of linear time”, Journal of Applied Non-Classical Logics, 1992, Vol. 2, No. 2, pp. 139–156.
Mints, 1968 – Mints, G. “Some calculi of modal logic”, Trudy Matematicheskogo Instituta imeni V.A. Steklova, 1968, Vol. 98, No. 88–111. (In Russian) Mints, 2000 – Mints, G. A Short Introduction to Intuitionistic Logic. New York: Kluwer Academic Publishers, 2000.
Mortimer, 1975 – Mortimer, M. “On languages with two variables”, Zeitschrift f¨ur Mathematische Logik und Grundlagen der Mathematik, 1975, pp. 135–140.
Nishimura, 1960 – Nishimura, I. “On formulas of one variable in intuitionistic propositional calculus”, The Journal of Symbolic Logic, 1960, Vol. 25, No. 4, pp. 327–331.
Ono, 1977 – Ono, H. “On some intuitionistic modal logics”, Publications of the Research Institute for Mathematical Sciences, 1977, Vol. 13, No. 3, pp. 687–722.
Pnueli, 1986 – Pnueli, A. “Applications of temporal logic to the specification and verification of reactive systems: A survey of current trends”, in: J.W. de Bakker, W.P. de Roever, G. Rozenberg (eds.), Current Trends in Concurrency, Vol. 224 of Lecture Notes in Computer Science. Springer, 1986.
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”, in: G. Governatori, I.M. Hodkinson, Y. Venema (eds.), Advances in Modal Logic 6. Stanford: College Publications, 2006, pp. 393–411.
Rybakov, 2008 – Rybakov, M. “Complexity of intuitionistic propositional logic and its fragments”, Journal of Applied Non-Classical Logics, 2008, Vol. 18, No. 2–3, pp. 267–292.
Rybakov, Shkatov, 2018a – Rybakov, M., Shkatov, D. “Complexity and expressivity of propositional dynamic logics with finitely many variables”, Logic Journal of the IGPL, 2018, Vol. 26, No. 5, pp. 539–547.
Rybakov, Shkatov, 2018b – Rybakov, M., Shkatov, D. “Complexity and expressivity of branching- and alternating-time temporal logics with finitely many variables”, in: B. Fischer, T. Uustalu (eds.), Theoretical Aspects of Computing–ICTAC 2018, Vol. 11187 of Lecture Notes in Computer Science. Springer, 2018, pp. 396–414.
Rybakov, Shkatov, 2018c – Rybakov, M., Shkatov, D. “A recursively enumerable Kripke complete first-order logic not complete with respect to a first-order definable class of frames”, in: G. Metcalfe, G. Bezhanishvili, G. D’Agostino, T. Studer (eds.), Advances in Modal Logic, Vol. 12. Stanford: College Publications, 2018, pp. 531–540.
Rybakov, Shkatov, 2019a – Rybakov, M., Shkatov, D. “Complexity of finite-variable fragments of propositional modal logics of symmetric frames”, Logic Journal of the IGPL, 2019, Vol. 27, No. 1, pp. 60–68.
Rybakov, Shkatov, 2019b – Rybakov, M., Shkatov, D. “Trakhtenbrot theorem for in: Proceedings of SAIC-classical languages with three individual variables”, SIT2019. Article No. 19. ACM, 2019.
Rybakov, Shkatov, 2019c – 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, pp. 695–717.
Rybakov, Shkatov, 2020a – Rybakov, M., Shkatov, D. “Recursive enumerability and elementary frame definability in predicate modal logic”, Journal of Logic and Computation, 2020, Vol. 30, No. 2, pp. 549–560.
Rybakov, Shkatov, 2020b – Rybakov, M., Shkatov, D. “Algorithmic properties of first-order modal logics of the natural number line in restricted languages”, in: S. Negri, N. Olivetti, R. Verbrugge, G. Sandu (eds.), Advances in Modal Logic, Vol. 13. Stanford: College Publications, 2020, pp. 523–539.
Rybakov, Shkatov, 2020c – 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, pp. 1305–1329.
Rybakov, Shkatov, 2021a – Rybakov, M., Shkatov, D. “Complexity of finite-variable fragments of products with K”, Journal of Logic and Computation, 2021, Vol. 31, No. 2, pp. 426–443.
Rybakov, Shkatov, 2021b – 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, pp. 494–522.
Rybakov, Shkatov, 2021c – 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, pp. 1266–1288.
Rybakov, Shkatov, 2021d – Rybakov, M., Shkatov, D. “Algorithmic properties of QK4.3 and QS4.3”, Smirnov Readings on Logic 2021, 2021, pp. 50–54.
Rybakov, Shkatov, 2021e – Rybakov, M., Shkatov, D. “Undecidability of the logic of partial quasiary predicates”. To appear in Logic Journal of the IGPL, doi 10.1093/jigpal/jzab018.
Schewe, 2008 – Schewe, S. “ATL ∗ satisfiability is 2EXPTIME-complete”, in: Automata, Languages and Programming. ICALP 2008, Vol. 5126 of Lecture Notes in Computer Science. Springer-Verlag Berlin Heidelberg, 2008, pp. 373–385.
Shehtman, Shkatov, 2019 – Shehtman, V., Shkatov, D. “On one-variable fragments of modal predicate logics”, in: Proceedings of SYSMICS2019. Amsterdam: Institute for Logic, Language and Computation; University of Amsterdam, 2019, pp. 129–132.
Shehtman, Shkatov, 2020 – Shehtman, V., Shkatov, D. “Some prospects for semiproducts and products of modal logics”, in: Short papers. AiML2020. Helsinki: University of Helsinki, 2020, pp. 107–111.
Simpson, 1994 – Simpson, A. The Proof Theory and Semantics of Intuitionistic Modal Logic. PhD thesis. Edinburgh: University of Edinburgh, 1995.
Sistla, Clarke, 1985 – Sistla, A.P., Clarke, E.M. “The complexity of propositional linear temporal logics”, Journal of ACM, 1985, Vol. 32, No. 3, pp. 733–749.
Spaan, 1993 – Spaan, E. Complexity of Modal Logics. PhD thesis. Amsterdam: University of Amsterdam, 1993.
Szalas, 1986 – Szalas, A. “Concerning the semantic consequence relation in first-order temporal logic”, Theoretical Computer Science, 1086, Vol. 47, pp. 329–334.
Szalas, Holenderski, 1988 – Szalas, A., Holenderski, L. “Incompleteness of first-order temporal logic with until”, Theoretical Computer Science, 1988, Vol. 57, pp. 317–325.
Trakhtenbrot, 1953 – Trakhtenbrot, B.A. “On recursive separability”, Doklady AN SSSR, 1953, Vol. 88, pp. 953–956. (In Russian)
Turing, 1936 – Turing, A.M. “On computable numbers, with an application to the ‘Entscheidungsproblem’”, Proceedings of the London Mathematical Society, 2 series, 1936/1937, Vol. 42, pp. 230–265.
van der Hoek, Wooldridge, 2003 – van der Hoek, W., Wooldridge, M. “Cooperation, knowledge, and time: Alternating-time temporal epistemic logic and its applications”, Studia Logica, 2003, Vol. 75, No. 1, pp. 125–157.
Vardi, Stockmeyer, 1985 – Vardi, M.Y., Stockmeyer, L. “Improved upper and lower bounds for modal logics of programs”, in: Proceedings of the seventeenth annual ACM symposium on Theory of computing, 1985, pp. 240–251.
Wolter, Zakharyaschev, 1997 – Wolter, F., Zakharyaschev, M. “On the relation between intuitionistic and classical modal logics”, Algebra and Logic, 1997, Vol. 36, pp. 121–155.
Wolter, Zakharyaschev, 1999 – Wolter, F., Zakharyaschev, M. “Intuitionistic modal logics as fragments of classical bimodal logics”, in: E. Orlowska (ed.), Logic at Work. Springer; Berlin, 1999, pp. 168–186.
Wolter, Zakharyaschev, 2000 – Wolter, F., Zakharyaschev, M. “Temporalizing description logics”, in: D. Gabbay and M. de Rijke (eds.), Frontiers of Combining Systems II. London: Studies Press/Wiley, 2000, pp. 379–401.
Wolter, Zakharyaschev, 1997 – Wolter, F., Zakharyaschev, M. “On the relation between intuitionistic and classical modal logics”, Algebra and Logic, 1997, Vol. 36, pp. 121–155.
Wolter, Zakharyaschev, 1999 – Wolter, F., Zakharyaschev, M. “Intuitionistic modal logics as fragments of classical bimodal logics”, in: E. Orlowska (ed.), Logic at Work. Springer; Berlin, 1999, pp. 168–186.
Wolter, Zakharyaschev, 2000 – Wolter, F., Zakharyaschev, M. “Temporalizing description logics”, in: D. Gabbay and M. de Rijke (eds.), Frontiers of Combining Systems II. London: Studies Press/Wiley, 2000, pp. 379–401.