У Клоксин - ПРОГРАММИРОВАНИЕ НА ЯЗЫКЕ ПРОЛОГ

Если множество формул { А 1, A 2,…, А n } совместно, то формула Вявляется следствием формул { A l ,A 2,…, A n } тогда и только тогда, когда множество формул { А 1, A 2,…, А n ⌉ В } - несовместно.

Таким образом, если множество гипотез совместно, то необходимо лишь добавить к нему дизъюнкты, соответствующие отрицанию высказывания, которое следует доказать. Резолюция даст пустой дизъюнкт в точности тогда, когда доказываемое высказывание следует из данных гипотез. Дизъюнкты, добавляемые к множеству гипотез, называются целевыми дизъюнктами. Отметим, что целевые дизъюнкты ничем не отличаются от гипотез – и те и другие являются дизъюнктами. Так что, если задано множество дизъюнктов { А 1, А 2, …, А п } и требуется проверить несовместность этого множества дизъюнктов, то в действительности невозможно определить, идет ли речь о доказательстве того, что ⌉ А 1 следует из A 2, А 3, …, А п или что ⌉ А 2следует из A 1, A 3, … , А n, или что ⌉ А 3 следует из А 1, А 2, A 4,…, А nи так далее. Именно это является причиной того, что необходимо указывать какие дизъюнкты в действительности являются целевыми дизъюнктами. Для системы, использующей метод резолюций, все перечисленные задачи эквивалентны.

Легко увидеть, как можно получить пустой дизъюнкт в примере с королем Артуром, если добавить целевой дизъюнкт:

:- король(артур). (5)

(это дизъюнкт для ~король(артур)). Ранее уже было показано, как дизъюнкт

король(артур); король(артур):-. (6)

может быть выведен из гипотез. Применяя правило резолюций к (5) и (6) (сопоставляя любую из атомарных формул в (5)), получаем:

король(артур):-. (7)

И наконец, резолюция дизъюнктов (6) и (7) дает

:-.

Таким образом, использование метода резолюций позволило доказать следствие, что Артур является королем.

Полнота метода резолюций является полезным математическим свойством. Это свойство означает, что, если некоторый факт следует из гипотез, то имеется возможность доказать его истинность (показав несовместность множества дизъюнктов, содержащего гипотезы и отрицание доказываемого факта)» используя для этого метод резолюций. Однако, когда мы говорим, что методом резолюций можно вывести пустой дизъюнкт, это значит, что существует последовательность шагов, на каждом из которых правило резолюций применяется к аксиомам или к дизъюнктам выведенным на предыдущих шагах, и эта последовательность заканчивается выводом дизъюнкта, не содержащего литералов. Единственная проблема – найти соответствующую последовательность шагов. Так как, хотя метод резолюций и говорит о том, как получить следствие двух дизъюнктов, он не сообщает, какие дизъюнкты выбрать для очередного шага и какие литералы в этих дизъюнкциях необходимо «сопоставить». Обычно, если имеется большое количество гипотез, то существует и много вариантов выбора среди них. Более того, на каждом шаге выводится новый дизъюнкт и он тоже становится кандидатом на участие в последующей обработке. Большинство из имеющихся возможностей выбора дизъюнктов и литералов в них не имеют отношения к решаемой задаче и, если не производить тщательного отбора среди кандидатов, то можно потратить слишком много времени на бесплодные поиски, а путь, ведущий к решению, так и не найти.

На решение этих вопросов направлено много различных улучшений исходного принципа резолюций. В следующем разделе рассматриваются некоторые из них.

10.5. Хорновские дизъюнкты

Рассмотрим теперь модификацию метода резолюций, разработанную для случая, когда все дизъюнкты имеют некоторый определенный вид – когда они являются хорновскими дизъюнктами, Хорновский дизъюнкт – это дизъюнкт, содержащий не более одного литерала без отрицания. Оказывается, что если процедура доказательства теорем используется для определения значений вычислимых функций, то вполне достаточно использовать для этого лишь хорновские дизъюнкты. Так как метод резолюций в случае хорновских дизъюнктов также является относительно простым, то естественно выбрать хорновские дизъюнкты в качестве основы для процедуры доказательства теорем, применяемой в практической системе программирования, Рассмотрим коротко, что представляет метод резолюций, если ограничиться хорновскими дизъюнктами.

Прежде всего, очевидно, что существуют два вида хорнов-ских дизъюнктов – дизъюнкты, содержащие один литерал без отрицания и дизъюнкты, не содержащие таких литералов. Будем называть эти два типа хорновских дизъюнктов соответственно дизъюнктами с заголовком и дизъюнктами без заголовка. Следующие примеры иллюстрируют указанные типы дизъюнктов (необходимо помнить, что литералы без отрицания записываются слева от знака ':-'):