4.1.3. Метод резолюций Робинсона
Каждый дизъюнкт в этом методе называют фразой. Две фазы могут быть резольвированы друг с другом, обращаясь в пустой дизъюнкт, если одна из них содержит положительный n-местный литерал, а вторая негативный n-местный литерал того же предиката.
Абстрактная переменная резольвирует с любой конкретной переменной, принимая значения этой конкретной переменной. В методе резолюций используется формула(3.4): при выводимости цели результат должен быть пустым дизъюнктом. Покажем сказанное на примере.
Пусть имеется система правил (дизъюнктов)
(4.1)
(4.2)
S(b) (4.3)
(4.4)
Необходимо определить, достижима ли цель P(a).
Возьмем отрицание цели
. (4.5)
Резольвируем (4.5) и (4.1) получаем
. (4.6)
Резольвируем (4.6) и (4.2) получаем
R(a,b). (4.7)
Резольвируем (4.7) и (4.4) получаем
#. (4.8)
Иногда строят дерево резолюций, показанное на рис. 4.3.
Метод резолюций Робинсона позволяет работать и с функциями. Он решает проблему выводимости цели из данной системы правил.
В общем случае процедура резольвирования носит комбинаторный (многовариантный), характер, поэтому появилось много разновидностей этого метода (рис. 4.2), которые называются стратегиями упорядочения и очищения.
4.1.4.. Стратегии упорядочения и очищения
Эти стратегии перечислены на рис. 4.2. Рассмотрим некоторые из них.
Метод предпочтения одночленов: метод рекомендует начинать с дизъюнктов с наименьшим числом литералов.
Метод исключения тавтологии и уникальных литералов. Если есть литерал и нет его отрицания, или наоборот, то резолюции ни в каком случае не произойдут и такие литералы могут не рассматриваться.
Если какой-либо дизъюнкт общезначим его можно не рассматривать. Обычно рассматриваются два резольвирующих дизъюнкта.
Персональный компьютер может рассмотреть несколько резольвирующих дизъюнктов и осуществить гиперрезолюцию.
Если в дереве резолюций последовательно записать дизъюнкты и резолюции осуществить в соответствии с этой записью дизъюнктов, то получается линейная резолюция.
Присоединенная процедура. Иногда на предварительном этапе анализа возможно оценивать значение истинности некоторых литералов, чтобы не включать их или их отрицания в базовое множество. Оценивание ведется для основных частных случаев. Например, если символ Е – равенство чисел, то достаточно оценить частные случаи, например, предикаты Е(7, 3). Если имеются такие предикаты или их отрицания и указан диапазон изменения аргументов, то для оценки следует составить таблицы возможных основных частных случаев, объем которых достаточно велик. С каждым предикатным сисмволом ассоциируются программы, получившие название присоединенных процедур. Литерал оценивается путем запуска соответствующей процедуры.
Возникает два варианта.
1. Если значение истинности есть истина, то все выражение, содержащее данный литерал, можно исключить.
2. Если значение истинности есть ложь, то можно исключить вхождение данного литерала в данный дизъюнкт и, например, выражение P(x)Q(a)E(7, 3) может быть заменено на P(x)Q(a).
Таким образом рассмотрен метод решения проблемы выводимости результата из системы правил.
4.2. Проблема извлечение результата
При определении выводимости с помощью метода резолюций Робинсона к системе правил добавляют отрицание целей. Чтобы получить результат, к системе правил добавляют дизъюнкт, состоящий из отрицания цели и цели. Покажем это на примере.
Пусть имеется система правил
1) Петр находится там же, где и Иван;
2) Иван находится в школе.
Цель: Определить где находится Петр;
Введем предикат B(X, Y) где X – имя, Y – место нахождения. Тогда система правил имеет вид
1) B(Иван, Y) B(Петр, Y),
2) B(Иван, школа).
Цель: B(Петр, Y).
Цель выводима, как это следует из рис. 4.4. Получим результат вывода (рис. 4.5).
Таким образом, найден математический аппарат для теоритического решения проблемы извлечения результата.
Вместе с тем такой математический аппарат не всегда удобен для прикладных целей. В связи с этим в прикладных целях для поиска решений используют другие методы: поиск в глубину и в ширину – в языке ПРОЛОГ, прямая и обратная аргументация – в оболочке экспертной системы GURU.