Шаг 1. принять отрицание заключения, т.е. ù В;
Шаг 2. привести все формулы посылок и отрицания заключения к конъюнктивной нормальной форме (см. с.35);
Шаг 3. выписать множество дизъюнктов всех посылок и отрицания заключения:
K = {D1; D2; . . . Dk };
Шаг 4. выполнить анализ пар множества K по правилу:
“если существуют дизъюнкты Di и Dj, один из которых (Di) содержит литеру А, а другой (Dj) — контрарную литеру ùА, то соединить эту пару логической связкой дизъюнкции (Di Ú Dj) и сформировать новый дизъюнкт — резольвенту, исключив контрарные литеры А и ùА;
Шаг5. если в результате соединения дизъюнктов, содержащих контрарные литеры, будет получена пустая резольвента — , то конец (доказательство подтвердило противоречие), в противном случае включить резольвенту в множество дизъюнктов K и перейти к шагу 4.
Пример: Работа автоматического устройства, имеющего три клапана А, В и С, удовлетворяет следующим условиям: если не срабатывают клапаны А или В или оба вместе, то срабатывает клапан С; если срабатывают клапаны А или В или оба вместе, то не срабатывает клапан С. Следовательно, если срабатывает клапан С, то не срабатывает клапан А [2].
((ùАÚùBÚùА &ùB)®С); ((AÚBÚА&B)®ùC)
(C®ùA).
1) F1=((ùАÚùBÚùА &ùB)®С)= (АÚC)&(BÚC) — посылка;
2) F2=((AÚBÚА&B)®ùC)= (ùАÚùC)&(ùBÚùC) -посылка;
3) F3=ù (C®ùA)=C&А –отрицание заключения;
4) множество дизъюнктов: K={(АÚC); (BÚC); (ùАÚùC); (ùBÚùC); C; А };
5) СÚ(ùАÚùC)=ùА – резольвента из 2) и 3);
6) K1={(АÚC); (BÚC); (ùАÚùC); (ùBÚùC); C; А; ùА };
7) ùАÚ(АÚC)=C – резольвента из 1) и 5);
8) K2={(АÚC); (BÚC); (ùАÚùC); (ùBÚùC); C; А; ùА };
9) СÚ(ùBÚùC)=ùB –резольвента из 2) и 5);
10) K3={(АÚC); (BÚC); (ùАÚùC); (ùBÚùC); C; А; ùА ; ùB };
11) ùBÚ(BÚC)=C – резольвента из 1) и 9);
12) CÚùA=(CÚùA) – резольвента из 5) и 11);
13) K4={(АÚC); (BÚC); (ùАÚùC); (ùBÚùC); C; А; ùА; ùB; (CÚùA)};
14) (CÚùA)Ú (ùАÚùC)=ùА – резольвента из 2) и 12);
15) K5={(АÚC); (BÚC); (ùАÚùC); (ùBÚùC); C; А; ùА; ùB; (CÚùA)};
16) ùАÚA= — пустая резольвента.
Так доказано, что если срабатывает клапан С, то не срабатывает клапан А.
Пример: Доказать истинность заключения
A; В; (С&A®ùB)
ùС.
1) A — посылка;
2) B — посылка;
3) C&A®ù B = (ùCÚùAÚùB) — посылка;
4) ù(ùC) = C — отрицание заключения;
5) множество дизъюнктов: K={A; B; (ùCÚùAÚùB); C};
6) AÚ(ùCÚùAÚùB)=(ùСÚùB) — резольвента из 1) и 3);
7) K1={A; B; (ùCÚùAÚùB); C; (ùСÚùB)};
8) BÚ(ùСÚùB)=ùC — резольвента из 2) и 6);
9) K2={A; B; (ùCÚùAÚùB); C; (ùСÚùB); ùC };
10) СÚùC = — пустая резольвента из 4) и 7).
Так доказана истинность заключения ù C по принципу резолюции.
Пример: Доказать истинность заключения
( A&B®С ); (C&D® ù M);(ù N® D&M )
A&B®N.
1) A&B®C=ù(A&B)ÚC=(ùAÚùBÚC) — посылка;
2) C&D®ùM=ù(C&D)ÚùM=(ùCÚùDÚùM) — посылка;
3)ùN®D&M=ù(ùN)ÚD&M=( N Ú D )&( N Ú M ) — посылка;
4) ù((A&B)®N)=A&B&ùN — отрицание заключения;
5) множество дизъюнкций:
K={(ùAÚùBÚC); (ùCÚùDÚùM); (NÚD); (NÚM); A; B;ùN};6) (MÚN)ÚùN=М — резольвента из 3) и 4);
7) K1={(ùAÚùBÚC); (ùCÚùDÚùM); (NÚD); (NÚM); A; B; M; ùN};
8) (DÚN)ÚùN=D — резольвента из 3) и 4);
9) K2={(ùAÚùBÚC); (ùCÚùDÚùM); (NÚD); (NÚM);A; B; M;ùN; D};
10) (ùAÚùBÚC)ÚB=(ùAÚC) – резольвента из 1) и 4);
11) K3={(ùAÚùBÚC); (ùCÚùDÚùM); (NÚD); (NÚM);A; B; M; ùN; D; (ùAÚC)};
12) (ùAÚC)ÚA=C — резольвента из 4) и 10);
13) K4={(ùAÚùBÚC); (ùCÚùDÚùM); (NÚD); (NÚM);A; B; M; ùN; D; (ùAÚC); C};
14) (ùCÚùDÚùM)ÚC =(ùDÚùM) — резольвента из 2) и 12);
15) K5={(ùAÚùBÚC); (ùCÚùDÚùM); (NÚD); (NÚM);A; B; M; ùN; D; (ùAÚC); C; (ùDÚùM)};
16) DÚ(ùDÚùM)=ùM — резольвента из 8) и 15;
17) K6={(ùAÚùBÚC); (ùCÚùDÚùM); (NÚD); (NÚM);A; B; M; ùN; D; (ùAÚC); C; (ùDÚùM); ùM};
12) МÚù M = — пустая резольвента.
Так доказана истинность заключения (A&B®N).
Для иллюстрации вывода удобно использовать граф типа дерево, корнем которого является один из дизъюнктов отрицания заключения, а концевыми вершинами ветвей – оставшиеся дизъюнкты отрицания заключения и всех посылок. Узлами графа типа дерево являются резольвенты. Ниже даны примеры, сопровождаемые графом.
Пример: Доказать истинность заключения
(A®B)&(C®D); (D&B®M);ù M
(ùAÚùC)
1) (A®B)&(C®D)=(ùAÚB)&(ùCÚD) — посылка;
2) D&B®M=ù(D&B)ÚM=(ùDÚùBÚM) — посылка;
3) ù M — посылка;
4) ( ù AÚ ù C ) = A & C — отрицание заключения;
5) K ={A; C; ùM; (ùAÚB); (ùCÚD); (ùDÚùBÚM)}
6) AÚ(ùAÚB)=B — резольвента;
7) BÚ(ùDÚùBÚM)=(ùDÚM) — резольвента;
8) (ùDÚM)Ú(ùCÚD)=(ùCÚM) — резольвента;
9) (ùCÚM)ÚùM=ùC — резольвента;
10)ùCÚC=ÿ — пустая резольвента.
Так доказана истинность заключения (ùAÚùC).
|
||||
|
B
|
(ùDÚM)
|
(ùCÚM)
|
ùC
|
ÿ
Рис.6. Граф доказательства
Пример: Доказать истинность заключения
(( AÚB)®C); (С®(DÚB)); (С®N); ((ùD)&(ù N))
ù A.
1) ((AÚB)®C)=(ùAÚC)&(ùBÚC) — посылка;
2) (C®(DÚB))=(BÚùCÚD) — посылка;
3) (C®N) = (ùCÚN) — посылка;
4)ùD — посылка;
5) ùN — посылка;
6) ù(ùA)=A – отрицание заключения;
7) K={(ùAÚC); (ùBÚC); (BÚùCÚD); (ùCÚN);ùD;ùN; A};
8
|
|
) AÚ(ùAÚC)=C – резольвента из 1) и 6);
9) CÚ(BÚùCÚD)=(BÚD) – резольвента из 2) и 7);
10) (BÚD)Ú(ùBÚC)=(CÚD) – резольвента из 1) и 8);
11) (CÚD)ÚùD=C – резольвента из 4) и 9);
12) CÚ(ùCÚN)=N – резольвента из 3) и 10);
|
13) NÚùN=ÿ — пустая резольвента.
|
|
||||||||||||||||
|
||||||||||||||||
|
||||||||||||||||
|
||||||||||||||||
|
||||||||||||||||
|
ùN
ÿ
Рис. 7. Граф доказательства.
|
1) AÚ(ùAÚC)=C – резольвента из 1) и 6);
|
|
2) CÚ(ùCÚN)=N – резольвента из 3) и 14);
|
|
3) NÚùN=ÿ — пустая резольвента.
|
|||
Рис. 8 Граф доказательства
Так как резольвенты включаются в множество дизъюнктов S, то возможно неоднократное их использование в процессе вывода. Многократное использование дизъюнкт множества S оправдано законом идемпотентности, т.к. Di=Di&Di&…&Di.
Пример: Доказать истинность заключения
(AÚB); (A«B);
(A&B).
1) (AÚB) — посылка;
2) (A«B)=(ùAÚB)&(ùBÚA) — посылка;
3)ù(A&B)=(ùAÚùB) –отрицание заключения;
4) K = {(AÚB); (ùAÚB); (ùBÚA); (ùAÚùB)};
5) (ùAÚùB)Ú(ùAÚB)= ùA — резольвента;
6) ùAÚ(AÚB)=B — резольвента;
7) BÚ(ùBÚA)=A — резольвента;
8) AÚùA= ÿ — пустая резольвента.
|
Рис. 9 Граф доказательства ÿ
Достоинством принципа резолюции является то, что при доказательстве истинности заключения применяют только одно правило: поиск и удаление контрарных литер на множестве дизъюнктов до получения пустой резольвенты.