Иллюстрированный самоучитель по введению в экспертные системы

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

Резолюция представляет собой правило вывода, с помощью которого можно вывести новую ППФ (правильно построенную формулу) из старой. Однако в приведенном выше описании логической системы ничего не говорилось о том, как выполнить доказательство. В этом разделе мы обратим основное внимание на стратегические аспекты доказательства теорем.

Пусть р представляет утверждение "Сократ – это человек", a q – утверждение "Сократ смертен". Пусть наша теория имеет вид: Т={{р,q}, {р}}.

Таким образом, утверждается, что если Сократ человек, то Сократ смертен, и что Сократ – человек. {17} выводится из теории Т за один шаг резолюции, эквивалентной правилу modus ponens..

Выражения {р, q} и {р} "сталкиваются" на паре дополняющих литералов р и р, а {q} является резольвентой. Таким образом, теория Алогически подразумевает д, что записывается в форме Т|-q. Теперь можно добавить новую фразу {q} – резольвенту – в теорию Т и получить таким образом теорию: Т'= {{ ip, q}, {p}, {q}}.

Конечно, в большинстве случаев для доказательства требуется множество шагов.

В этой теории р и q сохраняют прежний смысл, а г представляет утверждение "Сократ – бог". Для того чтобы показать, что Т|- r, потребуются два шага резолюции:

  • {q,p},{Р}/{q}
  • {q,-r},{q} / {-r}

Обратите внимание, что на первом шаге используются две фразы из исходного множества Т, а на втором– резольвента {q}, добавленная к Т. Кроме того, следует отметить, что доказательство может быть выполнено и по-другому, например:

  • {p,q},{q,r}/{p,r},
  • {p,r},{p}/{r}

При таком способе доказательства к Т добавляется другая резольвента. В связи со сказанным возникает ряд проблем.

  • Когда множество Т велико, естественно предположить, что должно существовать несколько способов вывести интересующую нас конкретную формулу (эта формула является целевой). Естественно, что предпочтение следует отдать тому методу, который позволяет быстрее сформулировать доказательство.
  • Множество Т может поддерживать и те правила, которые не имеют ничего общего с доказательством целевой формулы. Как же заранее узнать, какие правила приведут нас к цели?
  • Потенциально весь процесс подвержен опасности комбинаторного взрыва. На каждом шаге множество Г растет, и в нашем распоряжении оказывается все больше и больше возможных путей продолжения процесса, причем некоторые из них могут привести в зацикливанию.

Та схема логического вывода, которой мы следовали до сих пор, обычно называется прямой, или восходящей стратегией. Мы начинаем с того, что нам известно, и строим логические суждения в направлении к тому, что пытаемся доказать. Один из возможных способов преодоления сформулированных выше проблем – попытаться действовать в обратном направлении: от сформулированной целевой формулы к фактам, которые нужны нам для доказательства истинности этой формулы.

Предположим, перед нами стоит задача вывести {q} из некоторого множества фраз: Т= {…,{ p, q},…}.

Создается впечатление, что это множество нужно преобразовать, отыскивая фразы, включающие q в качестве литерала, а затем попытаться устранить другие литералы, если таковые найдутся. Но фраза {q} не "сталкивается" с такой фразой, как, например, { -р, q}, поскольку пара, состоящая из одинаковых литералов q, не является взаимно дополняющей.

Если q является целью, то метод опровержения резолюции реализуется добавлением негативной формулы цели к множеству Т, а затем нужно показать, что формула: Т' = Т U {q} является несовместной. Полагая, что множество Т непротиворечиво, приходим к выводу, что Т' может быть противоречивым вследствие Т | – q.

Рассмотрим этот вопрос более подробно. Сначала к существующему множеству фраз добавляется отрицание проверяемой фразы {-q}. Затем предпринимается попытка резольвировать {-q} с другой фразой в Т. При этом существуют только три возможные ситуации.

  • В Т не существует фразы, содержащей q. В этом случае доказать искомое невозможно.
  • Множество Т содержит {q}. В этом случае доказательство выполняется немедленно, поскольку из {q} и {q} можно вывести пустую фразу, что означает несовместность (наличие противоречия).
  • Множество Т содержит фразу {…, q,…}. Резольвирование этой фразы с {q} формирует новую фразу, которая содержит остальные литералы, причем для доказательства противоречия все они должны быть удалены в процессе резольвирования.

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

Если Вы заметили ошибку, выделите, пожалуйста, необходимый текст и нажмите CTRL + Enter, чтобы сообщить об этом редактору.