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

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

Таблица 2.1

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

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

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

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

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

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

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

A→В = ~А В

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

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

А (B C)=(A B) (A C).

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

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

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

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

Х Y Z ~P, X P W.

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

(Х Y Z) (Y W)=X Y Z W.

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

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

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

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

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

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

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

P Q, P→R, Q→S├R S

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

P Q, (2.12)

~ P R, (2.13)

~Q S (2.14)

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

~(R S)= ~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 для получения Q P и т.д. Это происходит отчасти потому, что все приводится к нормальной форме с самого начала, а отчасти потому, что для правила резолюции неважно положение отрезаемого атома в дизъюнкте.

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

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

Применение метода резолюций для ответов на вопросы

Предположим, что предикат F(х,у), означает х - отец у, и даны следующие факты об отцовстве:

F(john,. harry) F(john, sid) F(sid, liz)

Таким образом, есть три единичных (т.е. состоящих из одной литеры) дизъюнкта. Они не содержат переменных или импликаций, а просто представляют базисные факты того самого типа, который подходит для хранения в базе данных.

Введем еще три предиката М(х), S(х,у) и В(х, у), означающие соответственно, что х - мужчина, что он единокровен с у, что он брат у.

( х, у) F(х, у)→М(х)

( х, у, w) F(х,у) F(х, w)→S(у, w)

( х, у)S(х, у) М(х)→В(х, у)

Они утверждают следующее: 1) все отцы - мужчины; 2)если у детей один отец, то они единокровны; 3) брат - это единокровный мужчина.

Пусть задали вопрос ( z) В(z, harry)? Чтобы найти ответ с помощью метода резолюции, записываем отрицание вопроса ( z) ~В(z, harry). Затем приводим аксиомы к нормальной форме и записываем каждый дизъюнкт в отдельной строке (так как каждый дизъюнкт истинен сам по себе):

~Р(х, у) М(х) (2 21)

~Р(х, у) ~F(х, w) S(у, w) (2 22)

~S(х, у) ~M(х) B(х,у) (2.23)

F(john, harri) (2.24)

F(john, sid) (2 25)

F(john, liz) (2.26)

~B(z, harri) (2.27)

Не пишем внешних кванторов всеобщности, так как подразумевается, что каждая переменная связана таким квантором.

Константы отличаются от переменных тем, что они либо начинаются буквами из начала латинского алфавита, либо являются именами собственными, такими, как john, harri, sid и liz.

Для применения резолюции необходимо найти для данной пары дизъюнктов такую подстановку термов вместо переменных, чтобы после нее некоторая литера одного из дизъюнктов стала контрарна некоторой литере из другого дизъюнкта (т.е. отличалась от нее лишь отрицанием). Можно делать подстановки, так как все переменные связаны кванторами всеобщности. Если, например, подставим john вместо х и sid вместо у, то получим следующее:

~ F(john, sid) ~ F(john, w) S(sid, w).

Можно применить правило резолюции к этому дизъюнкту и (2.25), что дает новый дизъюнкт:

F(john, w) S(sid,w) (2.28)

из (2.5) и (2.2) {john/x, sid/у}

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

Продолжая, получим

S(sid, harri) (2.29)

из (2.24) и (2.27) {harri/у}

М(sid) (2.30)

из (2.26) и (2.21) {sid/х, liz/у}

~S(sid, y) B(sid, у) (2.31)

из (2.30) и (2.23) {sid/х}

В(sid, harry) (2.32)

из (2.29) и (2.31) {harry/у}

□

из (2.22) и (2.27) {sid/z} (2.33)

Таким образом, вывели единичный дизъюнкт (2.22),выражающий что sid - брат harry, использовав аксиомы и факты (2.24), (2.25), (2.26), имеющиеся в базе данных. Это противоречит отрицанию вопроса, которое утверждает, что harry не имеет братьев.

Если хотим знать, кто же брат Ьаггу, то должны следить за сделанными подстановками. Это можно сделать, введя новую литеру – так называемую литеру ответ с предикатом Answer(ответ).

Тогда вместо ~В(z, harri) напишем

~В(z, harri) Answer(z). (2.27a)

Теперь продолжим процесс резолюции не до получения пустого дизъюнкта, а до получения единичного дизъюнкта с предикатом Answer, которая запоминает подстановку для z, нужную для резолюции с дизъюнктом В(z, harri). Тогда (2.33) примет вид Answer(sid) из (2.22) и (2.27а) {sid/z}.

Полученный ответ означает, что sid – брат harry. При другой исходной информации получили бы вместо единичного дизьюнкта, скажем Answer(sid) Answer(fred).

Даже если провести резолюцию в несколько ином порядке, то получим тот же самый ответ. Допустим, что дошли до строки (2.21) так же, как и раньше, но затем применили (2.27а) вместо (2.27).

~S(х, harry) ~М(х) Ansver(х) (2.21)

из (2.27а) {х /z} и (2.23)

{harry/у} (2.21)

S(sid, harri) Answer(sid) (2.22)

из (2.30) и (2.31) {sid/х}

Answer(sid) (2.33)

из (2.32) и (2.29)

Однако если производить подстановки в иной последовательности, то попадаем в затруднительное положение:

~ F(john, w) S(sid,w) (2.28)

из (2.26) и (2.22) {john/x, harry/x)

S(hагrу, sid) (2.29)

из (2.25) и (2.28) {sid/w}

Проблема в том, что доказали S(hаггу, sid) вместо дизъюнкта S(sid, hаггу), который нужен нам для резолюции с (2.32). Эту трудность можно обойти, введя дополнительную аксиому:

( х, у) S(х, у) →S(у, х),

которая в нормальной форме имеет вид

~ S(х, у) S((у, х) (2.34)

К сожалению, далее нужно проявлять осторожность, чтобы не попасть в следующий бесконечный цикл:

S(sid, hагrу) (2.35)

из (2.29) и (2.34) {hагrу/х, sid/у}

S(hагrу, sid) (2.36)

из (2.35) и (2.34) {sid/х, harry/у}

S(sid, hагту) (2.37)

из (2.36) и т.д.

Это показывает, что необходимо тщательно планировать поиск доказательства, если хотим сохранить надежду искать его автоматически.