x 1.00
Скачать видео

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

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