Допустимость и унификация в модальных логиках, близких к $S4.2$

Изучаются проблемы унифицируемости и допустимости правил вывода для бесконечного класса модальных логик. Логики предполагаются разрешимыми, полными по Крипке и порождаемыми классами фреймов с наибольшими кластерами (в частности, такие логики расширяют модальную логику $S4.2$). Для любой такой логики $L$ и для любой формулы $\alpha$, унифицируемой $L$, эффективно строится некоторый унификатор $\sigma$ для $\alpha$ в $L$, проверяющий допустимость в $L$ любого данного правила вывода $\alpha/\beta$ с переключаемой главной модальностью для заключения правила $\beta$ (т. е. $\sigma$ решает проблему допустимости для всех таких правил вывода).