Darbe naudojamasi žinoma G. Mints kvantorinės modalumo logikos S4 formulių transformacija. Įrodomas vienos klasės su vienviečiais predikatiniais kintamaisiais išsprendžiamumas. Formulėse esantys disjunktai turi ne daugiau kaip tris narius.
Šis kūrinys yra platinamas pagal Kūrybinių bendrijų Priskyrimas 4.0 tarptautinę licenciją.