On axiomatization and polytime decidability of strictly positive fragments of some modal logics

We call a formula strictly positive, if it is built of propositional variables, conjunction and modal diamond operators. The strictly positive fragment (SP-fragment) of a logic L is the set of all provable in L implications A$\to$B, where A and B are strictly positive formulas. E. V. Dashkov proved that Gödel–Löb provability logic GL and the logic K4 have the same SP-fragments.
We study the SP-fragment of the logic K4.3 of all transitive linear frames. We give two different semantical characterizations of the fragmet. We will present a finite axiomatization of the SP-fragment of K4.3 and prove that it is polytime decidable.