4.1.2.4. Принцип резолюции

Существует эффективный алгоритм логического вывода - принцип резолюции. Он основан на том, что выводимость формулы В из множества посылок и аксиом F₁; F₂; F₃; . . . F_n равносильна доказательству теоремы

(F₁F₂F₃. . .F_nB);

((F₁F₂F₃. . .F_n)B);

(F₁F₂F₃. . .F_n B).

Из последней формулы следует, что заключение В истинно тогда и только тогда, когда формула (F₁F₂F₃...F_n(B))=л. Так как все формулы связаны логической связкой конъюнкции, то это справедливо при значении “л” хотя бы одной из подформул F_i илиB.

Для анализа формулы (F₁F₂F₃. . .F_nB) все подформулы F_i иB должны быть приведены к КНФ.

Два дизъюнкта КНФ, содержащие пропозициональные переменные с противоположными знаками формируют третий дизъюнкт - резольвенту, из которой будут исключены контрарные переменные. Многократно применяя эту процедуру к множеству дизъюнктов формулы (F₁F₂F₃...F_nB), стремятся получить пустой дизъюнкт. Наличие пустого дизъюнкта свидетельствует о выполнении условия (F₁F₂F₃...F_nB)=л. Следовательно, В является выводимой из множества заданных посылок и аксиом.

Алгоритм вывода по принципу резолюции:

Шаг 1: принять отрицание заключения, т.е.  В;

Шаг 2: привести все формулы посылок и отрицания заключения к конъюнктивной нормальной форме;

Шаг 3: выписать множество дизъюнктов всех посылок и отрицания заключения: K = {D₁; D₂; . . . D_k };

Шаг 4: выполнить анализ пар множества K по правилу:

“если существуют дизъюнкты D_i и D_j, один из которых (D_i) содержит пропозициональную переменную А, а другой (D_j) - контрарную ей переменную А, то соединить эту пару логи­ческой связкой дизъюнкции (D_i  D_j) и сформировать новый дизъюнкт - резольвенту, исключив контрарные литеры А и А; резольвенту включить в множество К,;

Шаг 5: если в результате соединения дизъюнктов, содержащих контрарные предикаты, будет получена пустая резольвента (пустой дизъюнкт) - , то конец (доказательство подтвердило противоречие), иначе включить резольвенту в множество дизъюнктов K и перейти к шагу 4; по закону идемпотентности любой дизъюнкт и любую резольвенту КНФ можно использовать неоднократно.

Пример: доказать истинность заключения

( ABС ); (CD  M); ( N DM )

ABN.

• ABC=(AB)C=(ABC) – посылка (один дизъюнкт);

• CDM=(CD)M=(CDM) –посылка (один дизъюнкт);

• NDM=(N)DM=( N  D )( N  M ) – посылка (два дизъюнкта);

• ((AB)N)=ABN - отрицание заключения (три однолитерных дизъюнкта);

• множество дизъюнктов:

K={(ABC); (CDM); (ND); (NM); A; B;N};

• (MN)N=М - резольвента;

• множество дизъюнктов:

K₁={(ABC); (CDM); (ND); (NM); A; B; M; N};

• (CDM)M =(CD) - резольвента;

• множество дизъюнктов:

K₂={(ABC); (CDM); (ND); (NM);A; B; M;N; (CD)};

• (ABC)(CD) =(ABD) – резольвента;

• множество дизъюнктов:

K₃={(ABC); (CDM); (ND); (NM); A; B; M; N; (CD); (ABD)};

• (ABD)A=(BD) - резольвента;

• множество дизъюнктов:

K₄={(ABC); (CDM); (ND); (NM); A; B; M; N; D; (CD); (ABD)}; (BD) };

• (BD)B=D - резольвента;

• множество дизъюнктов:

K₅={(ABC); (CDM); (ND); (NM); A; B; M; N; D; (CD); (ABD)}; (BD); D};

• D(ND)=N - резольвента;

• множество дизъюнктов:

K₆={(ABC); (CDM); (ND); (NM);A; B; M; N; D; (CD); (ABD)}; (BD); D}; N};

• N N = - пустая резольвента.

Для демонстрации удобно исполь­зовать граф типа дерево, корнем которого является один из дизъюнктов отрицания заключения, а вершинами – дизъюнкты всех посылок и отрицания заключения. Узлами графа типа дерево являются резольвенты.

Так доказана истинность заключения (ABN).

Пример: доказать истинность заключения

(AB)(CD); (DBM); M

(AC).

• (AB)(CD)=(AB)(CD) - посылка;

• DBM=(DB)M=(DBM) - посылка;

• M - посылка;

• (  A  C ) = A C - отрицание заключения;

• множество дизъюнктов:

K ={A; C; M; (AB); (CD); (DBM)};

• A(AB)=B - резольвента;

• множество дизъюнктов:

K ={A; C; M; (AB); (CD); (DBM); B};

• B(DBM)=(DM) - резольвента;

• множество дизъюнктов:

K ={A; C; M; (AB); (CD); (DBM); B; (DM)};

• (DM)(CD)=(CM) - резольвента;

• множество дизъюнктов:

K ={A; C; M; (AB); (CD); (DBM); B; (DM); (CM)};

• ( CM)M=C - резольвента;

• CC= - пустая резольвента.

Так доказана истинность заключения (AC).

П ример: доказать истинность заключения

((АBА B)С); ((ABАB)C)

(CA).

• ((АBА B)С)= (АC)(BC) - посылка;

• (ABАB)C)= (АC)(BC) -посылка;

• (CA)=CА – отрицание заключения;

• множество дизъюнктов:

K={(АC); (BC); (АC); (BC); C; А };

• С(АC)=А – резольвента;

• множество дизъюнктов:

K₁={(АC); (BC); (АC); (BC); C; А; А };

• А(АC)=C – резольвента;

• множество дизъюнктов:

K₂={(АC); (BC); (АC); (BC); C; А; А };

• С(BC)=B –резольвента;

• множество дизъюнктов:

K₃={(АC); (BC); (АC); (BC); C; А; А ; B };

• B(BC)=C – резольвента;

• множество дизъюнктов:

K₄={(АC); (BC); (АC); (BC); C; А; А;B};

• CA=(CA) – резольвента;

• множество дизъюнктов:

K₅={(АC); (BC); (АC); (BC); C; А; А; B; (CA)};

• (CA) (АC)=А – резольвента;

• множество дизъюнктов:

K₅={(АC); (BC); (АC); (BC); C; А; А; B; (CA)};

• (CA) (АC)=А – резольвента;

• АA= - пустая резольвента.

Так доказана истинность заключения (CA).

Так как резольвенты включаются в множество дизъюнктов K, то возможно их неоднократное использование в процессе вывода. Многократное использование дизъюнктов оправдано законом идемпотентности, т.к. D_i=D_iD_i...D_i.

Достоинством принципа резолюции является то, что при доказательстве истинности заключения применяют только одно правило: поиск и удаление контрарных пропозициональных переменных на множестве дизъюнктов до получения пустой резольвенты.