Курсы
Лекторы
Школьникам
О проекте
Войти
Главная
/
Курсы
/
Формальная семантика и верификация программного обеспечения
/
Семинар 5. Переписывание термов. Симплификатор Isabelle
Постановка задачи симплификации. Завершаемость процесса. Пример завершаемой системы
x 1.00
Математика
Формальная семантика и верификация программного обеспечения
Семинар 5. Переписывание термов. Симплификатор Isabelle
Миронов
Андрей Михайлович
Зиборов
Кирилл Викторович
Предыдущая лекция
Следующая лекция
00:15
Постановка задачи симплификации. Завершаемость процесса. Пример завершаемой системы
03:57
Симплификатор в Isabelle. Метод simp. Атрибуты симплификатора
08:50
Работа симплификатора в Isabelle на примерах работы со списком. Доказательство лемм. Пример незавершаемости. Приписывание assumption
21:30
Более сложный пример доказательства
24:56
Другие методы автоматизации (примеры доказательств)
29:50
Обобщение работы симплификатора. Правило переписывания. Использование предположений. Примеры (код)
34:14
Разбиение на случаи
39:27
Правила конгруэнции
41:00
Упорядоченное переписывание
45:19
Отладка симплификаторов
Курсы
Лекторы
Школьникам
О проекте
Контакты
Свяжитесь с нами
Отправить
2025 МГУ имени М.В. Ломоносова
Условия использования сайта
Сведения об образовательной организации
Нашли ошибку?
