Nagrinėjamos modalumo logikos S4 formulės, kuriose yra tik loginės operacijos ¬, ∨, ∧ ir neiginys sutinkamas tik prieš atomines formules. Jei į tokias formules įeina vien tik modalumo operatoriai ☐ ir nėra jose ♢ (arba įeina vien tik ♢ ir nėra jose ☐), tai tokių formulių klasės išsprendžiamos. Be to, įrodyta, kad normaliosios priešdėlinės formos su vienviečiais predikatiniais kintamaisiais formulių klasė išsprendžiama jei formulių matricose nėra modalumo operatoriaus ☐ įeičių.