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

Логика первого порядка. Методы автоматизации доказательств. 00:00:15 Кванторы. Правила для кванторов 00:04:56 Инстанцирование правил. Атрибуты of и where 00:28:38 Доказательство прямым выводом (forward proof) 00:35:29 Атрибуты OF и THEN 00:40:38 Методы автоматического доказательства. Настройка с помощью атрибутов 00:51:36 Упражнение Курс: Формальная семантика и верификация программного обеспечения Ссылка на плейлист: #мгу #мехмат #миронов #формальнаясемантикапо #верификацияпо