Курсы Лекторы Материалы О проекте
Курсы Лекторы Материалы О проекте
Войти
Семинар 5. Переписывание термов. Симплификатор Isabelle
Лекция из курса:
Формальная семантика и верификация программного обеспечения
Видео не может быть загружено из-за проблем с интернет-соединением или проблем на сервере. Или формат файла не поддерживается вашим браузером.
Семинар 5. Переписывание термов. Симплификатор Isabelle
Видео закончится через
NaN:NaN
00:00
00:00
00:15
Следующая секция начнется через 03:57
Постановка задачи симплификации. Завершаемость процесса. Пример завершаемой системы
03:57
Следующая секция начнется через 03:57
Симплификатор в Isabelle. Метод simp. Атрибуты симплификатора
08:50
Следующая секция начнется через 03:57
Работа симплификатора в Isabelle на примерах работы со списком. Доказательство лемм. Пример незавершаемости. Приписывание assumption
21:30
Следующая секция начнется через 03:57
Более сложный пример доказательства
24:56
Следующая секция начнется через 03:57
Другие методы автоматизации (примеры доказательств)
29:50
Следующая секция начнется через 03:57
Обобщение работы симплификатора. Правило переписывания. Использование предположений. Примеры (код)
34:14
Следующая секция начнется через 03:57
Разбиение на случаи
39:27
Следующая секция начнется через 03:57
Правила конгруэнции
41:00
Следующая секция начнется через 03:57
Упорядоченное переписывание
45:19
Следующая секция начнется через 03:57
Отладка симплификаторов
Свернуть таймкоды
00:00
00:00
Скорость
x 1.00
x 0.25
x 0.50
x 0.75
x 1.00
x 1.25
x 1.5
x 1.75
x 2.00
x 3.00
x 4.00
Качество
1080p
1080p
720p
480p
00:00
00:00
Скорость
x 1.00
x 0.25
x 0.50
x 0.75
x 1.00
x 1.25
x 1.5
x 1.75
x 2.00
x 3.00
x 4.00
Качество
1080p
1080p
720p
480p

Семинар 5. Переписывание термов. Симплификатор Isabelle

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