Об одной старой просто формулируемой нерешенной проблеме в модальной логике

Я расскажу об одной старой проблеме в модальной логике, которая до сих пор не поддается усилиям ученых. Формулируется она так: разрешима ли логика, задаваемая формулой $\Box \Box p -> \Box \Box \Box p$. В общем случае это n боксов p влечет m боксов p. Также я расскажу некоторые продвижения в решении этой задачи, которые были сделаны докладчиком в совместной работе с И.Шапировским. Мы доказали, разрешимость этих логик с некоторыми дополнительными естественными аксиомами. Задачу можно переформулировать в терминах направленных графов. И, судя по всему, в решении этой задачи могут помочь какие-то методы разработанные в теории графов. Поэтому я надеюсь, что слушателям будет интересно узнать о связи логики с теорией графов и, возможно, появятся идеи, которые могут помочь в дальнейшей атаке на эту проблему.