Математическая логика: часть 1 - Учебное пособие (Пономарев В.Ф.)

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).       

                                                             

 

 

 

 

 

 

(ùAÚB)

 

                                                                         

                                                                                B

                                                                                                                                             

(ùDÚùBÚM)

 

                                                              (ùDÚM)                                                     

 

(ùCÚD)

 

                                                              (ùCÚM)

 

 

 

ùM

 

 

                                                      ùC

 

 

 

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ÚC)

 

 

) 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);

Следует обратить внимание, что при выводе заключения дважды получена резольвента С. Это говорит об избыточности посылок. Например, можно удалить (C®(DÚB)), формирующую дизъюнкт (BÚùCÚD). Это существенно сократит вывод заключения. На рис. 8 показан вывод заключения без учета посылки (C®(DÚB)).

 

 

13) NÚùN=ÿ - пустая резольвента.

 

 

 

 

A

 

 

(ùAÚC)