Рассмотрим один пример применения правила резолюций при наличии переменных:
человек(f1(Х)); король(Х):-. (1)
король(Y):- почитает(f1(Y),Y). (2)
почитает(Z,артур):- человек(Y). (3)
Два первых дизъюнкта представляют стандартную форму формулы, которую можно выразить так: «если каждый человек почитает кого-то, то этот кто-то – король». Переменные переименованы для удобства объяснения. Третий дизъюнкт выражает высказывание о том, что каждый человек почитает Артура. Применяя правило резолюций к (2) и (3) (сопоставляя два соответствующих литерала), получаем:
король(артур):- человек(f1(артур)). (4)
(Y в (2) сопоставлен с артур в (3), a Z в (3) сопоставлен с fl(Y) в (2)). Теперь можно применить правило резолюций к (1) и (4), что дает:
король(артур); король(артур):-.
Это эквивалентно факту, гласящему, что Артур является королем.
В формальном определении метода резолюций процедура «сопоставления», на которую мы неформально ссылались, называется унификацией. Интуитивно, множество атомарных формул унифицируемо, если эти формулы могут быть сопоставлены друг с другом как структуры языка Пролог. В действительности, как это будет показано в одном из следующих разделов, процедура сопоставления, используемая в большинстве реализаций языка Пролог, не совпадает в точности с унификацией.
Как можно использовать метод резолюций для доказательства конкретных утверждений? Один из возможных способов состоит в том, чтобы последовательно, шаг за шагом, применять правило резолюций к имеющимся гипотезам и посмотреть, не появилось ли при этом то, что мы хотим доказать. К сожалению, нельзя гарантировать, что это в конце концов произойдет, даже если интересующее нас высказывание действительно следует из имеющихся гипотез. Так, например, в последнем примере нельзя вывести простой дизъюнкт король(артур), исходя из данного множества дизъюнктов и используя лишь указанный метод, несмотря даже на то, что это очевидное следствие. Следует ли отсюда, что метод резолюций не является достаточно мощным средством для наших целей? К счастью, ответом на этот вопрос является «нет», так как можно переформулировать постановку задачи таким образом, что метод резолюций гарантированно сможет решить ее, если это в принципе возможно.
Метод резолюций имеет одно важное формальное свойство – он является полным для доказательства несовместности множества дизъюнктов. Это значит, что если множество дизъюнктов несовместно, то используя метод резолюций всегда можно вывести из данного множества дизъюнктов пустой дизъюнкт:
:-.
Кроме того, так как метод резолюций является корректным, то единственное, что он может вывести в такой ситуации – это пустой дизъюнкт. Множество формул несовместно, если не существует интерпретации предикатов, констант и функциональных символов, делающей истинными одновременно все эти формулы. Пустой дизъюнкт является логическим выражением ложности - он представляет высказывание, которое ни при каких условиях не может быть истинным. Таким образом, метод резолюций наверняка определит, когда заданное множество формул является несовместным, выведя пустой дизъюнкт, являющийся выражением противоречия.
Каким образом это свойство метода резолюций может помочь нам? Имеет место следующий факт:
Если множество формул {А1, A2,…, Аn} совместно, то формула В является следствием формул {Al, A2,…, An} тогда и только тогда, когда множество формул {А1, A2,…, Аn ⌉В} - несовместно.
Таким образом, если множество гипотез совместно, то необходимо лишь добавить к нему дизъюнкты, соответствующие отрицанию высказывания, которое следует доказать. Резолюция даст пустой дизъюнкт в точности тогда, когда доказываемое высказывание следует из данных гипотез. Дизъюнкты, добавляемые к множеству гипотез, называются целевыми дизъюнктами. Отметим, что целевые дизъюнкты ничем не отличаются от гипотез – и те и другие являются дизъюнктами. Так что, если задано множество дизъюнктов {А1, А2, …, Ап} и требуется проверить несовместность этого множества дизъюнктов, то в действительности невозможно определить, идет ли речь о доказательстве того, что ⌉А1 следует из A2, А3, …, Ап или что ⌉А2 следует из A1, A3, …, Аn, или что ⌉А3 следует из А1, А2, A4,…, Аn и так далее. Именно это является причиной того, что необходимо указывать какие дизъюнкты в действительности являются целевыми дизъюнктами. Для системы, использующей метод резолюций, все перечисленные задачи эквивалентны.
Легко увидеть, как можно получить пустой дизъюнкт в примере с королем Артуром, если добавить целевой дизъюнкт:
:- король(артур). (5)
(это дизъюнкт для ~король(артур)). Ранее уже было показано, как дизъюнкт
король(артур); король(артур):-. (6)
может быть выведен из гипотез. Применяя правило резолюций к (5) и (6) (сопоставляя любую из атомарных формул в (5)), получаем:
король(артур):-. (7)
И наконец, резолюция дизъюнктов (6) и (7) дает
:-.
Таким образом, использование метода резолюций позволило доказать следствие, что Артур является королем.
Полнота метода резолюций является полезным математическим свойством. Это свойство означает, что, если некоторый факт следует из гипотез, то имеется возможность доказать его истинность (показав несовместность множества дизъюнктов, содержащего гипотезы и отрицание доказываемого факта)» используя для этого метод резолюций. Однако, когда мы говорим, что методом резолюций можно вывести пустой дизъюнкт, это значит, что существует последовательность шагов, на каждом из которых правило резолюций применяется к аксиомам или к дизъюнктам выведенным на предыдущих шагах, и эта последовательность заканчивается выводом дизъюнкта, не содержащего литералов. Единственная проблема – найти соответствующую последовательность шагов. Так как, хотя метод резолюций и говорит о том, как получить следствие двух дизъюнктов, он не сообщает, какие дизъюнкты выбрать для очередного шага и какие литералы в этих дизъюнкциях необходимо «сопоставить». Обычно, если имеется большое количество гипотез, то существует и много вариантов выбора среди них. Более того, на каждом шаге выводится новый дизъюнкт и он тоже становится кандидатом на участие в последующей обработке. Большинство из имеющихся возможностей выбора дизъюнктов и литералов в них не имеют отношения к решаемой задаче и, если не производить тщательного отбора среди кандидатов, то можно потратить слишком много времени на бесплодные поиски, а путь, ведущий к решению, так и не найти.
На решение этих вопросов направлено много различных улучшений исходного принципа резолюций. В следующем разделе рассматриваются некоторые из них.
10.5. Хорновские дизъюнкты
Рассмотрим теперь модификацию метода резолюций, разработанную для случая, когда все дизъюнкты имеют некоторый определенный вид – когда они являются хорновскими дизъюнктами, Хорновский дизъюнкт – это дизъюнкт, содержащий не более одного литерала без отрицания. Оказывается, что если процедура доказательства теорем используется для определения значений вычислимых функций, то вполне достаточно использовать для этого лишь хорновские дизъюнкты. Так как метод резолюций в случае хорновских дизъюнктов также является относительно простым, то естественно выбрать хорновские дизъюнкты в качестве основы для процедуры доказательства теорем, применяемой в практической системе программирования, Рассмотрим коротко, что представляет метод резолюций, если ограничиться хорновскими дизъюнктами.
Прежде всего, очевидно, что существуют два вида хорнов-ских дизъюнктов – дизъюнкты, содержащие один литерал без отрицания и дизъюнкты, не содержащие таких литералов. Будем называть эти два типа хорновских дизъюнктов соответственно дизъюнктами с заголовком и дизъюнктами без заголовка. Следующие примеры иллюстрируют указанные типы дизъюнктов (необходимо помнить, что литералы без отрицания записываются слева от знака ':-'):