Зиборов К.В. - Формальная семантика и верификация ПО - Семинар 5. Переписывание термов

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