Логика - доступно для всех

  • Увеличить размер шрифта
  • Размер шрифта по умолчанию
  • Уменьшить размер шрифта

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

Поможем написать любую работу на аналогичную тему

Получить выполненную работу или консультацию специалиста по вашему учебному проекту
Узнать стоимость

Шаг 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).     

     

A

 
 

(ù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=ÿ - пустая резольвента.

C

 
                                                                                                                     

                       

(BÚD)

 

(CÚD)

 

C

 

N

 

(ùCÚN)

 
 

 

 

 

 

 


ùN

 
                                                        ùN

                                  ÿ

 

                                                                                

Рис. 7. Граф доказательства.


 

A

 
1) AÚ(ùAÚC)=C – резольвента из 1) и 6);

С

 

(ùAÚC)

 
2) CÚ(ùCÚN)=N – резольвента из 3) и 14);

N

 

(ùCÚN)

 
 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= ÿ - пустая резольвента.                                  

ùA

 
                                                                                             

Рис. 9 Граф доказательства                                                ÿ

 

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

Внимание!
Если вам нужна помощь в написании работы, то рекомендуем обратиться к профессионалам. Более 70 000 авторов готовы помочь вам прямо сейчас. Бесплатные корректировки и доработки. Узнайте стоимость своей работы.

 

 

Случайная новость