4.6. Использование Пролога для доказательства теорем

Для получения программы 4.1 вам необходимо загрузить модули Пролог-системы PROLOG, SIMPLE и TOLD. Функции AND, OR и NOT встроены в Пролог. С помощью этих функций и определяемых в программе отношений true, false и Т мы сможем определять истинность сложных высказываний, а также проверять на эквивалентность различные высказывания.

В программе 4.1 отношения b, g и h соответствуют одноименным функциям, приведенным на табл. 4.8. Они могут быть представлены как b = p∨q, g = (р∧q)∨(~p∧~q) и h = р∧q. Для того чтобы предоставить пользователю возможность вводить значение той или иной логической переменной, используется отношение is-told. Запрос может иметь следующую форму "р истинно?" ("р true?",) и, если на него будет получен ответ "да" (yes), то значением р становится истина (true). В случае же, если вводится ответ "нет" (по), значением р считается ложь (false).

X true if

[h T, если р истина И q истина]

Отношение Т, как уже было указано, используется для проверки истинности сложных высказываний. С помощью данного отношения определяется истинность заданного сложного высказывания в зависимости от значений входящих в него переменных, которые в ответ на вопросы системы вводятся пользователем. Диалог между Пролог-системой и пользователем может иметь, например, следующий вид:

is (h T) ; Запрос пользователя

&.

В рассмотренном примере диалога проверяется высказывание, составленное с помощью операции AND. Аналогичная проверка для других значений переменных будет выглядеть следующим образом:

is (h T)

&.

Обратите внимание на то, что, обработав третий ответ пользователя, Пролог-система ответила сразу же после получения значения р, не производя в данном случае ненужной проверки значения q. Приведем теперь пример определения истинности высказывания b:

is (b T)

&.

Функция OR принимает значение истина, когда это же значение имеет хотя бы одна из двух ее переменных. Поэтому Пролог-система, обнаружив, что значением первой переменной является истина, прекращает проверку. Ниже приведены примеры диалога при проверке высказывания g = ((р ∧ q)∨(~p∧~q)).

Случай 1

is (g T)

[ДА]

Случай 2

& is (g T)

[НЕТ]

Случай 3

& is (g T)

[НЕТ]

Случай 4

& is (g T)

&.

В рассмотренном примере представлены варианты получения ответа для всех четырех позиций таблицы истинности данной функции. В первом варианте р и q истинны, поэтому второй терм анализируемой функции на проверяется, так как функция OR, связывающая оба терма, в случае истинности первого терма также принимает значение истина.

Значением первого терма во втором варианте является ложь, поэтому Пролог-система переходит к проверке истинности второго терма. Поскольку мы не обеспечили запоминание ответа на первый вопрос об истинности р (р true ?), он повторяется еще раз, и мы должны еще раз утвердительно на "его ответить. Сразу после этого Пролог-система устанавливает, что значением g является ложь, так как независимо от значения q значение второго терма - ложь.

В третьем и четвертом вариантах, так же как и во втором, Пролог-система повторяет вопрос "р true ?", чтобы определить значение второго терма функции g. Как будет показано в дальнейшем, можно избежать повторений вопросов, но сейчас мы не будем останавливаться на этом.

С помощью только что разобранного примера было показано, как можно использовать Пролог для проверки правильности логических уравнений, описывающих логические функции b, g и h.

Можно воспользоваться средствами Пролога для проверки правильности альтернативных выражений для этих же функций. Для этого воспользуемся правилом алгебры логики, позволяющим манипулировать знаком отрицания: двойное отрицание переменной равно самой переменной: ~ (~А) = А. Пусть ~А = В, тогда, взяв отрицание от обеих частей этого равенства и применив к левой части правило двойного отрицания, получим А = ~В. Рассмотрим логическую функцию b = р∨q . Согласно правилам алгебры логики, выражение для этой функции может быть преобразовано к следующему виду: ~b = ~ (р∨q). Ранее уже было указано, что символьное выражение для функций можно искать с помощью отрицания функции, являющейся по отношению к исходной альтернативной, т. е. принимающей значение истина при тех значениях переменных, где исходная функция ложна, и наоборот. Функция OR принимает значение ложь только в том случае, когда р и q ложны одновременно, поэтому справедливо следующее равенство ~b = ~р∧~q. С помощью программы 4.1 проверим справедливость последнего равенства, а также сравним его с~b = ~ (р∨q). Если они окажутся идентичными, это будет доказательством того, что ~р∧~q тождественно равно ~ (р∨q).

Добавим к программе 4.1 следующий фрагмент:

b F if

[b F, если р ложь И q ложь]

Поскольку справедливо "X ложь, если НЕ X истина" (X false if not X true), приведенный выше фрагмент эквивалентен следующему:

b F if

[b F, если НЕ р истина И НЕ q истина]

что в символьной записи соответствует b = ~р∧~q. Проверим это равенство с помощью следующих вопросов:

is (b F)

&.

Теперь удалим из программы отношение F с помощью команды kill F и введем другое его определение:

b F if

[b F, если НЕ (р истина ИЛИ q истина)]

Ниже приведен диалог, служащий для проверки введенного отношения:

is (b F)

&.

О том, что данное отношение эквивалентно удаленному, свидетельствует совпадение последних двух диалогов.