О теории доказательств модальной логики с оператором наименьшей неподвижной точки

Модальная мю-логика (мю-исчисление) является одной из самых красивых систем модальной логики, применяемых в информатике для верификации моделей программ. Язык данной системы расширяет язык модальной логики оператором взятия наименьшей неподвижной точки. Долгое время при изучении данной системы основными методами являлись методы теории автоматов и теории игр, в то время как подход с точки зрения теории доказательств стал развиваться относительно недавно. В докладе планируется дать обзор текущего состояния исследований в области теории доказательств модальной мю-логики, в том числе рассказать о применении циклических выводов для доказательства интерполяционного свойства Линдона данной системы.