Abstract:
The fragment of the language of modal logic that consists of all implications $A\to B$, where $A$ and $B$ are built from variables, the constant $\top$ (truth), and the connectives $\wedge$ and $\diamondsuit_1, \diamondsuit_2, \dots, \diamondsuit_m$. For the polymodal logic $S5_m$ (the logic of $m$ equivalence relations) and the logic $K4.3$ (the logic of irreflexive linear orders), an axiomatization of such fragments is found and their algorithmic decidability in polynomial time is proved.