Доказательство методом резолюции

 

 

Применяется всего одно правило вывода, что позволяет не запоминать многочисленных правил вывода и тавтологии. Это- правило резолюции, которое приведено в таблице 2.1 вместе с уже известными правилами.

 

 

Таблица 2.1

Резолюция	Цепное правило	Модус поненс
Из ХА	Из ~Х→А	А
И Y~А	И А→Y	А→Y
Получаем ХY	Получаем ~Х→Y	Y

 

 

Оно позволяет соединить две формулы, удалив из одной атом А а из другой ~А. Из приведенной выше таблицы видно, что правило резолюции можно рассматривать как аналог цепного правила в применении к формулам, находящимся в конъюнктивной нормальной форме В данном случае цепное правило записано в форме, эквивалентной приведенной ранее, но более удобной для сопоставления с правилом резолюции. Правило модус поненс можно считать частным случаем правила резолюции для случая ложного X.

Правило резолюции применяем следующим образом.

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

Приводим все посылки и отрицание заключения, принятого в качестве дополнительной посылки, к конъюнктивной нормальной форме.

а) Устраняем символы ↔и→ с помощью эквивалентностей

 

(А↔В) = (А→В) C)(В→А);

A→В = ~АВ

 

б) Продвигаем отрицания внутрь с помощью закона де Моргана.

в) Применяем дистрибутивность

 

А(BC)=(AB)(AC).

 

Этот метод приведения формул к виду, удобному для применения метода резолюции, обладает рядом серьезных недостатков, так как применение дистрибутивности, часто приводит к экспоненциальному разбуханию- испытуемой формулы и разрушает ее структуру. В пропозициональном случае лучше привести к конъюнктивной нормальной форме саму исходную формулу, что сразу решает вопрос о ее тавтологичности.

Зачастую гораздо целесообразнее упрощать формулу к виду, постепенно уменьшая ее глубину путем введения новых атомов, обозначающих ее части.

Теперь каждая посылка превратилась в конъюнкцию дизъюнктов, быть может, одночленную. Выписываем каждый дизъюнкт с новой строки; все дизъюнкты истинны, так как конъюнкция истинна по предположению.

Каждый дизъюнкт- это дизъюнкция (возможно, одночленная), состоящая из предложений и отрицаний предложений. Именно к ним применим метод резолюций. Берем любые два дизъюнкта, содержащие один и тот же атом, но с противоположными знаками, например

 

Х Y Z ~P, X P W.

 

Здесь Р - как раз тот атом, о котором шла речь. Применяем правило резолюции с атомом Р в роли А из этого правила, т.е. "отрезаем" Р от двух данных дизъюнктов:

 

(ХYZ)(YW)=XYZW.

 

Это правило легко применять, так как оно сводится к простому удалению членов дизъюнктов.

 

Из ХA,~AY выводим ХY.

Из A, ~AY выводим Y.

 

Продолжаем этот процесс, пока не получится Р и ~Р для некоторого атома Р. Применяя резолюцию и к ним, получим пустой дизъюнкт, выражающий противоречие, что завершает доказательство от противного.

Из Р, ~Р выводим ложь.

Пустой дизъюнкт обычно записывается в виде квадрата □.

В качестве примера рассмотрим доказательство соотношения:

 

PQ, P→R, Q→S├RS

 

1. Приводим посылки к нормальной форме и выписываем их на отдельных строках.

PQ, (2.12)

~ PR, (2.13)

~QS (2.14)

2. Записываем отрицание заключения и приводим его к нормальной форме.

 

~(RS)= ~R~S

~R (2.15)

~S (2.16)

 

3. Выводим пустой дизъюнкт с помощью резолюции.

 

~Р из (2.15) и (2.13) (2.17)

Q из (2.17) и (2.12) (2.18)

~Q из (2.16) и (2.14) (2.19)

□ из (2.18) и (2.19) (2.20)

По сравнению с классической логикой метод резолюции имеет ряд преимуществ.

- Не приходится применять эквивалентности для того, чтобы переставлять члены дизъюнкции РQ для получения QP и т.д. Это происходит отчасти потому, что все приводится к нормальной форме с самого начала, а отчасти потому, что для правила резолюции неважно положение отрезаемого атома в дизъюнкте.

- Нужно помнить всего одно правило.

Применение этого правила легко автоматизировать, т.е. запрограммировать для компьютера. Однако в случае длинного доказательства легко зациклиться, а однородные обозначения делают все дизъюнкты похожими друг на друга, так что трудно удерживать в памяти их смысл и выбирать нужный дизъюнкт.