  We establish a natural translation from word rewriting systems to strictly
positive polymodal logics. Thereby, the latter can be considered as a
generalization of the former. As a corollary we obtain examples of undecidable
strictly positive normal modal logics. The translation has its counterpart on
the level of proofs: we formulate a natural deep inference proof system for
strictly positive logics generalizing derivations in word rewriting systems. We
also formulate some open questions related to the theory of modal companions of
superintuitionistic logics that was initiated by L.L. Maximova and V.V.
Rybakov.
