Аналитическое и формальное доказательство теоремы в ИВ
Курсовой проект - Компьютеры, программирование
Другие курсовые по предмету Компьютеры, программирование
/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, *******