Аналитическое и формальное доказательство теорем в исчислении высказываний

Размещено на http://www.allbest.ru/

«Аналитическое и формальное доказательство теорем в исчислении высказываний»

Содержание

1. Введение

2. Задание

3. Описание и решение задачи

3.1 Аналитическое прямое доказательство истинности заключения (теоремы)

3.2 Аналитическое доказательство истинности заключения (теоремы) от противного

3.3 Доказательство теоремы по методу пропозициональной резолюции

4. Содержательный (словесный) алгоритм по методу Вонга

5. Блок-схема алгоритма доказательства теоремы по методу Вонга

6. Содержательный (словесный) алгоритм по методу пропозициональной резолюции

7. Блок-схема алгоритма доказательства теоремы по методу пропозициональной резолюции

8. Сравнительный анализ алгоритмов

Заключение

Список литературы

Приложение

а) Программа (для метода пропозициональной резолюции)

б) Результат выполнения программы

1.Введение

Логика образует такой пласт общечеловеческой культуры, без освоения которого в настоящее время не может состояться ни одна мыслящая личность. Основы логической культуры закладываются в школе и в первую очередь на уроках математики, ибо, как точно подметил еще Л. Н.Толстой, «математика имеет задачей не обучение исчислению, но обучение приемам человеческой мысли при исчислении».

Математическая логика -- вершина развития логики, достигнутая ею в XX в. Органично соединив в себе традиционную логику, восходящую к Аристотелю, и методы современной математики, она получила столь глубокие и поразительные результаты, не принимать в расчет которые стало просто невозможно не только тем, кто изучает, преподает и творит математику, но и всем тем, для кого методы рассуждений, обоснований и доказательств являются главными методами деятельности.

Результаты, полученные с помощью математической логики, легли в основу проектирования и создания электронно-вычислительных машин (компьютеров) и программного обеспечения к ним, нашли широчайшее применение в областях информатики и систем искусственного интеллекта.

2. Задание

доказательство теорема исчисление высказывание

Исходные данные

Доказать справедливость (истинность или ложность) данного предложения (формулы):

Посылки : A > ?(B ? C), D ? E > G, G > ?(H ? I)

Теорема : D > (G ? ?H)

Правильно построенная формула (ППФ):

A > ?(B ? C), D ? E > G, G > ?(H ? I) => D > (G ? ?H)

3. Описание и решение задачи

3.1 Аналитическое прямое доказательство истинности заключения(теоремы)

В основе прямого доказательства истинности заключения лежит первая версия теоремы дедукции, которая гласит:

Формула Q (теорема, предложение) истина тогда и только тогда, когда формула

P1 P2… PnQ, (1)

где: P1,…,Pn - формулы посылок, Q - формула теоремы,

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

1. Подставить в формулу (1) данные значения;

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

Следовательно, теорема истинна.

3.2 Аналитическое доказательство истинности заключения (теоремы) от противного

В основе доказательства теоремы от противного лежит вторая версия

( следствие) теоремы дедукции, которая гласит:

- формула Q ( теорема, предположение) истинна тогда и только тогда, когда формула P1 P2… PnQ, (2) противоречива.

Действительно, если Q- истинна, то формула отрицания Q ложна, следовательно, из свойства конъюнкции вытекает, что формула (2) противоречива.

Таким образом, для доказательства теоремы от противного, надо осуществить поиск противоречия в формуле (2)

Алгоритм поиска противоречия в формуле (2) построен на методе пропозициональной резолюции, в основе которого лежит принцип силлогизма, позволяющий из двух предложений получить третье истинное предложение.

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

1) подставим в формулу (1) посылки и теорему, указанные в задании.

2) доказать или опровергнуть общезначимость данной теоремы с помощью законов равносильности логики высказываний.

Мы получили противоречие следовательно теорема доказана.

3.3 Доказательство теоремы методом пропозициональной резолюции

Представим формальное доказательство теоремы методом резолюции:

A > ?(B ? C), D ? E > G, G > ?(H ? I) => D > (G ? ?H)

Для этого алгоритма необходимо брать отрицание теоремы:

ПОСЫЛКИ - (?A ? ?B ? ?C) ? (G ? ?D) ? (G ? ?E) ? (?G ? ?H) ? (?G ? ?I)

ОТРИЦАНИЕ ТЕОРЕМЫ - D ? (?G ? H)

Заменив запятой, получим множество ППФ (дизъюнктов)

?A??B??C, G??D, G??E, ?G??H, ?G??I, D, ?G?H

Делим посылки и теорему на 1-элементные, 2-хэлементные и 3-хэлементные:

1-элементные	D	G	?H	?I	?G
2-элементные	G??D	G??E	?G??H	?G??I	?G?H
3-элементные	?A??B??C

Для доказательства теоремы необходимо, чтобы в группе одноэлементных ППФ встретилась одна и та же переменная с отрицанием и без отрицания.

G и ?G - в первой группе, следовательно теорема доказана.

4. Содержательный(словесный) алгоритм доказательства теорем по методу Вонга

Vн Начало

V1 Ввести формулы посылок и теоремы

Z1 Проверить формулы посылок и теоремы на наличие знаков эквиваленции. Если есть, то перейти к п. V2, иначе - к п. Z2

V2 Заменить эквиваленцию по формуле:

Z2 Проверить все формулы посылок и теоремы на наличии знака импликации. Если есть импликация, то переходим к п. V3, иначе к п. Z3

V3 Заменить импликации дизъюнкциями по формуле:

Z3 Проверить все формулы посылок и теоремы на наличие общего отрицания, связывающего два или более букв. Если есть общее отрицание, то переходим к п. V4, иначе к п. Z4

V4 Применить правило де Моргана: ,

Z4 Проверить все формулы и теоремы на наличие второго отрицания. Если есть, то перейти к п. V5,иначе к п.Z5.

V5 Заменить А на А.

Z5 Проверить формулу посылок и теорему на наличие дистрибутивности. Если есть, то перейти к п.V6,иначе к п.V7.

V6 Применяем дистрибутивный закон:

,

V7 Выписать формулы посылок слева от стрелки, формулы теоремы справа.

V8 Заменяем на запятые все конъюнкции слева от стрелки и дизъюнкции справа от стрелки.

Z6 Проверить есть ли одинаковые и несвязанные переменные без отрицания или с отрицанием слева и (или) справа от стрелки. Если есть, то перейти к п.V9, иначе к п.Z7.

V9 Все одинаковые высказывательные переменные слева или справа вычеркнуть, кроме 1.

Z7 Проверить есть ли две одинаковые несвязанные переменные с отрицанием и без отрицания, слева или справа от стрелки. Если есть, то перейти к п.V10, иначе к п.Z8.

V10 Высказывательные переменные с отрицанием перенести слева направо от стрелки или справа налево от стрелки. Пометить, что этострока закрыта (доказана).

Z8 Проверить все ли формулы посылок раскрыты.Если нет, то перейти к п.Z9, иначе к п.V11.

Z9 Проверить все ли переменные несвязны и одна переменна слева и справа от стрелки в одинаковой форме. Если да, то перейти к п.V11, иначе к п.V12.

V11 Вывести решение “теорема истинна” на конец.

V12 Разбить i-ю посылку на строки по каждой высказывательной переменной, перейти к п.Z6.

Z10 Проверить все ли высказывательные переменные несвязны (разные). Если да, то перейти к п.V13, иначе к п.V12.

V13 Вывести решение “теорема ложна”.

Vk Конец.

5.Блок - схема алгоритма доказательства теоремы по методу Вонга

V_н

Z₁

Z₂

Z₃

Z₄

Z₅

А

А

Z₆

Z₇

Z₈

Z₉

V₁₂

V_k

6. Содержательный(словесный) алгоритм доказательства теоремы по методу пропозициональной резолюции

1. (Vn) Начало

2. (V1) Вводим посылки и теорему

3. (Z1) Проверяем все формулы на наличии эквиваленции

Если есть эквиваленция, то переходим к п. V2, иначе - к п. Z2

4. (V2) Заменяем эквиваленцию по формуле:

5. (Z2) Проверяем все формулы на наличии импликации

Если есть импликация, то переходим к п. V3, иначе - к п. Z3

6. (V3) Заменяем импликации дизъюнкциями по формуле:

7. (Z3) Проверяем все формулы на наличие общей инверсии

Если есть общая инверсия, то переходим к п. V4, иначе - к п. Z4

8. (V4) Применяем правило де Моргана: ,

9. (Z4) Проверяем все формулы на наличие дистрибутивности

Если есть дистрибутивность, то переходим к п. V5, иначе к п. V6

10. (V5) Применяем дистрибутивный закон:

,

11. (V6) Все полученные предложения (дизъюнкты) помещаются в единую группу из n элементов, (n=1,2,3…)

12. (V7) Отбираем из группы (полученная выше) по очерёдности, от 1 до n, одно предложение(a1), которое ранее не бралось

13. (V8) Отбираем из группы второе предложение (a2), такое что оно не

является a1, и ранее не бралось (после последнего отбора предложения a1)

14. (Z5) Если в группе нет предложений (a1), которые ранее не брались, то теорема ложна, и переходим к п.Vk. Иначе к п. V9

15. (V9) Из этих двух предложений строится новое предложение (a3), состоящее из соединенных связкой И элементов двух отобранных предложений, причём включаются все элементы, кроме и . Предложение s1 заменяется полученным предложением (a3)

16. (Z6) Если в группе нет предложения (a2) которые ранее не брались, то переходим к пункту V8. Иначе к п. Z7

17. (Z7) Если в одном из двух предложений существует такая переменная, что в другом предложении существует переменная, то переходим к п.V10.

Иначе к п.V9.

18. (V10) Вновь образованное предложение включается в группу и переходим к п.V9

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

Иначе к п. V11

20 .(Vk) Конец.

7. Блок-схема алгоритма доказательства теоремы по методу пропозициональной резолюции

нет

да

да

нет

нет

да

да

нет

нет

да нет да

да

нет

нет

да

Заключение

В данной курсовой работе были рассмотрены различные методы доказательств теорем исчисления высказываний:

1. Аналитические:

- Прямое доказательство истинности теоремы

- Доказательства истинности теоремы от противного

2.Формальные

- доказательство теоремы методом Вонга

- доказательство теоремы методом пропозициональной резолюции

Особо тщательно были рассмотрены формальные методы доказательства теорем. К каждому из методов давались словесные (содержательные) алгоритмы и блок-схема по алгоритму. Для метода пропозициональной резолюции приводится программа, реализованная на языке Turbo Pascal, и результаты выполнения программы для курсового задания.

В результате выполнения данной курсовой работы я узнал много нового касающегося как программирования, так и методов доказательства теорем высказываний. Работа была очень интересной, хотя временами и возникали некоторые трудности в области программирования; программная реализация метода оказалась довольно трудной, чем предполагалась в начале выполнения работы.

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

Список литературы

1. Гаджиев А.А. Курс лекций по дисциплине «МЛиТА». 2002.

2. Гаджиев А.А. Методические указания к выполнению лабораторного практикума по дисциплине “Математическая логика и теория алгоритмов”. Махачкала. ДГТУ. 2003.

3. Новиков Ф.А. Дискретная математика для программистов. Санкт-Петербург. Питер. 2001.

4. Столл Р. Множества. Логика. Аксиоматические теории. Москва. Просвещение. 1968.

5. Мендельсон Э. Введение в математическую логику. Москва. Наука. 1976.

Приложение

а) Программа (для метода пропозициональной резолюции)

Program PROPOZ_REZOLUTION;

Uses Crt;

VAR A: Array[1..10] of string;

i,k,kol,i1,k1,m: INTEGER;

c: Char;

Pust: Set of Char;

St,s1,s2,Teo : string;

Yes,Teor,Yes1 : Boolean;

Perem,Perem1,P : Set of char;

Const Posl: string='A+B+C,g+D,g+E,G+H,G+I,d,G+h';

Procedure Space (var s:string);

var i: integer;

begin

i:=1;

While i<length(s) do begin

if s[i]='' then Delete(s,i,1)

else i:=i+1;

end; end;

Procedure Zpt(c:char; var s:string);

var I:integer;

begin

For i:=2 to length(s)-1 do

if s[i]=c then s[i]:=','

else if (s[i]='(') or (s[i]=')') then s[i]:=' ';

Space(s);

end;

Procedure Dis(f:char; Var s:string);

var I,K,T,V,M: integer; C: string;

begin

i:=1;

While i<=Length(S) do begin

i:=i+1;

if (S[i-1]=f) and (S[i]='(') then begin

S[i]:=' ';

t:=1;

k:=i;

while (S[k]<>',') and (k>1) do k:=k-1;

v:=i-k-1;

C:=Copy(S,k+1,v);

For m:=k+1 to k+1+v do S[m]:=' ';

end;

if (t=1) and (S[i]=')') then begin

t:=0;

S[i]:=' ';

end;

if (t=1) and (S[i] in P) then begin

Insert (C,S,i);

i:=i+v;

end; end;

Space(s); end;

Procedure Vvod;

var

i,k,n: integer;

s: string;

begin

i:=1;

While i<length(Posl) do begin

if Posl[i]='+' then Delete (Posl,i,1)

else i:=i+1;

end;

i:=0; k:=0;

While k<=length(Posl) do begin

k:=k+1;

if Posl[k]=',' then i:=i+1;

end;

for k:=1 to i do begin

a[k]:=copy(posl,1,pos(',',posl)-1);

Delete (Posl,1,pos(',',posl));

end;

a[i+1]:=Posl;

Kol:=i+1;

Space(s);

end;

Procedure dok (s1,s2: string; var yes : boolean; var st: string);

var sim: char; p:byte;

i,k: integer;

Procedure plus(s: string);

var i:integer;

begin

for i:=1 to length(s) do

if s[i]<>'' then St:=st+s[i];

end;

begin

St:='';

yes:=false;

for i:=1 to length(s1) do begin

p:=0;

for k:=1 to length(s2) do begin

if s1[i]<>s2[k] then

if (ord(s1[i])>64) and (ord(s1[i])<97)

then Sim:=chr(ord(S1[i])+32)

else if ord(s1[i])>=97 then Sim:=UpCase(S1[i]);

if (sim=s2[k]) and (p=0) then begin

p:=1;

yes:=true;

s1[i]:=' ';

s2[k]:=' ';

end; end; end;

if yes=true then begin

Plus(s1); Plus(s2);

if st='' then begin

textcolor(2);

Write ('Teorema Dokazana');

Halt;

end end; end;

BEGIN

textbackground(1);

Teor:=True;

Perem:=['a'..'z']; Perem1:=['A'..'Z'];

P:=Perem+Perem1;

Clrscr;

Write('TEOREMA: ');

read(teo);

writeln(posl);

readkey;

Dis('+',Posl);

Zpt('*',Posl);

Vvod;

for i:=1 to kol-1 do

for k:=i+1 to kol do

begin

s1:=a[i]; s2:=a[k];

if (a[i]<>'') and (a[k]<>'') then

dok(s1,s2,Yes,st);

end;

While Teor do begin

Yes:=False;

for i:=1 to kol-1 do

for k:=i+1 to kol do begin

s1:=a[i]; s2:=a[k];

if (a[i]<>'') and (a[k]<>'') then

dok (s1,s2,Yes,st);

if yes then begin

a[i]:=St;

a[k]:='';

for i1:=1 to kol-1 do

for k1:=i1+1 to kol do

begin

s1:=a[i1]; s2:=a[k1];

if (a[i1]<>'') and (a[k1]<>'') then

dok (a[i1], a[k1],Yes1,st);

end; end; end;

if not yes then begin

Teor:=False;

textcolor(4);

writeln ('Teorema ne dokazana');

end; end;

readkey;

END.

б)Результаты выполнения программы

Размещено на Allbest.ru