Программа реализации метода Резолюции

uses crt;{метод резолюции}

type str100=string[100]; mn_char = set of char;{описание типов}

const oper= ['*','+']; {множество логических операций}

var stek:array[1..50] of str100;{в нем хранятся доказываемые строки}

m, {длина доказываемой строки}

ik, {индекс последней строки в массиве}

it, {индекс текущей рассматриваемой строки}

io:byte; {индекс операции '+' или '*' в текущей строке}

sk1,sk2, {индексы начальной и конечной скобок}

k:byte; {параметр циклов}

vl:shortint;{проверка вложенности скобок}

procedure set_var;

var k:byte;

begin

{ writeln('введите число посылок: '); readln(k);}K:=4;

{ writeln('введите посылки:');}

{ for ik:=1 to k do readln(stek[ik]);{k:=3;}

stek[1]:='^A+^C+B';stek[2]:='^B+^E+^D';stek[3]:='F+E';stek[4]:='F+^D';}

writeln('введите отрицание теоремы:'); readln(stek[ik+1]);

end;

procedure reset_var;

var st:str100; i:byte;

procedure obrab(it:byte;z,nz:char);

type mn_dig = set of byte;

const mn_sk = ['(',')'];

var i:byte; st:str100; nsk:mn_dig; not_op:boolean;

procedure del_space_and_upcase(it:byte);

Var st:str100; I:byte;

begin

st:='';

for i:=1 to length(stek[it]) do

if stek[it,i]<>#32 then st:=st+upcase(stek[it,i]);

stek[it]:=st;

end; {del_space_&_upcase}

procedure find_implic(it:byte);

var i,ind:byte;

begin

for i:=length(stek[it])-1 downto 2 do

if stek[it,i]='-' then begin

sk1:=i-1; sk2:=i-1;

if stek[it,i-1]=')' then begin vl:=0;

for sk1:=sk2-1 downto 1 do

begin

if (stek[it,sk1]='(')and(vl=0) then break;

if stek[it,sk1]=')' then vl:=vl+1 else

if stek[it,sk1]='(' then vl:=vl-1;

end; end;

ind:=i;

if (stek[it,sk1-1]='^')and(sk1>1)

then begin dec(ind);delete(stek[it],sk1-1,1); end

else begin inc(ind);insert('^',stek[it],sk1); end;

delete(stek[it],ind,2); insert('+',stek[it],ind);

end;

end; {find_implic}

procedure de_morgan(sk1,sk2:byte);

var i:byte;

begin{de_morgan}

delete(stek[it],sk1-1,1); vl:=0;

for i:=sk1 to sk2-1 do

begin

if stek[it,i]='(' then inc(vl)

else if stek[it,i]=')' then dec(vl);

if (stek[it,i]=z)and(vl=0)

then begin delete(stek[it],i,1); insert(nz,stek[it],i); break;end

else if (stek[it,i]=nz)and(vl=0)

then begin delete(stek[it],i,1);insert(z,stek[it],i);break;end;

end;

if stek[it,i+1]='^' then delete(stek[it],i+1,1)

else insert('^',stek[it],i+1);

if stek[it,sk1]='^' then delete(stek[it],sk1,1)

else insert('^',stek[it],sk1);

nsk:=[];

end; {de_morgan}

procedure distrib(sk1,sk2,num:byte);

var i:byte; found:boolean; st1,st2,st3:str100;

procedure set_k;

begin{set_k} vl:=0;

for k:=sk1+1 to sk2-1 do begin

if stek[it,k]='(' then inc(vl)

else if stek[it,k]=')' then dec(vl);

if (stek[it,k]=z)and(vl=0) then break;

end;

end; {set_k}

procedure set_i(var i:byte;pc1,pc2:byte;pc3:shortint);

begin{set_i}

i:=pc1-pc3; vl:=0;

repeat

i:=i+pc3;

if stek[it,i]='(' then inc(vl)

else if stek[it,i]=')' then dec(vl);

if ((stek[it,i] in oper)and found)and(vl=0) then break

else if (stek[it,i] in oper)and(vl=0) then found:=true;

until i=pc2;

if vl<>0 then i:=i+vl;

end; {set_i}

procedure distrib1(sk1,sk2:byte);