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