Нужны некоторые намеки о резолюции Правило доказать - PullRequest
Новая
       31

Нужны некоторые намеки о резолюции Правило доказать

2 голосов
/ 01 ноября 2011

Это домашнее задание. Я пытаюсь доказать, что (a v b) ^ (~ b V c) | = (a V c)

это правильное правило разрешения. И мне не разрешают использовать правило разрешения, чтобы доказать это. Немного запутаться, не знаю, что мне делать в первую очередь ..

И еще одна проблема, учитель, давайте докажем KB | = a , когда KB ^ ~ a неудовлетворительно. насколько я знаю, мне может понадобиться создать КБ, которая включает в себя несколько предложений, тогда я могу доказать KB ^ ~ a неудовлетворительно. но учитель сказал мне, что если я хочу привести пример, я должен позволить, чтобы он подходил для каждого случая. Я хочу знать, есть ли универсальный пример, чтобы доказать это? Должен ли я использовать пример?

Надеюсь, кто-нибудь может дать мне несколько советов или полезных ссылок .. Спасибо ..

1 Ответ

2 голосов
/ 01 ноября 2011

Вы можете сделать это с помощью правила, описанного в третьем абзаце:

Сначала создайте базу знаний из всего, что вам известно: а именно a v b и ~b v c.

Затемдобавьте отрицание утверждения, которое вы пытаетесь доказать: ~(a v c).Вы можете переписать это в CNF и добавить в КБ.

Теперь покажите, что этот КБ является неудовлетворительным.Есть два способа сделать это:

  • Просто составьте таблицу истинности.Есть восемь возможных назначений для a, b, c, поэтому он будет иметь восемь строк;Вы можете показать, что хотя бы одно утверждение в КБ является ложным для любого возможного назначения.Это не «пример», потому что вы рассматриваете все возможные случаи.

  • В зависимости от моделей, которые вы используете, вы можете сделать некоторые выводы в самой КБ.У вас будут некоторые утверждения, которые просто утверждают, что определенная переменная является истинной или ложной;затем вы можете использовать этот факт для упрощения других операторов в КБ.Вы захотите проверить, что вы делаете это таким образом, который соответствует вашему формализму.

Итак, чтобы доказать, что KB ^ ~a неудовлетворительно подразумевает KB |= a, сделайте доказательство от противного:

  • У вас есть KB.
  • Предположим, что, учитывая KB, ~a - выполнимо.
  • Но если это правда, то KB ^ ~a - выполнимо, и вы доказываете, что это ложь, т. Е. KB ^ ~a неудовлетворительно.
  • Поэтомунаше предположение должно быть ошибочно, и поэтому ~a неудовлетворительно, учитывая KB.

Теперь вы в значительной степени там.

...