Nagrinėjamos kvantorinės modalumo logikos formulės pavidalo
∀*□i∀*∃*(A1 ⋁⋯ ⋁ As ∨ □ B1 ⋁ ⋯ ⋁ □ Bu v ◊C1 ⋁ ⋯ ⋁ ◊ Cv).
Čia Ai , Bi, Ci yra klasikinės logikos literos. Tokio pavidalo formulėms aprašytas rezoliucijų metodas modalumo logikoje S4. Be to, aprašytas išvedamų disjunktų pavidalas.
Šis darbas apsaugotas Creative Commons priskyrimo 4.0 viešąja licencija.