Файл: В. Ф. Пономарев математическая логика.doc

=(AA’)(BB’) - посылка;

2) F₂=(AA’) - заключение по формуле F₁ и правилу удаления логической связки конъюнкции;

3) F₃=(BB’) - заключение по формуле F₁ и правилу удаления логической связки конъюнкции;

4) F₄=(AB’)(BA’) - посылка;

5) F₅=(AB’) - заключение по формуле F₄ и правилу удаления логической связки конъюнкции;

6) F₆=(BA’) - заключение по формуле F₄ и правилу удаления логической связки конъюнкции;

7) F₇=(B’A) - заключение по формуле F₅ и закону контрапозиции;

8) F₈=(A’B) - заключение по формуле F₆ и закону контрапозиции;

9) F₉=(AB) - посылка;

10) F₁₀=AB - заключение по формуле F₉ и правилу эквивалентного преобразования;

11) F₁₁=AA’ - заключение по формулам F₆, F₁₀ и закону силлогизма;

12) F₁₂= B’A’ - заключение по формулам F₇, F₁₁ и закону силлогизма;

13) F₁₃= A’A - заключение по формуле F₂ и закону контрапозиции;

14) F₁₄=A’B - заключение по формулам F₁₀, F₁₃ и закону силлогизма;

15) F₁₅=A’B’ - заключение по формулам F₃, F₁₄ и закону силлогизма;

16) F₁₆= (B’A’)(A’B’)=(B’A’) – заключение по формулам F₁₂, F₁₅ и правилу введения логической связки конъюнкции.

Так доказана истинность формулы (B’A’).

Пример. "Если Петров говорит неправду (A), то он заблуждается (В) или сознательно вводит в заблуждение других (С). Петров говорит неправду и явно не заблуждается. Следовательно, он сознательно вводит в заблуждение других" [2]

А(ВС); AB

С.

1) F₁=А(ВС) - посылка;

2) F₂=AB - посылка;

---

3) F₃=A - заключение по формуле F₂ и правилу 2);

4) F₄=B - заключение по формуле F₂ и правилу 2);

5) F₅=(ВС) - заключение по формулам F_1, F₃ и правилу m. p.;

6) F₆=C - заключение по формулам F_4, F₅ и правилу 5).

Так доказано, что Петров сознательно вводит в заблуждение других.

П ример: Доказать истинность заключения
А;В;(АС   В)

 C. 1) F₁=A  C   B - посылка;2) F₂=B - посылка;

3) F₃= ( A  C ) - заключение по формулам F₁, F₂ и правилу m. t.;

4) F₄= A - посылка;

5) F₅= C - заключение по формула F₃, F₄ и правилу 2).

Процесс дедуктивного вывода удобно проследить на графе, вершинами которого являются формулы, а дугами – отношения между ними (см. рис.1).

B

ACB

A



(AC)

C

Рис.1. Граф вывода заключения

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

(AB); (AC); (BD)

(CD).

1) F₁=(AC) посылка;

3. 
   F₂=(AB)(CB) заключение по формуле F₁ и правилу 9);
   

3) F₃=(BD) посылка;

4) F₄=(CB)(CD) заключение по формуле F₃ и правилу 9);

5) F₅=(AB)(CD) заключение по формулам F₂ и F₄ и правилу 11);

6) F₆=(AВ) посылка;

7) F₇=(CD) заключение по формулам F₅ и F₆ и правилу m. p..

Так доказана истинность заключения (CD).


AC

BD

AВ



(AB)(CB)

(CB)(CD)

---

(AB)(CD)


CD


Рис. 2. Граф вывода заключения

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

(AB)(CD); ( DBE );  E

C A.

1) F₁=(DBE) посылка;

2) F₂=E посылка;

3) F₃=(DB) заключение по формулам F₁ и F₂ и правилу m. t.;

4) F₄=(АВ)(СD) посылка;

5) F₅=(AВ) заключение по формуле F₄ и правилу 2);

6) F₆=(СD) заключение по формуле F₄ и правилу 2);

7) F₇=(BA) заключение по формуле F₅ и правилу 8);

8) F₈=(DB) заключение по формуле F₃ и закону де Моргана;

9) F₉=(DB) заключение по формуле 8) и правилу введения ипликации;

10) F₁₀=(D A) заключение по формулам F₇ и F₉ и правилу 11);

11) F₁₁=(С A) заключение по формулам F₆ и F₁₀ и правилу 11);

12) F₁₂=(С A) заключение по формуле F_II и правилу введения дизъюнкции.


(АВ)(СD)

(DBE)

E



(AВ)

(СD)

(DB)


(DB)


(BA)


(D A)

(DB)

Рис.3. Граф вывода заключения


(С A)

(С A)

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

((A  B) С); (С(D  M )); (MN); (( D)( N))

 A.

1) F₁=(( D)( N)) посылка;

2) F₂=N заключение по формуле F₁ и правилу 2);
3) F₃=(MN); посылка ;

4) F₄=M заключение по формулам F₂ и F₃ и правилу m.t;

5) F₅=D заключение по формуле F₁ и правилу 2);

6) F₆=(D)(M) заключение по формулам F

---

₄ и F₅ и правилу 1);

7) F₇=(DМ) заключение по формуле F₆ и закону де Моргана;

8) F₈=(( AB)C) посылка;
9) F₉=(С (DМ)) посылка;

10) F₁₀=((AB)(DM)) заключение по формулам F₈ и F₉ и правилу 11);

11) F₁₁=(AB) заключение по формулам F₇ и F₁₀ и правилу m.t.;

12) F₁₂=(А)(B) заключение по формуле F₁₁ и закону де Моргана;

13) F₁₃=A заключение по формуле F₁₂ и правилу 2).


((D)(N))

(MN)

(( AB)C)

(С(DМ))


(D)

(N)

(M)

( AB)(DМ)


(D)(M)

(DМ)

(AB)


(А)(B)

A



Рис. 4. Граф вывода заключения
Эти примеры показывают, что правила вывода обеспечивают ло­гическую последовательность в преобразовании формул, каждая из которых есть либо посылка, либо промежуточный результат, либо заключение.

4. 
   Принцип резолюции
   

Существует эффективный алгоритм логического вывода - алгоритм резолюции. Этот алгоритм основан на том, что выводимость формулы В из множества посылок 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.4.1 Алгоритм вывода по принципу

резолюции

Шаг 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А –отрицание заключения;

4. 
   множество дизъюнктов: K={(АC); (BC); (АC); (BC); C; А };
   
5. 
   С(АC)=А – резольвента из 2) и 3);
   
6. 
   K₁={(АC); (BC); (АC); (BC); C; А; А };
   
7. 
   А(АC)=C – резольвента из 1) и 5);
   
8. 
   K₂={(АC); (BC); (АC); (BC); C; А; А };
   
9. 
   С(BC)=B –резольвента из 2) и 5);
   

---