МФСП, 13 лекция (от 03 декабря)

Материал из eSyr's wiki.

---

Версия 17:09, 6 декабря 2008

Пример первой задачи

В данной задаче в первом методе Флойда получилось 6 базовых путей и соответствующих предикатов. На коллоквиуме нужно будет каждый из них сформулировать на языке теории PVS (синтаксические ошибки не будут строго караться) и описать последовательность команд, которые приведут к доказательству его истинности. Дерево строить не надо.

Пример (для первого предиката):

1. (skolem!)
2. (skolem!)
3. (flatten)
4. (assert)