Computational complexity of the word problem in modal and pseudo-Boolean algebras

M. Rybakov

Izvestiâ vysših učebnyh zavedenij. Matematika, no. 5 (2022), pp. 42-60.

Résumé

We consider the computational complexity of the word problem for finitely generated Heyting and modal algebras. It is shown that the word problem is PSPACE-complete if only constant modal terms or only $0$-generated modal algebras are considered; similar results are obtained for two-variable terms and $2$-generated Heyting algebras. It is also shown that, if an equation of positive terms is refuted in a Heyting algebra, it is refuted in a $2$-generated algebra. We also consider the word problem for certain classes of modal and Heyting algebras and obtain results similar to those mentioned above for infinite families of such classes. The obtained results are optimal in the number of generators: reduction in generators leads to the polynomial time decidable word problem.

Détail

Keywords: word problem, finitely generated algebra.
Mots-clés : modal algebra, Heyting algebra, pseudo-Boolean algebra

Bibliographie

[1] Thue A., “Problem über Veränderungen von Zeichenreihen nach gegebehen Regeln”, Vid. Skr. Math.-natur. KI., 10 (1914)

[2] Markov A. A., “Nevozmozhnost nekotorykh algorifmov v teorii assotsiativnykh sistem”, Dokl. AN SSSR, 55:7 (1947), 587–590

[3] Post EL., “Recursive unsolvability of a problem of Thue”, J. Symbolic Logic, 12:1 (1947), 1–11 | DOI | MR | Zbl

[4] Adyan S. I., Durnev V. G., “Algoritmicheskie problemy dlya grupp i polugrupp”, UMN, 55:2(332) (2000), 3–94 | MR | Zbl

[5] Ladner R. E., “The computational complexity of provability in systems of modal propositional logic”, SIAM J. on Comput., 6:3 (1977), 467–480 | DOI | MR | Zbl

[6] Statman R., “Intuitionistic propositional logic is polynomial-space complete”, Theoretical Comput. Sci., 9 (1979), 67–72 | DOI | MR | Zbl

[7] Levin L. A., “Universalnye zadachi perebora”, Probl. peredachi informatsii, 9:3 (1973), 115–116 | MR | Zbl

[8] Cook S. A., “The Complexity of Theorem-Proving Procedures”, Proceedings of the Third Annual ACM Symposium on the Theory of Computation, 1971, 151–158 | DOI | MR | Zbl

[9] Rybakov M. N., “Slozhnost problemy razresheniya bazisnoi i formalnoi logik”, Logicheskie issledov., 10, Nauka, M., 2003, 158–166 | Zbl

[10] Rybakov M. N., “Slozhnost konstantnogo fragmenta propozitsionalnoi dinamicheskoi logiki”, Vestn. Tversk. gos. un-ta. Ser. Prikl. matem., 2007, no. 5, 5–17

[11] Chagrov A., Rybakov M., How many variables does one need to prove PSPACE-hardness of modal logics?, Adv. in Modal Logic, 4 (2003), 71–82 | MR | Zbl

[12] Demri S., Schnoebelen P., “The complexity of propositional linear temporal logics in simple cases”, Information and Comput., 174 (2002), 84–103 | DOI | MR | Zbl

[13] Halpern J. Y., “The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic”, Aftificial Intelligence, 75:2 (1995), 361–372 | DOI | MR | Zbl

[14] Rybakov M., “Complexity of finite-variable fragments of EXPTIME-complete logics”, J. Appl. Non-Classical Logics, 17:3 (2007), 359–382 | DOI | MR | Zbl

[15] Rybakov M., “Complexity of intuitionistic propositional logic and its fragments”, J. Appl. Non-Classical Logics, 18:2–3 (2008), 267–292 | DOI | MR | Zbl

[16] Rybakov M., Shkatov D., “Complexity and expressivity of branching- and alternating-time temporal logics with finitely many variables”, Theoretical Aspects of Computing, ICTAC 2018, Lect. Notes in Comput. Sci., 11187, eds. Fischer B., Uustalu T., Springer, 2018, 396–414 | DOI | MR | Zbl

[17] Rybakov M., Shkatov D., “Complexity and expressivity of propositional dynamic logics with finitely many variables”, Logic J. of the IGPL, 26:5 (2018), 539–547 | DOI | MR

[18] Rybakov M., Shkatov D., “Complexity of finite-variable fragments of propositional modal logics of symmetric frames”, Logic J. of the IGPL, 27:1 (2019), 60–68 | MR

[19] Rybakov M., Shkatov D., “Complexity of finite-variable fragments of products with K”, J. Logic and Comput., 31:2 (2021), 426–443 | DOI | MR | Zbl

[20] Rybakov M., “Complexity of intuitionistic and Visser's basic and formal logic in finitely many variables”, Adv. in Modal Logic, 6, King's College Publications, London, 2006, 393–411 | MR

[21] Spaan E., Complexity of Modal Logics, PhD thesis, Univ. van Amsterdam, 1993 | MR

[22] Švejdar V., “The decision problem of provability logic with only one atom”, Archive for Math. Logic, 42:8 (2003), 763–768 | DOI | MR

[23] Chagrov A., Zakharyaschev M., Modal Logic, Oxford Univ. Press, 1997 | MR | Zbl

[24] Papadimitriou C. H., Computational Complexity, Addison–Wesley Publishing Company, 1995 | MR

[25] Savitch W. J., “Relationships between nondeterministic and deterministic tape complexity”, J. Comput. and Syst. Sci., 4 (1970), 177–192 | DOI | MR | Zbl

[26] Nishimura I., “On formulas of one variable in intuitionistic propositional calculus”, J. Symbolic Logic, 25:4 (1960), 327–331 | DOI | MR | Zbl

[27] Yankov V. A., “Ob ischislenii slabogo zakona isklyuchennogo tretego”, Izv. AN SSSR. Ser. matem., 2:5 (1968), 1044–1051

[28] Mardaev S. I., “Vlozheniya implikativnykh reshetok v superintuitsionistskie logiki”, Algebra i logika, 26:3 (1987), 318–357 | MR

[29] Rybakov M., Shkatov D., “Undecidability of first-order modal and intuitionistic logics with two variables and one monadic predicate letter”, Studia Logica, 107:4 (2019), 695–717 | DOI | MR | Zbl

[30] Rybakov M., Shkatov D., “Algorithmic properties of first-order modal logics of finite Kripke frames in restricted languages”, J. Logic and Comput., 30:7 (2020), 1305–1329 | DOI | MR | Zbl

[31] Rybakov M., Shkatov D., “Algorithmic properties of first-order superintuitionistic logics of finite Kripke frames in restricted languages”, J. Logic and Comput., 31:2 (2021), 494–522 | DOI | MR | Zbl