6. Применение метода доказательства теоремы дедукции для преобразования данного вывода в результирующий вывод.
Алгоритм преобразования данного вывода в результирующий.
Пример 3. Проиллюстрировать метод доказательства теоремы дедукции, преобразовав вывод в вывод
Данный вывод
1. Посылка
2.B 2. Посылка
3. 3. Посылка
|
Результирующий вывод
1. 1. Посылка
2.
2.
3. 3.
4.B 4. Посылка
5. 5.
6. 6.
7.
7.
8. 8.AC1
9.
9.
10. 10.
11. 11.
12.
|
4. 4.
5. 5.
|
12.
13.
13.
14. 14.
15.
15.AC2
16. 16.
17. 17.
| Установление доказуемости формул.
Как показывают примеры 6 и 7, применение метода преобразования вывода Г,А├B в вывод Г├АB, описанного в доказательстве МТ3, приводит к «разбуханию» результирующего вывода: если данный вывод содержит k формул, то результирующий вывод – 3k +2 формул. Существуют более «экономные методы». Например, неважно иметь содержащее 161 формулу доказательство формулы ,которое получается трехкратным применением описанного алгоритма к выводу , В, А├ С (см. пример 6), важно только знать, что эта формула доказуема.
Do'stlaringiz bilan baham: |
