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

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

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

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

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

P₁ P₂ … P_n Q.

общезначима (т.е. тождественно истинна) где P₁, P₂, …, P_n — формулы посылок.

Q — формула теоремы На основе этой теоремы докажем истинность следующей формулы с помощью законов логики высказываний:

[()()() ()].

[() ()() ()]=.

= () () () ()=.

=.

= ()()D =.

= ()D =.

CD=.

=.

= `истина'.

Представим формальное доказательство теоремы по Вонгу.

[() () () ()].

Приведем к КНФ.

()()() () .

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

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

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

P₁ P₂ … P_n.

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

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

Алгоритм поиска противоречия построен на методе пропозициональной резолюции, в основе которого лежит принцип силлогизма.

Сущность, принципа силлогизма состоит в том, что из двух предложений вида (A B) и (A C) следует третье истинное предложение (B C) или.

[(A B) (A C)] (B C).

т.е. эта формула является общезначимой (тавтологией).

() () () () = =.

= [() () () ()] () =.

= () () () () =.

= () () () =.

= B ()C () =.

= BDC =.

BDC B= `ложь'.

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

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

() () () ().

Приведем к КНФ.

() () () ().

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

(), (), (), (),.

Граф — дерево доказательства от противного.

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

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

(V_H) Начало.

(V₁) 1. Ввести формулы посылок и теорему.

(Z₁) 2. Проверить формулы посылок и теорему на наличие знака эквиваленции, если есть, то перейти к п. 3, иначе к п. 4.

(V₂) 3. Заменить формулу AB на.

(Z₂) 4. Проверить формулы посылок и теорему на наличие знака импликации, если есть, то перейти к п. 5, иначе к п. 6.

(V₃) 5. Заменить формулу AB на.

(Z₃) 6. Проверить формулы посылок и теорему на наличие общего отрицания, связывающее две или более букв, если есть, то перейти к п. 7, иначе к п. 8.

(V₄) 7. Заменить на и на .

(Z₄) 8. Проверить формулы посылок и теорему на наличие двойного отрицания, если есть, то перейти к п. 9, иначе к п. 10.

(V₅) 9. Заменить на .

(Z₅) 10. Проверить формулы посылок и теорему на наличие дистрибутивности относительно, если есть, то перейти к п. 11, иначе к п. 12.

(V₆) 11. Заменить формулы на .

(V₇) 12. Выписать формулы посылок слева от стрелки, теорему справа.

(V₈) 13. Заменить слева и справа на запятую.

(Z₆) 14. Проверить есть ли одинаковые и несвязанные высказывательные переменные без отрицания, или с отрицанием, слева или справа от стрелки, если есть, то перейти к п. 15, иначе к п. 16.

(V₉) 15. Все одинаковые переменные слева и справа от стрелки вычеркнуть.

(Z₇) 16. Проверить есть ли две одинаковые и несвязанные высказывательные переменные без отрицания, или с отрицанием, слева или справа от стрелки, если есть, то перейти к п. 17, иначе к п. 18.

(V₁₀) 17. Высказывательную переменную с отрицанием перенести слева на права или справа на лево от стрелки с исключением знака отрицания. Пометить что эта строка закрыта (доказана).

(Z₈) 18. Проверить все ли формулы посылок раскрыты, если нет, то перейти к п. 19, иначе к п. 20.

(Z₉) 19. Проверить все ли переменные несвязны, и одна переменная слева и справа от стрелки в одинаковой форме, если да то перейти к п. 20, иначе к п. 21.

(V₁₁) 20. Выдать решение. Теорема доказана.

(V₁₂) 21. Разбить i — ю посылку на строки, по каждой высказывательной переменной, перейти к п. 14.

(Z₁₀) 22. Проверить все ли высказывательные переменные несвязны и разные.

Если да, то перейти к п. 23 иначе к п. 21.

(V₁₃) 23. Вывести решение. Теорема не доказуема и предположение не верно.

(V_К) Конец.

4. Содержательный словесный алгоритм и граф — схема алгоритма доказательства методом пропозициональной резолюции (к п. 3).

(Vn) Начало.

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

(Z1) 2. Проверяем все формулы на наличии эквиваленции, если есть эквиваленция, то переходим к п. 3, иначе — к п. 4.

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

(Z2) 4. Проверяем все формулы на наличии импликации, если есть импликация, то переходим к п. 5, иначе — к п. 6.

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

(Z3) 6. Проверяем все формулы на наличие общей инверсии, если есть общая инверсия, то переходим к п. 7, иначе — к п. 8.

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

(Z4) 8. Проверяем все формулы на наличие дистрибутивности, если есть дистрибутивность, то переходим к п. V5, иначе к п. V6.

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

.

(V6) 10. Полученную преобразованную формулу теоремы инвертируем.

(V7) 11. Все полученные предложения (дизъюнкты) помещаются в единую группу из n элементов.

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

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

(V9) 14. Отбираем из группы второе предложение (s2), такое что оно не является s1, и ранее не бралось (после последнего отбора предложения s1).

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

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

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

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

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

(Vк) Конец.

5. Сравнительный анализ формальных алгоритмов доказательства по Вонгу и метода пропорциональной резолюции.

Для сравнительной оценки логической сложности алгоритмов предлагается использовать количественную меру в виде полной энтропии (алгоритмической меры количества информации по Колмагороу) двоичной последовательности.

I_A(k, s) = n*H (k, s) (1).

где H (k, s) = - (log + log + + log) (2).

или H (k, s) = - (log + 2 * log) (3).

n — общее число входов безусловных и условных операторов содержательного алгоритма (граф — схема).

k — число входов безусловных операторов.

s₁ — число «единичных» выходов условных операторов.

s₀ — число «нулевых» выходов условных операторов.

s — число условных операторов (s = s₁ = s₀).

В формуле (1) I_K(k, s) = - n (log), бит — доля логической сложности алгоритма по безусловным операторам.

I_S(k, s) = - n (2 * log), бит — доля логической сложности алгоритма по условным операторам.

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

Для сравнительной оценки сложности двух альтернативных алгоритмов можно использовать формулу.

= (4).

где I (k, s) I (k, s).

Численное значение позволяет принять решение о выборе алгоритма для реализации программы:

— алгоритм, характеризующийся меньшим значением полной энтропии I (k, s) принимается для написания рабочей программы.

Заключение.

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

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

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

Приложение 1. (рабочая программа по методу пропозициональной резолюции).

uses crt;

Type mas=array [1. 50,1.40] of string[2];

VAR stp: mas;

sx:array [1.40] of byte;

i, j, n: byte;

{**************************************************************}.

{Процедура ввода и преобразования формул}.

Procedure Wwod;

var np, j, i, k, n1, n2: byte;

ss, s1: string; sc: char;

Procedure Obrab (c1, c2: char);

Procedure zamena;

var i: byte;

begin.

i:=pos ('(', s1);

while i<>0 do.

begin.

s1 [i]: =' (';

i:=pos ('(', s1);

end;

i:=pos (')', s1);

while i<>0 do.

begin.

s1 [i]: =')';

i:=pos (')', s1);

end;

i:=pos ('-', s1);

while i<>0 do.

begin.

s1 [i]: ='^';

i:=pos ('-', s1);

end;

end;

{**************************************************************}.

{Процедура применения закона Де Моргана}.

Procedure DeMorgan (var s1: string);

var i, j, k: byte;

begin.

i:=pos ('^', s1); delete (s1, i, 2);

k:=pos (')', s1); delete (s1, k, 1);

while true do.

begin.

if s1 [i]='^' then.

begin.

delete (s1, i, 1);

inc (i);

dec (k).

end.

else.

begin.

insert ('-', s1, i);

inc (i, 2);

inc (k).

end;

if i=k then break;

if s1 [i]='+' then s1 [i]: ='*'.

else s1 [i]: ='+';

inc (i);

end;

end;

{**************************************************************}.

{Процедура применения дистрибутивного закона}.

Procedure Disp;

var i, j, k: byte;

sp:string;

Function dis (s:string):string;

var x, l, i, j, p, n: byte;

s1, s2, sn: string[80];

begin.

i:=pos ('(', s); j:=pos (')', s); sn:='';

if (s [j+1]=c1) and (j<>length (s)) then.

begin.

x:=i;

s1:=copy (s, i+1, j-i-1);

l:=length (s); p:=l;

for n:=j+2 to l do.

if s[n]=c2 then.

begin.

l:=n;

break.

end;

if l=p then s2:=copy (s, j+1, l-j).

else s2:=copy (s, j+1, l-j-1);

if l=p then delete (s, i, l-i+1).

else delete (s, i, l-i);

repeat.

i:=pos (c2, s1);

if i=0 then.

begin.

i:=length (s1);

insert (copy (s1,1, i)+s2+', ', sn, 1);

delete (sn, length (sn), 1);

insert (sn, s, x);

delete (sn, 1,80);

break;

end;

insert (copy (s1,1, i-1)+s2+', ', sn, 1);

delete (s1,1, i).

until false;

end.

else.

begin.

s1:=copy (s, i+1, j-i-1);

l:=1;

for n:=i-2 downto 1 do.

if s[n]=c2 then.

begin.

l:=n;

break.

end;

if l=1 then.

begin.

s2:=copy (s, 1, i-l);

x:=1;

end.

else.

begin.

s2:=copy (s, l+1, i-l-1);

x:=l+1;

end;

if l=1 then delete (s, 1, j).

else delete (s, l+1, j-l);

repeat.

i:=pos (c2, s1);

if i=0 then.

begin.

i:=length (s1);

insert (s2+copy (s1,1, i)+', ', sn, 1);

delete (sn, length (sn), 1);

insert (sn, s, x);

delete (sn, 1,80);

break;

end;

insert (s2+copy (s1,1, i-1)+', ', sn, 1);

delete (s1,1, i);

until false;

end;

dis:=s;

end;

begin.

repeat.

i:=pos ('(', s1);

j:=pos ('^', s1);

k:=pos (')', s1);

if i=j+1 then.

if ((s1 [j-1]=c2) or (s1 [j-1]=', ') or (j=1)) and.

((s1 [k+1]=c2) or (s1 [k+1]=', ') or (k=length (s1))) then.

begin.

DeMorgan (s1);

continue;

end;

if (i<>j+1) and (j<>0) then.

begin.

s1 [j]: ='-';.

continue;.

end;.

if (i=j+1) then.

begin.

sp:=copy (s1, j, k-i+2);.

delete (s1, j, 1);.

delete (s1, i, k-i-1);.

DeMorgan (sp);.

insert (sp, s1, i);.

end;.

if i>0 then s1:=dis (s1);.

until pos ('(', s1)=0;.

end;.

begin.

if pos ('(', s1)>0 then Disp;.

zamena;.

end;.

{**************************************************************}.

{Процедура инверсии формулы (строки) s1}.

Procedure inversia;.

var i, j, k: byte;.

s:string;.

Procedure proverka;.

var s:^string;.

begin.

i:=pos ('(', s1); j:=pos (')', s1);.

while i<>0 do.

begin.

s^:=copy (s1, i+1, j-1-i);.

if (((i=1) or (s1 [i-1]='+')) and (s1 [i-1]<>'^')).

and ((s1 [j+1]='+') or (j=length (s1))).

then.

begin.

delete (s1, i, 1);.

delete (s1, j — 1,1).

end.

else.

if (pos ('+', s^)=0) and ((((i=1) or.

(s1 [i-1]='*')) and (s1 [i-1]<>'^')).

and ((s1 [j+1]='*') or (j=length (s1)))) then.

begin.

delete (s1, i, 1);.

delete (s1, j — 1,1).

end.

else.

begin.

s1 [j]: =')';.

s1 [i]: =' (';.

end;.

i:=pos ('(', s1); j:=pos (')', s1);.

end;.

end;.

begin.

i:=pos ('(', s1); j:=0;.

while i<>0 do.

begin.

if (i=1) or (s1 [i-1]<>'^') then.

begin.

insert ('^', s1, i);.

inc (i).

end.

else.

begin.

delete (s1, i — 1,1);.

dec (i).

end;.

k:=pos (')', s1);.

s1 [i]: =' ['; s1 [k]: =']';.

i:=pos ('(', s1);.

end;.

s:=s1;.

repeat.

i:=pos ('(', s);.

if (i=1) or (i=2) then.

begin.

k:=pos (')', s);.

j:=j+k+1;.

if j-1.

begin.

if s1 [j]='*' then s1 [j]: ='+'.

else s1 [j]: ='*'.

end;.

delete (s, 1, k+1);.

end.

else.

begin.

if s[1]='^' then.

begin.

delete (s1, j+1,1);.

delete (s, 1,3);.

inc (j, 2);.

if j.

begin.

if s1 [j]='+' then s1 [j]: ='*'.

else s1 [j]: ='+'.

end;.

end.

else.

begin.

insert ('^', s1, j+1);.

inc (j, 3);.

if j.

begin.

if s1 [j]='+' then s1 [j]: ='*'.

else s1 [j]: ='+'.

end;.

delete (s, 1,2);.

end.

end.

until length (s)=0;.

proverka;.

end;.

{**************************************************************}.

{Процедура исключения импликации путём замены на эквивалентную формулу в строке s1}.

Procedure implik;.

var i, j, k: byte;.

begin.

while pos ('>', s1)<>0 do.

begin.

i:=pos ('>', s1);.

if s1 [i-1]=')' then.

begin.

j:=pos (')', s1);.

while j<>i-1 do.

begin.

k:=pos ('(', s1);.

s1 [j]: =']'; s1 [k]: =' [';.

j:=pos (')', s1);.

end;.

k:=pos ('(', s1);.

insert ('^', s1, k);.

s1 [i+1]: ='+';.

end.

else.

begin.

insert ('^', s1, i-1);.

s1 [i+1]: ='+';.

end;.

end;.

end;.

{**************************************************************}.

{Процедура исключения двойного отрицания из строки s1}.

Procedure inverX2;.

var i: byte;.

begin.

while pos ('^', s1)<>0 do.

begin.

i:=pos ('^', s1);.

if s1 [i+1]='^' then delete (s1, i, 2).

else s1 [i]: ='-';.

end;.

while pos ('-', s1)>0 do.

begin.

i:=pos ('-', s1);.

s1 [i]: ='^';.

end;.

end;.

{**************************************************************}.

{Процедура исключения эквиваленции путём замены на эквивалентную формулу в строке s1}.

Procedure ekvivalentia;.

var i, j, k: byte;.

s2, s3: string[2];.

ss:string[20];.

begin.

repeat.

i:=pos ('<', s1);.

if (s1 [i-2]='^') and (i-1<>1) then.

begin.

s2:=copy (s1, i — 2,2);.

j:=i-2.

end.

else.

begin.

s2:=copy (s1, i — 1,1);.

j:=i-1.

end;.

if (s1 [i+2]='^') and (i+1<>length (s1)) then.

begin.

s3:=copy (s1, i+2,2);.

k:=i+4-j.

end.

else.

begin.

k:=i+3-j;.

s3:=copy (s1, i+2,1);.

end;.

delete (s1, j, k);.

ss:=' ('+'^'+s2+'+'+s3+')'+'*'+' ('+s2+'+'+'^'+s3+')';.

insert (ss, s1, j);.

until pos ('<>', s1)=0;.

end;.

begin.

clrscr;.

write (' Введите количество посылок:');.

readln (np);.

writeln;.

n:=0;.

for i:=1 to np do.

begin.

write ('введите', i, '-ю строку:');.

readln (s1);.

if pos ('<>', s1)<>0 then ekvivalentia;.

if pos ('>', s1)<>0 then implik;.

inverX2;.

Obrab ('+', '*');.

j:=pos ('*', s1);.

while j<>0 do.

begin.

s1 [j]: =', ';.

j:=pos ('*', s1);.

end;.

repeat.

n1:=1;.

inc (n);.

k:=pos (', ', s1);.

if k=0 then k:=length (s1)+1;.

ss:=copy (s1,1, k-1);.

delete (s1,1, k);.

repeat.

n2:=pos ('+', ss);.

if n2=0 then n2:=length (ss)+1;.

stp [n, n1]: =copy (ss, 1, n2−1);.

delete (ss, 1, n2); inc (n1);.

until length (ss)=0;.

sx[n]: =n1−1;.

until length (s1)=0;.

end;.

write ('введите теорему:'); readln (s1);.

if pos ('<>', s1)<>0 then ekvivalentia;.

if pos ('>', s1)<>0 then implik;.

Obrab ('+', '*');.

inverX2;.

inversia;.

inverX2;.

i:=pos ('*', s1);.

while i<>0 do.

begin.

s1 [i]: =', ';.

i:=pos ('*', s1);.

end;.

repeat.

n1:=1;.

inc (n);.

k:=pos (', ', s1);.

if k=0 then k:=length (s1)+1;.

ss:=copy (s1,1, k-1);.

delete (s1,1, k);.

repeat.

n2:=pos ('+', ss);.

if n2=0 then n2:=length (ss)+1;.

stp [n, n1]: =copy (ss, 1, n2−1);.

delete (ss, 1, n2);.

inc (n1);.

until length (ss)=0;.

sx[n]: =n1−1;.

until length (s1)=0;.

end;.

{**************************************************************}.

{Процедура применения метода пропозициональной резолюции к группе формул.

(массива)}.

Procedure MetRezolut (var a: mas);.

procedure cop (var sw: string; ss: string);.

begin.

sw:='';.

while length (ss)<>0 do.

begin.

if ss[1]='^' then.

begin.

sw:=sw+copy (ss, 1,2)+'+';.

delete (ss, 1,2).

end.

else.

begin.

sw:=sw+copy (ss, 1,1)+'+';.

delete (ss, 1,1).

end;.

end;.

delete (sw, length (sw), 1);.

end;.

var b: boolean;.

q, i, j, j1, h, k: byte;.

x:string[2];.

s:string;.

f:text;.

sj1, sj, si: set of byte;.

sw1, sw2, sw3: string;.

begin.

clrscr;.

assign (f, 'rez.txt');.

rewrite (f);.

writeln (f, ' введеные строки ');.

writeln (f, '***********************');.

for i:=1 to n do.

begin.

s:='';.

for j:=1 to sx[i] do s:=s+a [i, j]+'+';.

delete (s, length (s), 1);.

writeln (f, s, ' < - ', i, '-я строка ');.

end;.

writeln (f, '***********************');.

for q:=1 to n do.

begin.

s:='';.

si:=[];.

include (si, q);.

for j:=1 to sx[q] do s:=s+a [q, j];.

sw1:='';.

cop (sw1, s);.

writeln (f, sw1,' <- исходная строка ');.

repeat.

b:=false;.

for i:=1 to n do.

begin.

if not (i in si) then.

begin.

sj:=[];.

sw1:='';.

cop (sw1, s);.

for j:=1 to sx[i] do.

begin.

x:=a [i, j];.

h:=length (x);.

if h=2 then.

begin.

delete (x, 1,1);.

dec (h).

end.

else.

begin.

insert ('^', x, 1);.

inc (h).

end;.

k:=pos (x, s);.

if (k>0) and (s[k-1]='^') and (a[i, j]=copy (s, k — 1,2)) then.

begin.

k:=0;.

sj:=sj+[j];.

end.

else if k>0 then.

begin.

sj1:=sj1+[j];.

delete (s, k, h).

end;.

end;.

if sj1<>[] then.

begin.

for j:=1 to sx[i] do.

if (not (j in sj1)) and (not (j in sj)).

then s:=s+a [i, j];.

b:=true;.

include (si, i);.

sj1:=[];.

sw2:='';.

for j:=1 to sx[i] do sw2:=sw2+a [i, j];.

cop (sw2, sw2);.

if length (s)<>0 then cop (sw3, s).

else sw3:='__';.

writeln (f, sw3,' выведена из:', sw1,' и ', sw2);.

if length (s)=0 then.

begin.

writeln (f, ' получили противоречие, значит теорема доказана ');.

writeln (f, '***********************');.

close (f);.

exit;.

end;.

break;.

end;.

end;.

if b then break.

end;.

if (i=n) and (not (b)) then break;.

until false;.

writeln (f, ''Не возможно построить ни одного нового предложения ');.

end;.

writeln (f, ' теорема не доказана, т.к. не возможно получить противоречия ');.

writeln (f, '***********************');.

close (f);.

end;.

{**************************************************************}.

BEGIN.

for i:=1 to 50 do.

for j:=1 to 40 do stp [i, j]: ='0';.

Wwod;.

clrscr;.

MetRezolut (stp);.

writeln ('резульат смотрите в файле rez. txt');.

END..

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

Введите количество посылок: 4.

Ведите 1-ю посылку:

Ведите 2-ю посылку:

Ведите 3-ю посылку:

Ведите 4-ю посылку:

Введите теорему:

<<�Данная теорема истинна>>

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

2. Гаджиев А. А. Методические указания к выполнению лабораторного практикума по дисциплине «Математическая логика и теория алгоритмов» (для специальностей 22.01 — ВМКСиС и ПОВТиАС). Махачкала, 2003 г.