значительные упрощения. Так, например, в него заложено чрезвычайно простое и жесткое правило разрешения конфликтов: всегда запускать
?- пуск.
Назад | Содержание | Вперёд
Назад | Содержание | Вперёд
16. 3. Простая программа для автоматического докаэательства теорем
В настоящем разделе мы реализуем простую программу для
автоматического доказательства
теорем в виде системы, управляемой образцами. Эта программа будет основана на
- популярном методе, обычно используемом в машинном доказательстве теорем. Мы ограничимся случаем
, поскольку нашей целью будет дать всего лишь простую иллюстрацию используемого принципа. На самом деле, принцип резолюции можно легко обобщить на случай исчисления высказываний первого порядка (с применением логических формул, содержащих переменные). Базовый Пролог можно рассматривать как частный случай системы доказательства теорем, основанной на принципе резолюции.
Задачу доказательства теорем можно сформулировать так: дана формула, необходимо показать, что эта формула является теоремой, т. е. она верна всегда, независимо от интерпретации встречающихся в ней символов. Например, утверждение, записанное в виде формулы
и означающее '
Мы будем использовать в качестве операторов следующие символы:
~ отрицание, читается как 'не'
& конъюнкцию, читается как 'и'
v дизъюнкцию, читается как 'или'
=> импликацию, читается как 'следует'
Согласно правилам предпочтения операторов, оператор 'не' связывает утверждения сильнее, чем 'и', 'или' и 'следует'.
Метод резолюции предполагает, что мы рассматриваем отрицание исходной формулы и пытаемся показать, что полученная формула противоречива. Если это действительно так, то исходная формула представляет собой тавтологию. Таким образом, основную идею можно сформулировать так: доказательство противоречивости формулы с отрицанием эквивалентно доказательству того, что исходная формула (без отрицания) есть теорема (т. е. верна всегда). Процесс, приводящий к искомому противоречию, состоит из отдельных шагов, на каждом из которых применяется резолюция.
Давайте проиллюстрируем этот принцип на примере. Предположим, что мы хотим доказать, что теоремой является следующая пропозициональная
