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

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

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)

(VH) Начало

(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<i) 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<length(s1) then

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<length(s1) then

begin

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

else s1 [j]:='+'

end;

end

else

begin

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

inc (j, 3);

if j<length(s1) then

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

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