Об устранении сечения для системы $K^+$

При изучении модальной мю-логики, логики общего знания и других логик, содержащих операторы взятия неподвижных точек, возникают исчисления, допускающие циклические и нефундированные выводы. К сожалению, структурная теория доказательств подобных исчислений остается не вполне развитой.
Мы обсудим один из методов устранения сечения в системах с нефундированнми выводами на примере исчисления секвенций для модальной логики транзитивного замыкания $K^+$.