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 kūrinys yra platinamas pagal Kūrybinių bendrijų Priskyrimas 4.0 tarptautinę licenciją.