Реферат Аналітичне та формальний доказ теореми в ІВ

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