Навигация
Поиск доказательства в системе резолюций
44446
знаков
1
таблица
1
изображение
3.4 Поиск доказательства в системе резолюций
Резолюция представляет собой правило вывода, с помощью которого можно вывести новую ППФ (правильно построенную формулу) из старой. Однако в приведенном выше описании логической системы ничего не говорится о том, как выполнить доказательство. Обратим основное внимание на стратегические аспекты доказательства теорем.
Пусть р представляет утверждение "Сократ — это человек", 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.
В качестве примера положим, что множество Т, как и ранее, имеет вид {{¬p,q},{¬q,¬r},{p}}. Мы пытаемся показать, что Т|- ¬r. Для этого докажем, что фраза {r} является следствием существующего множества Т, для чего добавим к этому множеству отрицание фразы ¬r. Поиск противоречия происходит следующим образом:
[{¬q,¬r},{r}]/{¬q}
[{¬p,q},{¬q}]/{¬q}
[{¬p},{p}]/{}
Этот метод доказательства теорем получил название "опровержение резолюции", поскольку, во-первых, он использует правило вывода резолюций, а во-вторых, следует стратегии "от противного" (стратегии опровержения).
Теперь вернемся к примеру PROLOG-программы, представленному в листинге 1. На рис. 1 показано дерево доказательства утверждения above(a, с). Дерево строится сверху вниз, и каждая ветвь связывает две "родительские фразы", в которых содержатся дополняющие литералы, с фразой, которая образуется в результате применения правила резолюции. Ко всем целям, записанным справа от значка ":-", неявно применяется отрицание. В левой части дерева представлены формулы целей, а в правой — фразы, взятые из базы данных.
Корнем дерева является пустая фраза {}. Это означает, что поиск доказательства был успешным. Добавление негативной фразы :- above (а, с) к исходному множеству (теории) привело к противоречию. Таким образом, можно утверждать, что фраза above (а, с) является логическим следствием из этой теории.
Обратите внимание на роль операции унификации в этом доказательстве. Цель above (а, с) унифицируется с головной фразой above(X, Y) с помощью подстановки {Х/а, Y/c}, где выражение Х/а можно интерпретировать как "X получает значение а". Затем эта подстановка применяется к хвостовой части фразы
on(Z, Y), above(X, Z),
из чего следует формулировка подцелей
on(Z, с), above(a, Z).
Следующая подцель on(Z, с) унифицируется с on(b, с) подстановкой {Z/b}. Эта подстановка затем применяется и к оставшейся подцели, которая таким образом превращается в above (а, b), и так до тех пор, пока не образуется пустая фраза.
Рис. 1. Дерево доказательства методом опровержения резолюций
Восходящий процесс доказательства, использующий в качестве отправной точки утверждение, которое мы стараемся доказать, позволяет сфокусировать внимание на процессе поиска решения, поскольку анализируемые логические связи по крайней мере потенциально ведут нас к цели. Правда, основанный на этой стратегии метод опровержения резолюций не позволяет решить все перечисленные выше проблемы. В частности, этот метод не гарантирует, что найденный путь доказательства будет короче других (или длиннее).
Похожие работы
... задач и выдвигать гипотезы , которые могут быть подтверждены или опровержены. Знания могут быть получены в процессе наблюдения за каким-либо объектогм. Режимы работы инженера по знаниям, консультолога в процессе приобретения знаний. протокольный анализ записываются рассуждения вслух в процессе решения задач. О.с. составляются протоколы, которые анализируются Интервью - ведется диалог с ...
... философии - особенно с методологических позиций материалистического понимания истории и материалистической диалектики с учетом социокультурной обусловленности этого процесса. Однако в западной философии и методологии науки XX в. фактически - особенно в годы «триумфального шествия» логического позитивизма (а у него действительно были немалые успехи) - научное знание исследовалось без учета его ...
... субъекта (Юм), априорным формам мышления (Кант), целевым установкам личности (прагматизм), интерсубъективным конвенциям (А. Пуанкаре) и др. Фундаментальными проблемами в данной сфере выступали в классической философии проблема критерия И., трактовка которого соответствовала принятому определению И. (от эйдотического образца у Платона до Божественной Мудрости у Фомы Аквинского, с одной стороны, и ...
описания знания подразделяются на: 1) Декларативные (факты) - это знания вида “А есть А”. 2) Процедурные - это знания вида “Если А, то В”. Декларативные знания подразделяются на объекты, классы объектов и отношения. Объект - это факт, который задается своим значением. Класс объектов - это имя, под которым объединяется конкретная совокупность объектов-фактов. Отношения - определяют связи ...
0 комментариев