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

Язык структурированных доказательств Isar (продолжение) 00:00:15 ?thesis. Представление теоремы на языке Isar (повторение) 00:03:12 Ключевое слово let. Цитирование facts по имени и по значению. Разбитие доказательства на мелкие шаги. Синтаксис для локальных лемм (повторение) 00:08:27 Пример 00:13:34 Теорема про квадрат разности (пример) 00:21:07 Утверждение о существовании двух списков таких, что любой список можно представить в виде их конкатенации, причем их длины совпадают или различаются на 1 (пример) 00:40:49 Метод cases 00:46:33 Структурная индукция 01:04:46 Вычислительная индукция (пример) Курс: Формальная семантика и верификация программного обеспечения Ссылка на плейлист: #мгу #мехмат #миронов #формальнаясемантикапо #верификацияпо