1.4. принцип резолюцииСуществует эффективный алгоритм логического вывода - алгоритм резолюции. Этот алгоритм основан на том, что выводимость формулы В из множества посылок F1; F2; F3; . . . Fn равносильна доказательству теоремы |¾(F1&F2&F3&. . .&Fn®B), формулу которой можно преобразовать так: |¾(F1&F2&F3&. . .&Fn®B) = |¾(ù(F1&F2&F3&. . .&Fn)ÚB) = |¾ù(F1&F2&F3&. . .&Fn&( F2ù B)). Следовательно, заключение В истинно тогда и только тогда, когда формула (F1&F2&F3&...&Fn&(ùB))=л. Это возможно при значении “л” хотя бы одной из подформул Fi илиùB. Для анализа этой формулы все подформулы Fi иùB должны быть приведены в конъюнктивную нормальную форму и сформировано множество дизъюнктов, на которые распадаются все подформулы. Два дизъюнкта этого множества, содержащие пропозициональные переменные с противоположными знаками (контрарные атомы) формируют третий дизъюнкт - резольвенту, в которой будут исключены контрарные пропозициональные переменные. Неоднократно применяя это правило к множеству дизъюнктов и резольвент, стремятся получить пустой дизъюнкт. Наличие пустого дизъюнкта свидетельствует о выполнении условия F1&F2&F3&...&Fn&ùB=л.
1.4.1 Алгоритм вывода по принципу резолюции Шаг 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&А –отрицание заключения; множество дизъюнктов: K={(АÚC); (BÚC); (ùАÚùC); (ùBÚùC); C; А }; СÚ(ùАÚùC)=ùА – резольвента из 2) и 3); K1={(АÚC); (BÚC); (ùАÚùC); (ùBÚùC); C; А; ùА }; ùАÚ(АÚC)=C – резольвента из 1) и 5); K2={(АÚC); (BÚC); (ùАÚùC); (ùBÚùC); C; А; ùА }; СÚ(ùBÚùC)=ùB –резольвента из 2) и 5); 10) K3={(АÚC); (BÚC); (ùАÚùC); (ùBÚùC); C; А; ùА ; ùB }; 11) ùBÚ(BÚC)=C – резольвента из 1) и 9); CÚùA=(CÚùA) – резольвента из 5) и 11); K4={(АÚC); (BÚC); (ùАÚùC); (ùBÚùC); C; А; ùА; ùB; (CÚùA)}; (CÚùA)Ú (ùАÚùC)=ùА – резольвента из 2) и 12); K5={(АÚC); (BÚC); (ùАÚùC); (ùBÚùC); C; А; ùА; ùB; (CÚùA)}; ùАÚ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 - отрицание заключения; множество дизъюнкций: 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=ÿ - пустая резольвента.
|