Пример доказательства выводимости правильного умозаключения

методом резолюции. Доказательство «от противного». Пусть следствие (умозаключение) ложно, т.е. , тогда . Список дизъюнктов – добавляется к списку дизъюнктов посылок.

1. Алгоритм проверки выводимости правильного построенного умозаключения Вонга (Wong, 1960, США)

(1960 г. Гарвард).

Выводимость P из S означает, что из множества посылок

⊦ множество следствий.

Это соответствует логической формуле или более детально

, где .

Правильно построенному рассуждению (умозаключению) должна соответствовать тавтология .

Каждая и суть ППФ, построенная из связок &, Ú, ù, ®.

⊦ называется строкой Вонга.

Правила обработки строки Вонга, приводящие к доказательству выводимости P ⊦ S таковы, что каждое правило суть логический закон и является тождественно истинным преобразованием.

Пусть дана строка Вонга

⊦

левая часть правая часть

строки строки

1) Замена импликации в строке на ДНФ:

В Р_i и S_j, там, где встречается знак «®».

…⊦ … строка с «®»

…⊦ … строка ДНФ

2) Избавление от знака отрицания «ù » переносом из одной части строки в другую.

а) ⊦ , добавление к правой части.

⊦ редуцированная строка Вонга.

б) Р ⊦ добавление к левой части

Р,А ⊦ редуцированная строка Вонга.

Перенос любой переменной в левую (правую) часть строки всегда вызывает её «отрицание».

Пример: Избавление от знака отрицания.

а) Строка Вонга [( , B) ⊦ (C)] редуцируется в строку

[(B) ⊦ (А, C)] ⊦ (С) – строка Вонга интерпретируется как логическая формула . Редуцированная строка Вонга [ ⊦ ] и соответствующая формула .

Правило редуцирования строки Вона является тождественно истинным преобразованием. Доказательство тождественности двух выражений.

Таким образом, если из выводима С, то из В выводима

б) ⊦ редуцируется в ⊦ С] и соответственно

3) Расщепление на строки (левой и правой части строки Вонга).

а) ⊦ S ; расщепление левой части

⊦ S; ⊦ S

б) ⊦ ; расщепление правой части

⊦ ; ⊦

Выводимость (тавтология, тождественная истинность каждой строки должна быть доказана).

Пример: а) ⊦ ; расщепление – ⊦ и ⊦ ; ;

4) Замена логических связок на «,» (правило перечисления).

Строка Вонга

⊦

редуцируется в строку

⊦