program Logic;
{
Разработчик: lamed. RFPRO, 2010
ABC Pascal
Идея использования префиксной нотации для логических выражений описана в [2], с.27, упр.3
В программе используется постфиксная нотация (обратная польская запись)
Подробное описание построения калькулятора арифметических выражений
можно получить в главе 4, п.4.1,4.2,4.3,4.4 [1].
и в решение задач 4.6, 4.10, [3]
Использованные источники.
1. Керниган, Брайан У., Ритчи, Деннис М. Язык программирования C. 2-е издание.:
   Пер. с англ. - М.: Издательский дом "Вильямс", 2006.
2. Мендельсон Э. Введение в математическую логику.
   Пер. с англ./Под ред. С. И. Адяна - 3-е изд. - М.:Наука, 1984
3. Тондо К., Гимпел С. Книга ответов: Пер. с англ. - М. Финансы и статистика, 1994
Вместо булевых значений ИСТИНА и ЛОЖЬ обрабатывются 1 и 0 соответсвенно.

В настоящей версии добавлены:
- обработка импликации
- печать эквивалентной СДНФ
}
const
  MAXVAL=100;
  TotalRows    = 1024; // программа рассчитана на 10 переменных
type
  TBit = 0..1;

var
  MaxLetter: integer;
  MaxRow   : integer;
  letters  : array[char] of integer;
  cond     : array[1..TotalRows, 1..26] of TBit; // таблица условий

var
  vals    : array[1..MAXVAL] of TBit;
  sp      : integer;
  ctype   : char;
  variable: array['a'..'z'] of TBit;

function bit(x: word; n: integer): TBit;
// получение n-го бита числа
begin
  bit := (x shr n ) and 1;
end;

procedure CreateTable(s: string);
// создание таблицы переменных
// и таблицы значений переменных
var
  len : integer;
  used: set of char;
  i,j : integer;
  num : word;
  c   : char;
begin
  len := length(s);
  used := [];

  for c:= 'a' to 'z' do
    letters[c] := 0;

  // Не все 26 букв используются в качестве переменных
  // Множество использованных букв
  for i:= 1 to len do
    if (s[i] in ['a'..'z']) then
      used := used+[s[i]];

  // Использованные буквы должны быть лексикографически упорядочены
  // при печати, нумеруем каждую использованную букву, начиная с 1
  MaxLetter:= 0;
  for c:= 'a' to 'z' do
    if (c in used) then
      begin
        inc(MaxLetter);
        letters[c] := MaxLetter;
      end;

  MaxRow := 1 shl MaxLetter;
  num:= 0;
  for j:= 1 to MaxRow do
    begin
      for i:= 1 to MaxLetter do
        cond[j, i]:= 1-bit(num, i-1);
      inc(num);
    end;
end;


procedure push(f: TBit);
// "вталкивание" элемента в стек
begin
  if (sp<=MAXVAL) then
    begin
      vals[sp]:=f;
      sp := sp+1;
    end
  else
    writeln('error stack full');
end; { push }

function pop: TBit;
// "выталкивание" элемента из стека
begin
  if (sp>1) then
    begin
      dec(sp);
      pop := vals[sp];
    end
  else
    begin
      writeln('error stack empty');
      pop := 0;
    end;
end; { pop }

function getop(var s: string): char;
// получение кода операции
var
  i: integer;
begin
  i:= 1;
  while (s[i]=' ') do
    inc(i);
  getop := s[i];
  delete(s,1,i);
end; { getop }

procedure CalcBool(s: string; var b: TBit; var code: integer);
// логический калькулятор
// построен на основе стека
begin
	s:= trim(s);
	if (s<>'') then
    begin
      repeat
     	  ctype := getop(s);
        case ctype of
          '0','1':		// значение И/Л
            push(ord(ctype)-ord('0'));
          '+':			// бинарная операция v дизъюнкция
            push(pop() or pop());
          '*':			// бинарная операция & конъюнкция
            push(pop() and pop());
          '>':			// бинарная операция => следование
            push(pop() or (1-pop()));
          '~':			// бинарная операция отрицание
            push(1-pop());
          else
            begin
              if ctype in ['a'..'z'] then
                push(variable[ctype])	// имя переменной
              else
                begin
                  writeln('error: unknown command ', s);
                  code:=1;
                  halt;
                end;
            end;
        end;
      until s='';
      b:= pop();						// последнее значение в стеке
      code := 0;						// результат выражения
    end
  else
    code:= -1;
end; { process }

var
  s    : string;
  i, j : integer;
  c    : char;
  code : integer;
  F    : TBit;
begin
  write('Ваша строка ');
  readln(s);
  
  // на первом проходе создаем таблицу имен аргументов
  // и заполняем таблицу значений 
  CreateTable(s);

  sp := 1;	// инициализация стека
			// указатель на вершину стека
  
  // в цикле по строкам и по столбцам
  // вычисляем значение выражения
  for j:= 1 to MaxRow do
    for c:= 'a' to 'z' do
	// удобней создать и использовать массив, содержащий имена и значения
	// всех букв, для данной задачи выделение памяти некритично
	// выигрываем в простоте кода
      begin
        if letters[c]>0 then
          variable[c]:= cond[j,letters[c]];
        CalcBool(s, F, code);
        cond[j, MaxLetter+1]:=F;
      end;

// Печать результата
  write(' ':3);
  for c:= 'a' to 'z' do
    if letters[c]>0 then
      write(c:3);
  writeln('F=':4, s);

  for j:= 1 to MaxRow do
    begin
      write(j: 3);
      for i:= 1 to MaxLetter+1 do
        write(cond[j,i]: 3);
      writeln;
    end;

  // Печать эквивалентной СДНФ
  //
  writeln('Эквивалентная СДНФ');
  for j:= 1 to MaxRow do
    if cond[j, MaxLetter+1]=1 then
      begin
        for i:= 1 to MaxLetter do
          begin
            if (cond[j,i]=0) then write('(~');
            for c:= 'a' to 'z' do
              if letters[c]=i then
                write(chr(ord(c)-ord('a')+ord('A')));
            if (cond[j,i]=0) then write(')');
            if i< MaxLetter then write('&');
          end;
        if j < MaxRow then
          write(' + ');
      end;
  writeln;

end.

Ваша строка c c ~ +
     c  F=c c ~ +
  1  1  1
  2  0  1
Ваша строка a b * a b ~ * +
     a  b  F=a b * a b ~ * +
  1  1  1  1
  2  0  1  0
  3  1  0  1
  4  0  0  0

Пример 1
(a->(b->c))->((a->b)>(a->c))
ПОЛИЗ. a b c > > a b > a c > > >
Диалог
Ваша строка 
     a  b  c  F=a b c > > a b > a c > > >
  1  1  1  1  1
  2  0  1  1  1
  3  1  0  1  1
  4  0  0  1  1
  5  1  1  0  1
  6  0  1  0  1
  7  1  0  0  1
  8  0  0  0  1
Эквивалентная СДНФ
A&B&C + (~A)&B&C + A&(~B)&C + (~A)&(~B)&C + A&B&(~C) + (~A)&B&(~C) + A&(~B)&(~C) + (~A)&(~B)&(~C)

Пример 2. Вопрос 180429
Автор вопроса: sveta11115 (Посетитель)
Автор ответа : Лысков Игорь Витальевич
(x'-> y')->(y& z)->(x & z)
ПОЛИЗ. x ~ y ~ > y z * > x z * >

Диалог
Ваша строка
     x  y  z  F=x ~ y ~ > y z * > x z * >
  1  1  1  1  1
  2  0  1  1  0
  3  1  0  1  1
  4  0  0  1  1
  5  1  1  0  1
  6  0  1  0  0
  7  1  0  0  1
  8  0  0  0  1
Эквивалентная СДНФ
X&Y&Z + X&(~Y)&Z + (~X)&(~Y)&Z + X&Y&(~Z) + X&(~Y)&(~Z) + (~X)&(~Y)&(~Z)