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 darbas apsaugotas Creative Commons priskyrimo 4.0 viešąja licencija.