4.2.2.5. Принцип резолюции
Если матрица формулы в результате приведения к виду ПНФ не будет содержать свободных переменных и сколемовских функций, то для вывода заключения применим алгоритм принципа резолюции исчисления высказываний. Однако если в результате приведения к виду ССФ аргументы атомов содержат сколемовские функции, то для поиска контрарных атомов необходимо выполнить подстановки термов вместо предметных переменных и получить новые формулы дизъюнктов, которые допускают их унификацию при формировании контрарных пар. Множество подстановок нужно формировать последовательно, просматривая каждый раз только одну предметную переменную.
Принцип резолюции может быть усилен упорядочением атомов в дизъюнкте и использованием информации о резольвируемых атомах.
Упорядоченным дизъюнктом называется дизъюнкт с заданной последовательностью атомов. Атом Pj старше атома Pi в упорядоченном дизъюнкте тогда и только тогда, когда j>i. Например, в упорядоченном дизъюнкте (P1P2P3P4) самым младшим считается атом P1, а самым старшим - P4. При наличии в упорядоченном дизъюнкте двух одинаковых атомов, по закону идемпотенции, следует удалить старший атом, сохранив на прежнем месте младший.
Другим усилением принципа резолюции является использование информации о резольвируемых атомах. Обычно при выполнении процедуры унификации происходит удаление резольвируемых атомов. Однако они несут полезную информацию. Поэтому вместо удаления резольвируемых атомов при унификации удаляют только старший атом, а младший - сохраняют в резольвенте, выделив какой-либо рамкой.
Если за обрамленным атомом в дизъюнкте не следует никакой другой атом, то его удаляют. Если за обрамленным атомом в дизъюнкте следует какой-либо необрамленный атом, то его следует оставить для последующего анализа. И, наконец, если последний необрамленный атом резольвенты унифицируется с отрицанием атома боковой ветви, то его следует обрамить и удалить вместе с литерой боковой ветви. Используя резольвенты на последующих этапах, можно получить обрамленными все атомы последней резольвенты.
Пример: существуют студенты, которые любят всех преподавателей. Ни один из студентов не любит невежд. Следовательно, ни один преподаватель не является невеждой. [1]
Пусть P1(x):=” x – студент”, P2(y):=”y – преподаватель”, P23(x, y):=”x любит y”, P4(y):=”y - невежда”.
Формулы этого суждение имеют вид:
x(P1(x)y(P2 (y)P23(x; y)));
x(P1(x)
y(P4
(y)P23(x;
y)));
y(P2 (y)P4(y)).
Преобразовать посылки и отрицание заключения в ССФ:
F1=x(P1(x)y(P2 (y)P3(x; y)))= xy(P1(x) (P2 (y)P3(x; y)))= y(P1(a)(P2 (y)P3(a; y)))= y(P1(a)(P2 (y)P3(a; y)));
F2=x(P1(x)y(P4 (y)P3(x; y)))=xy(P1(x)(P4 (y)P3(x; y)))=
xy(P1(x)P4 (y)P3(x; y)));
F3=y(P2 (y)P4(y))=y((P2(y)P4(y)))=y(P2(y)P4(y))=P2(b)P4(b).
Выписать множество дизъюнктов:
K={P1(a); (P2 (y)P3(a; y)); (P1(x)P4 (y)P3(x; y)); P2(b); P4(b)}.
Выполнить унификацию и формирование резольвент:
P2(b)
P2(b)
P2(b)
= P3(a; b)(P1(x)P4 (b)P23(x; b));
P2(b)
P3(a; b)xa(P1(x)P4 (b)P23(x; b))=
P2(b)
P3(a;
b)
= P1(a)P4 (b);
P3(a;
b)
P2(b)
)
P1(a)P4 (b) P1(a)=
P3(a;
b)
P2(b)
P1(a)
P2(b)
)
P3(a;
b)
P1(a)
P4(b) P4(b)= .
Процесс вывода заключения по принципу резолюции представлен графом на рис. 4.10.
Пример: “Преподаватели принимали зачеты у всех студентов, не являющихся отличниками. Некоторые аспиранты и студенты сдавали зачеты только аспирантам. Ни один из аспирантов не был отличником. Следовательно, некоторые преподаватели были аспирантами.” [1]
Пусть P1(x):=”x – отличник”, P2(x):=”x – аспирант”, P3(x):=”x –студент”, P4(x; y):=”x сдает зачет y”, P5(x):=”x – преподаватель”.
Формулы этого суждения имеют вид:
x(P3(x)P1(x)y(P5(y)P4(x, y)));
x(P2(x)P3(x)y(P4(x, y)P2(y)));
x(P2(x)P1(x)) .
x(P5(x)P2(x)).
Преобразовать посылки и отрицание заключения в ССФ:
F1=x(P3(x)P1(x)y(P5(y)P4(x,y)))=x(P3(x)P1(x)P5(f(x)))
&(P3(x)P1(x)P4(x; f(x)));
F2=x(P2(x)P3(x)y(P4(x;y)P2(y)))=y(P2(a)P3(a)
(P4(a; y)P2(y)));
F3=x(P2(x)P1(x))=x(P2(x)P1(x));
F4=x(P5(x)P2(x))= x(P5(x)P2(x)).
Выписать множество дизъюнктов:
K= {(P3(x)P1(x)P5(f(x))); (P3(x)P1(x) P4(x, f(x))); P2(a); P3(a);
(P4 (a, y)P2(y)); (P1(x)P2(x)); (P5(x)P2(x))};
Эти операции показаны на графе 4.10.