Если матрица формулы в результате приведения к виду ПНФ не будет содержать свободных переменных и сколемовских функций, то для вывода заключения полностью пpuменим алгоритм принципа резолюции, рассмотренный в исчислении высказываний. Этот алгоритм основывается на том, что если две формулы состоящие из дизъюнкции атомов (в дальнейшем такие формулы будем называть дизъюнктами ) связаны конъюнкцией, и в них имеются два одинаковых или приводимых к одинаковым (унифицируемых ) атома с разными знаками, то из них можно получить третий дизъюнкт , который будет логическим следствием первых двух, и в нем будут исключены эти два атома. Однако, если в результате приведения к виду ССФ аргументы атомов содержат сколемовские функции, то для поиска контрарных атомов необходимо выполнить подстановки термов вместо предметных переменных и получить новые формулы дизъюнктов, которые допускают их унификацию при формировании контрарных пар. Множество подстановок нужно формировать последовательно, просматривая каждый раз только одну предметную переменную.
Например, если даны два дизъюнкта (P1(x)ÚùP2(x)) и (ùP1(f(x))ÚP3(y)), то для получения контрарной пары атомов возможна подстановка
xòf(х)(P1(x)ÚùP2(x))=(P1(f(x))ÚùP2(f(x))) и
xòf(х)(ùP1(f(x))ÚP3(y))= (ùP1(f(x))ÚP3(y)).
В результате склеивания этих дизъюнктов может быть получена резольвента: (P1(f(x))ÚùP2(f(x)))Ú(ùP1(f(x))ÚP3(y))= (ùP2(f(x))Ú P3(y)).
Если пара дизъюнктов имеет вид (P1(f1(x))ÚùP2(x)) и (ùP1(f2(x))ÚP3(y)), то никакая подстановка не позволит сформировать резольвенту.
Пример: Даны две формулы P3(a;x;f(q(y))) и ùP3(z;f(z);f(u)).
Выполнить унификацию контрарных атомов.
1) zòa ùP3(z;f(z);f(u))=ùP3(a;f(a);f(u));
2) xòf(a) P3(a;x;f(q(y)))=P3(a;f(a);f(q(y)));
3) uòq(y) ùP3(a;f(a);f(u))=ùP3(a;f(a);f(q(y))).
В результате получены два контрарных атома: P3(a;f(a);f(q(y))) и ùP3(a;f(a);f(q(y))). Если в эти формулы атомов вместо предметной переменной y сделать подстановку предметной постояннойb, т.е.
yòbP3(a;f(a);f(q(y)))=P3(a;f(a);f(q(b))) и
yòbùP3(a;f(a);f(q(y)))= P3(a;f(a);f(q(b))),
то получим два контрарных высказывания.
Пример. Даны две формулы P3(x;a;f(q(a))) и ùP3(z;y;f(u)).
Выполнить унификацию контрарных формул.
1) xòbP3(x;a;f(q(a)))=P3(b;a;f(q(a)));
2) yòaù P3(z;y;f(u))=ùP3(z;a;f(u));
3) yòaùP3(z;a;f(u))=ùP3(b;a;f(u));
4) uòq(a)ùP3(b;a;f(u))=ùP3(b;a;f(q(a))).
В результате получены две контрарных формулы: P3(b;a;f(q(a))) и ùP3(b;a;f(q(a))).
Принцип резолюции может быть усилен линейным выводом, упорядочением атомов в дизъюнкте и использованием информации о резольвируемых атомах.
Линейным выводом из множества дизъюнктов K называется последовательность дизъюнктов D1, D2,…Dn, где каждый член DiÎK, а каждый Di+1 является резольвентой центрального дизъюнкта (или предшествующей резольвенты) и бокового дизъюнкта из множества K.
Упорядоченным дизъюнктом называется дизъюнкт с заданной последовательностью атомов. Атом Pj старше атома Pi в упорядоченном дизъюнкте тогда и только тогда, когда j > i. Например, в упорядоченном дизъюнкте (P1ÚP2ÚP3ÚP4) младшим считается атом P1, а старшим — P4. При наличии в упорядоченном дизюънкте двух одинаковых атомов, по закону идемпотенции, следует удалить старший атом, сохранив на прежнем месте младший.
Другим усилением принципа резолюции является использование информации о резольвируемых атомах. Обычно при выполнении процедуры унификации происходит удаление резольвируемых атомов. Однако они несут полезную информацию. Поэтому вместо удаления резольвируемых атомов при унификации предлагается удалять только старший атом, а младший — сохранить в резольвенте, выделив какой-либо рамкой. Если за обрамленным атомом в резольвенте не следует никакой другой атом, то обрамленный атом удалить. Если за обрамленным атомом резольвенты следует какой-либо необрамленный атом, то его следует оставить для последующего исследования. И наконец, если последний необрамленный атом резольвенты унифицируется с отрицанием атома боковой ветви, то его следует обрамить и удалить вместе с литерой боковой ветви. Используя резольвенты на последующих этапах, можно получить обрамленными все атомы последней резольвенты, т.е.получить пустой дизъюнкт.
Пример: Суждение “Преподаватели принимали зачеты у всех студентов, не являющихся отличниками. Некоторые аспиранты и студенты сдавали зачеты только аспирантам. Ни один из аспирантов не был отличником. Следавательно, некоторые преподаватели были аспирантами.” [1] Пусть P1(x):=”x – отличник”, P2(x):=”x – аспирант”, P3(x):=”x –студент”, P24 (x; y):=”x сдает зачет y”, P5(x):=”x – преподаватель”. Формулы этого суждение имеют вид:
«x(P3(x)&ùP1 (x)®$y(P5(y)&P24 (x; y))); $x(P2(x)&P3(x)&»y(P24 (x; y)®P2 (y)));
«x(P2(x)®ùP1(x)) .
$x(P5(x)&P2(x)).
· Преобразовать посылки и отрицание заключения в ССФ:
1) F1=»x(P3(x)&ùP1 (x)®$y(P5(y)&P24 (x; y)))=
«x$y(P3(x)&ùP1 (x)®(P5(y)&P24 (x; y)))=
«x(P3(x)&ùP1 (x)®(P5(f(x))&P24 (x; f(x)))).
M1=(P3(x)&ùP1 (x)®P5(f(x))&P24 (x; f(x)))=
ù(P3(x)&ùP1 (x))Ú P5(f(x))&P24 (x; f(x)) =
(ùP3(x)ÚP1 (x)Ú P5 (f(x))&P24 (x; f(x))=
(ùP3(x)ÚP1 (x)Ú P5(f(x)))&(ùP3(x)ÚP1 (x)Ú P24 (x; f(x))).
2) F2=$x(P2(x)&P3(x)&»y(P24 (x; y)®P2 (y)))=
$x»y(P2(x)&P3(x)&(P24 (x; y)®P2 (y)))=
«y(P2(a)&P3(a)&(P24 (a; y)®P2 (y))).
M2=(P2(a)&P3(a)&(P24 (a; y)®P2 (y)))=
P2(a)&P3(a)&(ùP24 (a; y)ÚP2 (y))).
3) F3=»x(P2(x)®ùP1(x)).
M3=(P2(x)®ùP1(x))= (ùP2(x)ÚùP1(x)).
4) F4=ù$x(P5(x)&P2(x))= «x(ù (P5(x)&P2(x))).
M4=(ù (P5(x)&P2(x)))= (ùP5(x)Úù P2(x))).
· Выписать множество дизъюнктов:
K= {(ùP3(x)ÚP1 (x)ÚP5(f(x))); (ùP3(x)ÚP1 (x)Ú P24 (x; f(x))); P2(a); P3(a);
(ùP24 (a; y)ÚP2(y)); (ùP1(x)ÚùP2(x)); (ùP5(x)ÚùP2(x))};
· Выполнить унификацию и формирование резольвент
|
1) xòa (ùP1(x)ÚùP2(x)) Ú P2(a)= ùP1(a)Ú = ùP1(a);
|
2)ùP1(a)Úxòa(ùP3(x)ÚP1 (x)ÚP24 (x; f(x)))= ÚùP3(a)Ú P24 (a; f(a));
|
3) ÚùP3(a) Ú P24 (a; f(a))Ú yòf(a) (ùP24 (a; y)ÚP2(y))=
|
|
ÚùP3(a)Ú Ú P2(f(a));
|
|
4) ÚùP3(a)Ú Ú P2(f(a)) Úxòf(a)(ùP5(x)ÚùP2(x))=
|
|
|
ÚùP3(a)Ú Ú ÚùP5(f(a));
|
|
|
5) ÚùP3(a)Ú Ú ÚùP5(f(a)) Ú
|
|
|
|
xòa(ùP3(x)ÚP1 (x)ÚP5(f(x)))= ÚùP3(a)Ú Ú Ú Ú P1 (a);
|
|
|
|
6) ÚùP3(a)Ú Ú Ú Ú P1 (a)ÚùP1(a)=
|
|
|
|
|
ÚùP3(a)Ú Ú Ú Ú =
|
ÚùP3(a);
|
|
|
7) ÚùP3(a) Ú P3(a)= Ú = .
На рис. 14 дан граф линейной унификации этого примера.
ùP1(x)ÚùP2(x)
ùP1(a) P2(a)
|
ÚùP3(a)Ú P24 (a; f(a)) ùP3(x)ÚP1 (x)ÚP24 (x; f(x))
|
|
ÚùP3(a)Ú Ú P2(f(a)) ùP24 (a; y)ÚP2(y)
|
|
|
ÚùP3(a) Ú Ú Ú ùP5(x)ÚùP2(x)
|
|
|
ÚùP5(f(a))
ÚùP3(a)Ú Ú Ú ùP3(x)ÚP1 (x)ÚP5(f(x))
|
|
Ú ÚP1 (x)
ÚùP3(a) ùP1(a)
P3(a)
Рис. 14. Граф линейной унификации
Пример: Существуют студенты, которые любят всех преподавателей. Ни один из студентов не любит невежд. Следовательно, ни один из преподавателей не является невеждой. [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));
· Преобразовать посылки и отрицание заключения в ССФ:
1) F1=$x(P1(x)&»y(P2 (y)®P23(x; y)))= $x»y(P1(x)& (P2 (y)®P23(x; y)))= «y(P1(a)& (P2 (y)®P23(a; y)))= «y(P1(a)& (ùP2 (y)ÚP23(a; y)));
M1= P1(a)&(ùP2 (y)ÚP23(a; y));
2) F2=»x(P1(x) ®»y(P4 (y)®ùP23(x; y)))=
«x»y (P1(x) ® (P4 (y)®ùP23(x; y)))= «x»y (ùP1(x)ÚùP4 (y)ÚùP23(x; y)));
M2=(ùP1(x)ÚùP4 (y)ÚùP23(x; y));
3) F3=ù»y(P2 (y)®ùP4(y))= $y(ù(ùP2(y)ÚùP4(y))= $y(P2(y) &P4(y))=
P2(b)&P4(b);
M3=P2(b)&P4(b).
· Выписать множество дизъюнктов:
K={P1(a); (ùP2 (y)ÚP23(a; y)); (ùP1(x)ÚùP4 (y)ÚùP23(x; y)); P2(b); P4(b)};
· Выполнить унификацию и формирование резольвент:
|
1) P2(b) Ú xòb(ùP2 (y)ÚP23(a; y))= ÚP23(a; b);
|
2) ÚP23(a; b)Úyòb (ùP1(x)ÚùP4 (y)ÚùP23(x; y))=
|
ÚP23(a; b)Ú(ùP1(x)ÚùP4 (b)ÚùP23(x; b));
|
3) ÚP23(a; b)Úxòa(ùP1(x)ÚùP4 (b)ÚùP23(x; b))=
Ú
|
|
ÚùP1(a)ÚùP4 (b);
|
|
4) Ú ÚùP1(a)ÚùP4 (b) ÚP1(a)=
|
|
|
Ú Ú ÚùP4 (b);
|
|
|
5) Ú Ú ÚùP4 (b) ÚP4(b)=
|
|
|
|
Ú Ú Ú = .
На рис. 15 приведен граф линейной унификации для этого примера.
P2(b)
|
|
ÚP23(a; b) ùP2 (y)ÚP23(a; y)
ÚP23(a; b)Ú (ùP1(x)ÚùP4 (b)Ú ùP1(x)ÚùP4 (y)ÚùP23(x; y)
|
|
ÚùP23(x; b))
|
Ú ÚùP1(a) ÚùP4 (b) ùP1(x)ÚùP4 (b)ÚùP23(x; b))
|
|
Ú Ú ÚùP4 (b) P1(a)
P4(b)
Рис. 15. Граф линейной унификации