Ну и наконец начинаем сравнивать две формулы на предмет наличия признаков эквивалентности.

//проверка на одинаковость наборов переменных
if peremennye<>postroenie(workstr2) then begin ShowMessage('Формулы не эквивалентны: разные наборы переменных!'); exit; end;
//проверка эквивалентности
k:=2;
for i:=2 to length(peremennye) do
k:=k*2;
for t:=0 to k-1 do begin
binstr:=int2bin(t,length(peremennye));
podstavim1:=workstr1;
for i:=1 to length(peremennye) do
for j:=1 to length(podstavim1) do
if podstavim1[j]=peremennye[i] then podstavim1[j]:=binstr[i];
podstavim2:=workstr2;
for i:=1 to length(peremennye) do
for j:=1 to length(podstavim2) do
if podstavim2[j]=peremennye[i] then podstavim2[j]:=binstr[i];
if istinnost(podstavim1)<>istinnost(podstavim2) then begin ShowMessage('Формулы не эквивалентны!'); exit; end;
end;
ShowMessage('Формулы эквивалентны!');
end;
end;

Ссылки на дальнейшие куски кода из MLIT'ы я не буду выводить в главное меню. Выведу их здесь.

• Вычисление СДНФ/СКНФ
• Проверка наличия переменных
• Цикл по формулам
• Не равна ли формула нулю?
• А может один?
• Заканчиваем вычисление СДНФ/СКНФ
• Закрашиваем stringgrid
• Добавление переменых
• Окончание MLITA