Главная страница | Контакты | Случайная страница Автомобили Астрономия Биология География Дом и сад Другие языки Другое Информатика История Культура Литература Логика Математика Медицина Металлургия Механика Образование Охрана труда Педагогика Политика Право Психология Религия Риторика Социология Спорт Строительство Технология Туризм Физика Философия Финансы Химия Черчение Экология Экономика Электроника

Метод резолюций в логике высказываний.

Метод резолюций

Существует эффективный алгоритм логического вывода - алгоритм резолюции. Этот алгоритм основан на том, что выводимость формулы В из множества посылок F₁; F₂; F₃;... F_n равносильна доказательству теоремы

|¾(F₁&F₂&F₃&...&F_n®B),

формулу которой можно преобразовать так:

|¾(F₁&F₂&F₃&...&F_n®B) =

|¾(ù(F₁&F₂&F₃&...&F_n)ÚB) =

|¾ù(F₁&F₂&F₃&...&F_n&(F₂ù B)).

Следовательно, заключение В истинно тогда и только тогда, когда формула (F₁&F₂&F₃&...&F_n&(ùB))=л. Это возможно при значении “л” хотя бы одной из подформул F_i илиùB.

Для анализа этой формулы все подформулы F_i иùB должны быть приведены в конъюнктивную нормальную форму и сформировано множество дизъюнктов, на которые распадаются все подформулы. Два дизъюнкта этого множества, содержащие пропозициональные переменные с противоположными знаками (контрарные атомы) формируют третий дизъюнкт - резольвенту, в которой будут исключены контрарные пропозициональные переменные. Неоднократно применяя это правило к множеству дизъюнктов и резольвент, стремятся получить пустой дизъюнкт. Наличие пустого дизъюнкта свидетельствует о выполнении условия F₁&F₂&F₃&...&F_n&ùB=л.

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

Шаг 1. принять отрицание заключения, т.е. ù В;

Шаг 2. привести все формулы посылок и отрицания заключения к конъюнктивной нормальной форме (см. с.35);

Шаг 3. выписать множество дизъюнктов всех посылок и отрицания заключения:

K = {D₁; D₂;... D_k };

Шаг 4. выполнить анализ пар множества K по правилу:

“если существуют дизъюнкты D_i и D_j, один из которых (D_i) содержит литеру А, а другой (D_j) - контрарную литеру ùА, то соединить эту пару логической связкой дизъюнкции (D_i Ú D_j) и сформировать новый дизъюнкт - резольвенту, исключив контрарные литеры А и ùА;

Шаг5. если в результате соединения дизъюнктов, содержащих контрарные литеры, будет получена пустая резольвента - , то конец (доказательство подтвердило противоречие), в противном случае включить резольвенту в множество дизъюнктов K и перейти к шагу 4.

Пример: Работа автоматического устройства, имеющего три клапана А, В и С, удовлетворяет следующим условиям: если не срабатывают клапаны А или В или оба вместе, то срабатывает клапан С; если срабатывают клапаны А или В или оба вместе, то не срабатывает клапан С. Следовательно, если срабатывает клапан С, то не срабатывает клапан А [2].

((ùАÚùBÚùА &ùB)®С); ((AÚBÚА&B)®ùC)

(C®ùA).

1) F₁=((ùАÚùBÚùА &ùB)®С)= (АÚC)&(BÚC) - посылка;

2) F₂=((AÚBÚА&B)®ùC)= (ùАÚùC)&(ùBÚùC) -посылка;

3) F₃=ù (C®ùA)=C&А –отрицание заключения;

1) множество дизъюнктов: K={(АÚC); (BÚC); (ùАÚùC); (ùBÚùC); C; А };

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

3) K₁={(АÚC); (BÚC); (ùАÚùC); (ùBÚùC); C; А; ùА };

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

5) K₂={(АÚC); (BÚC); (ùАÚùC); (ùBÚùC); C; А; ùА };

6) СÚ(ùBÚùC)=ùB –резольвента из 2) и 5);

10) K₃={(АÚC); (BÚC); (ùАÚùC); (ùBÚùC); C; А; ùА; ùB };

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

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

13) K₄={(АÚC); (BÚC); (ùАÚùC); (ùBÚùC); C; А; ùА; ùB; (CÚùA)};

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

15) K₅={(АÚ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) K₁={A; B; (ùCÚùAÚùB); C; (ùСÚùB)};

8) BÚ(ùСÚùB)=ùC - резольвента из 2) и 6);

9) K₂={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) K₁={(ùAÚùBÚC); (ùCÚùDÚùM); (NÚD); (NÚM); A; B; M; ùN};

8) (DÚN)ÚùN=D - резольвента из 3) и 4);

9) K₂={(ù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) K₃={(ù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) K₄={(ù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) K₅={(ù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) K₆={(ù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)®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=ÿ - пустая резольвента.

Так как резольвенты включаются в множество дизъюнктов S, то возможно неоднократное их использование в процессе вывода. Многократное использование дизъюнкт множества S оправдано законом идемпотентности, т.к. D_i=D_i&D_i&...&D_i.

Пример: Доказать истинность заключения

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