Негативные модальные схемы

Исследуется определимость на моделях Крипке решений модальных пропозициональных негативных схем. Показывается, что существует формула, определяющая решение такой схемы в любой транзитивной модели Крипке с обрывом возрастающих цепей, в которой решение существует. Предлагается алгоритм построения такой формулы.