Изучение возможностей проверки моделей для некоторых темпоральных логик в средстве доказательства теорем Coqкурсовая работа (Магистр)