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

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

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

Курсовой проект

Компьютеры, программирование

Другие курсовые по предмету

Компьютеры, программирование

Сдать работу со 100% гаранией
;+s3+')';

insert (ss, s1, j);pos ('<>', s1)=0;

end;

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

readln(np);;:=0;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;;

{**************************************************************}

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

(массива)}

Procedure MetRezolut (var a:mas);cop (var sw:string; ss:string);:='';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;(sw, length(sw), 1);;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;;(f, 'rez.txt');(f); (f, ' введеные строки ');

writeln (f, '***********************');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;(f, '***********************');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);;

{**************************************************************}i:=1 to 50 doj:=1 to 40 do stp [i, j]:='0';;;(stp);('резульат смотрите в файле rez.txt');.

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

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

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

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

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

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

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

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

 

 

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

 

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

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

 

Похожие работы

<< < 1 2 3