О формализации модальной логики в системе Coqдипломная работа (Магистр)