МФСП, 12 лекция (от 26 ноября)

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

Докажем с применением индукции с помощью PVS, что марок номиналом 3 и 5 хватит, чтобы покрыть любую сумму, большую 7.

stamps : THEORY
BEGIN
    stamps : LEMMA
    (FORALL (i : nat) : (i > 7) IMPLIES
    EXIST (t : nat, f : nat) :
        i = 3 * t + 5 * f
    )
END stamps

Сразу применять (skolem!) нельзя, так как мы хотим провести доказательство с использованием индукции. Следовательно, сначала применяем (induct "i"), а потом уже в индуктивном переходе применим (skolem!).

По этому поводу будут 2 задачи:

1. Написать формулу, получающуюся при решении задачи по методу Флойда и показать, как она будет доказываться в PVS.
2. Тоже на доказательство в PVS, скорее всего с применением индукции, но не сильно сложное.

Следующая среда — консультация, через раз — коллоквиум.

Ссылки:

• http://sed.ispras.ru/fmprac