|
ИСТИНА |
Войти в систему Регистрация |
ФНКЦ РР |
||
Проверка моделей для логики ветвящегося времени в исчислении индуктивных конструкцийдипломная работа (Бакалавр)
- Научный руководитель: Подымов Владислав Васильевич
- Автор: Тищенко Анастасия Сергеевна
- Тип: Бакалавр
- Организация, в которой проходила защита: МГУ имени М.В. Ломоносова
- Год защиты: 2024
- Аннотация: В работе предложена тактика (алгоритм) доказательства произвольной выполнимости формулы языка логики ветвящегося времени (CTL) на произвольной модели Крипке на языке LTac средства автоматизации доказательства теорем Coq, если формула действительно выполняется на модели: лаконично и ясно переизлагаются математические основы языка тактик LTac, предлагается тактика, доказывается полнота этой тактики.
- Добавил в систему: Подымов Владислав Васильевич