Секвенциальные рефлексивные логики с оператором разрешимости

Построены системы гильбертовского типа $L^\vartriangleright$ и секвенциальные исчисления $[L^\vartriangleright]$ для вариантов логик $L=\mathbf T,\mathbf{S4},\mathbf B,\mathbf {S5}$ и $\mathbf {Grz}$, сформулированных в языке с единственным модальным оператором разрешимости $\vartriangleright A=\square A\vee\square\neg A$. Доказано, что в исчислениях $[L^\vartriangleright]$ сечение не устранимо, однако можно ограничиться аналитическим сечением, сохраняющим свойство подформульности. Тем самым, исчисления $[\mathbf T^\vartriangleright]$, $[\mathbf {S4}^\vartriangleright]$, $[\mathbf {S5}^\vartriangleright]$ (соответственно $[\mathbf {Grz}^\vartriangleright]$) обладают (соответственно слабым) свойством подформульности (для $[\mathbf B_2^\vartriangleright]$ этот вопрос остается открытым). Установлено интерполяционное свойство Крейга для рассмотренных логик разрешимости.
Библиография: 17 названий.