Axiomatization and Polynomial Solvability of Strictly Positive Fragments of Certain Modal Logics

Resumo

The fragment of the language of modal logic that consists of all implications A → B, where A and B are built from variables, the constant ⊤ (truth), and the connectives ∧ and ◊₁,◊₂,...,◊_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.