A®B; B®C; C 4 страница

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

 

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

 

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

 

 

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

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)

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Ú(ù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

 

 

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

ùA

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

 

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

 

1.5 Проблемы в исчислении высказываний

Для обоснования исчисления высказываний, как для любой аксиоматической теории, необходимо рассмотреть проблемы разрешимости и непротиворечивости.

Проблема разрешимости исчисления выказываний заключена в доказательстве существования алгоритма, который позволил бы для любой формулы исчисления высказываний определить ее доказуемость. Любая формула исчисления высказываний может быть представлена формулой алгебры высказываний. Эффективность процедуры разрешения показана таблицами истинности для различных наборов значений пропозициональных переменных.

Проблема непротиворечивости исчисления высказываний заключена в доказательстве невыводимости формулы и ее отрицания.

Исчисление высказываний непротиворечиво, т. к. каждая формула, доказуемая в исчислении высказываний, является тождественно истинной формулой в алгебре высказываний и легко проверяется на таблицах истинности. Тогда отрицание формулы не является тождественно истинной формулой, что проверяется на таблицах истинности и при доказательстве в исчислении высказываний ведет к противоречию.

1.6 Описание высказываний на языке PROLOG

Для программирования задач исчисления высказываний используют язык программирования Prolog.Само название Prolog есть сокращение, означающее про граммирование в терминах лог ики.

Пролог-программа состоит из предложений, которые бывают трех типов: факты, правила и вопросы.

Факты есть высказывания, которые заканчиваются точкой и имеют значение только “и”. Структура такого предложения описана предикатом или n-местным отношением, все аргументы которого есть термы или предметные постоянные. Предметные постоянные на языке PROLOG называют атомами. Термы описывают структуру или какие-то функциональные отношения между атомами. Предметные постоянные всегда начинаются со сточной буквы латинского алфавита и представляют собой последовательность букв, цифр и знака подчеркивания.

Например,

· простое_число(3).

Это есть высказывание A1 (см. с. 5), структура которого описана предикатом P1(x):=”x-простое число”, где x=3 есть атом.

· частное_от_деления(6, 2, 3).

Это есть высказывание Е (см. с.6), структура которого описана предикатом P₃(x, y, z):=”z есть частное от деления числа x на y”, где x=6, y=2, z=3 есть атомы.

· студент_университета,_обучающийся_по_специальности(Петров, КГТУ, прикладная информатика").

Это есть высказывание, структура которого описана предикатом

P₆(x, y, z):= "студент x университета y, обучающийся по специальности z”, где x=”Петров”, y=”КГТУ”, z=”прикладная информатика” есть атомы.

· родословная русских князей X века:

отец(игорь, святослав).

отец(святослав,владимир).

отец(владимир, борис).

отец(владимир,глеб).

дед(игорь, владимир).

дед(святослав, борис).

дед(святослав, глеб).

брат(борис,глеб).,

 

где игорь, святослав, владимир, борис, глеб есть атомы. Правила есть предложения, истинность которых зависит от истинности условий: “если истинны условия (посылки), то истинно и заключение (вывод)”.

На языке Prolog эти правила записывают так:

<заключение>:- <условия>.

Символ “:-“ соответствует символу обратной импликации ””.

Левую часть правила называют головой предложения, а правую – телом предложения. В теле предложения перечисляют условия, определяющие вывод заключения. Если условия имеют между собой конъюнктивную связь, то между ними ставится запятая “,”. Если условия в правиле имеют между собой дизъюнктивную связь, то между ними ставится точка с запятой (“;”). Голова предложения всегда сдвинута влево относительно перечня условий. Каждое условие начинается с новой строки.

Например, для родословной русских князей X века имеем:

· дед(игорь, владимир):-

отец(игорь, святослав),

отец(святослав, владимир).

Это - высказывание о том, что если игорь был отцом святослава, а святослав – отцом владимира, то игорь был дедом владимиру.

· дед(святослав, борис); дед(святослав, глеб):-отец(святослав,владимир),

отец(владимир, борис);

отец(святослав,владимир),

отец(владимир,глеб).

Это есть высказывание о том, что святослав был отцом владимира и дедом борису или глебу.

· брат(борис, глеб):-.

родитель (владимир, борис),

родитель (владимир,глеб).

Это есть высказывание о том, что если владимир был отцом бориса и отцом глеба, то борис и глеб были братьями

 

2. ЛОГИКА ПРЕДИКАТОВ

Если объект высказывания, т.е. о чем говорится в предложении, не определен, то это предложение называют высказывательной функцией. Аргументами высказывательной функции являются предметные переменные, которые обозначают строчными буквами латинского алфавита х, у,z ¼; Эта функция приобретет значение "и" или "л" только при подстановке в высказывательную функцию вместо предметных переменных их конкретных значений. Конкретные значения аргументов высказывательной функции называют предметными постоянными, которые обозначают строчными буквами латвийского ал­фавита а, в, с, ¼.

Высказывательную функцию иначе называют предикатом (лат. praedicatum - логическое сказуемое).

Например,

а) если на множестве натуральных чисел задать высказывательные функции или предикаты

Р₁(x):= "x - простое число",

P₂(6, y):="y меньше 6",

P₃(6, y, z):="z есть частное от деления числа 6 на y",

где z и y есть предметные переменные (целые числа), а 6 – предметная постоянная (целое число), то высказываниями будут

P₁(3) = и, P₁(4) = л,

P₂(6,2) = и, P₂(6,7) = л,

P₃(6,2,3) = и, P₃(6,2,5) = л,

б) если на множестве имен индивидов, университетов и специальностей задать высказывательные функции или предикаты

P₄(x):="х - студент",

P₅(x, КГТУ):="студент х университета КГТУ",

P₆(x, y, прикладная информатика):= "студент x университета y, обучающийся по специальности "прикладная информатика””,

где x и y есть предметные переменные, а КГТУ и “прикладная информатика” – предметные постоянные, то высказываниями будут

P₄(Петров) = и, P₄(Сидоров) = л,

P₅(Петров, КГТУ) = и, P₅(Сидоров, КГТУ) = л,

P₆(Петров, КГТУ, "прикладная информатика") = и,

P₆(Сидоров, КГТУ, "прикладная информатика") = л.

При ограничении области определения предметных переменных вводят операторы, которые называют кванторами.

Суждение, в котором утверждается или отрицается наличие каких-либо признаков или отношений у части предметных переменных области определения, называют частным суждением. Как правило, эти суждения на естественном язы­ке отражают словами “один”, "несколько", "часть" и т.п. Для формализации таких суждений используют логическую операцию, ограничивающую область определения предиката. Этот оператор по­лучил название квантора существования, который обозна­чают так: “ $_x ”. Предикат записывают после квантора существования в круглых скобках $_x (Р_n (x)) На естественном языке эта запись означает: “существуют такие элементы х, что Рn(х) истинно (или ложно)".

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

$ _x, $ _y, $ _z,...(P_n(x, y, z,...)).

Для обозначения числа аргументов предиката часто используют верхние индексы. Например, часто записывают так

Р(х₁,x₂,x₃, ¼ x_n) = Рⁿ (х).

 

Например,

$_x(P₁(x)):= "cуществуют целые числа, которые являются простыми". Это условие выделяет на множестве целых чисел подмножество X = {2, 3, 5, 7, 11, 13, 17,...}, для которого предикат P₁(x) принимает значение “и”.

$_y(P²₂(6,y)):="существуют числа y, которые меньше 6". Это условие выделяет на множестве целых чисел подмножество

Y= {1, 2, 3, 4, 5}, для которого предикат P₂(6,y) принимает значение “и”.

$_y(P³₃(6,2,z)):="существует число z, которое является частным от деления 6 на 2". Это условие выделяет на множестве целых чисел единственное число Z=3, для которого предикат P₃(6,2,z) принимает значение “и”.

Если P₇(x):="x имеет зачетную книжку", то

$_x(P₄(x)&ùP₇(x)):= "существуют студенты (x), которые не имеют зачетной книжки";

$_x$_y(P²₅(x,y)& ùP₇(x)):="существуют студенты (x) некоторых университетов (y), которые не имеют зачетной книжки".

Суждение, в котором утверждается или отрицается наличие каких-либо признаков или отношений для всех предметных переменных области определения, называют общими суждениями. Как правило, эти сужде­ния в естественном языке отмечают словами "все", "каждый", "любой" и т.п. Для формализации этих суждений используют логическую операцию над всей областью определения предиката. Оператор этой логической операции получил название квантора всеобщности, который обозначают так: "_x. Предикат записывают после квантора всеобщности в круглых скобках