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

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 ◊1,◊2,...,◊m. For the polymodal logic S5m (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. [ABSTRACT FROM AUTHOR]