Напишем:


✔ Реферат от 200 руб.
✔ Контрольную от 200 руб.
✔ Курсовую от 500 руб.
✔ Решим задачу от 20 руб.
✔ Дипломную работу от 3000 руб.
✔ Другие виды работ по договоренности.

Узнать стоимость!

Не интересно!

 

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

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

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

Шаг 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 Граф доказательства                                                ÿ

 

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

 

 
Здесь можно купить вино Шато Мутон Ротшильд

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