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

Курсовой проект - Компьютеры, программирование

Другие курсовые по предмету Компьютеры, программирование

/p>

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;

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 (i0) 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;

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

zamena;;

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

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

Procedure inversia;

var i, j, k:byte;

s:string;

Procedure proverka;s:^string;:=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;;:=pos ((, s1); j:=0;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;:=pos(), s1);

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

i:=pos ((, s1);

end;:=s1;

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

endlength(s)=0;

proverka;;

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

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

Procedure implik;i, j, k:byte;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;;

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

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

Procedure inverX2;i:byte;pos (^, s1)<>0 do

begin

i:=pos (^, s1);

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

else s1 [i]:=-;

end;pos (-, s1)>0 do

begin

i:=pos (-, s1);

s1 [i]:=^;

end;;

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

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

Procedure ekvivalentia;i, j, k:byte;

s2, s3:string[2];

ss:string[20];

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);pos (<>, s1)=0;

end;

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

readln(np);;:=0;i:=1 to np do

begin

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

readln(s1);

if pos (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 (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, *******