Kosat, алгоритм проверки формулы по таблице истинности представляете? Когда сначала для каждой буквы устанавливается - истинна она или ложна, затем для выражений, образованных из этих букв, затем для выражений из выражений и так далее, пока до формулы не дойдём.
Например, та же

. Начинаем с четырёх стартовых позиций - четырёх строк таблицы истинности. Например, для случая

,

. Вычисляем

:

. Вычисляем

:

. Затем вычисляем

. Затем вычисляем

. Наконец вычисляем всё выражение

. А откуда мы знаем, что

,

и т. д.? А у нас должны быть забиты в программу таблички, в которых все возможные варианты записаны.
Доказательство производится также. Только вместо "рассчитать значение подвыражения

-

или

" для каждой подформулы

нужно написать доказательство - либо доказательство

, либо доказательство

. Например, для случая

,

. Доказываем

:

. Доказываем

:

. Затем доказываем

. Как? А у нас должны быть забиты в программу таблички, в которых все возможные варианты записаны. Только теперь это должны быть таблички функций. В предыдущем случае у нас для дизъюнкции была табличка из четырёх строк, так?
Вот такая:
Код:
x | y | x V y
0 | 0 | 0
0 | 1 | 1
1 | 0 | 1
1 | 1 | 1
И здесь у нас тоже должна быть такая же табличка их четырёх строк. Но теперь каждая строка - это не тройка чисел, а функция, которая принимает два аргумента. Первый аргумент - это ряд формул, доказательство

либо

- в зависимости от строки таблицы. Второй аргумент - опять же ряд формул, доказательство

или

- опять же в зависимости от строки. А возвращать эти функции должны соответственно доказательство

(для функций из нижних трёх строк) или

(для функции в верхней строке).
Таким образом, мы выбираем подходящую функцию и скармливаем ей доказательство

(а это, напоминаю, просто список из одной формулы - собственно

) и доказательство

(аналогично, список из одной этой формулы). И получаем на выходе доказательство

. Дальше таким же макаром получаем доказательство

. Наконец, берём табличку для импликации, берём фукцию из последней строки, скармливаем ей имеющиеся у нас на этом этапе доказательства

и

, и получаем назад искомое доказательство.
Видите - всё очень просто, надо только накодить эти таблички функций. Всего функций будет 14 штук - две для отрицания и по четыре для остальных операций.
Если эта идея понятна, можете начинать писать функцию для первой строки таблицы импликации. Я вам помогу.