Книга: ПРОГРАММИРОВАНИЕ НА ЯЗЫКЕ ПРОЛОГ

10.4. Принцип резолюций и доказательство теорем

10.4. Принцип резолюций и доказательство теорем

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

В 60-х годах в этой области наблюдалась большая активность, связанная с возможностью использования вычислительных машин для автоматического доказательства теорем. Именно эта область научной деятельности, по-прежнему остающаяся источником новых идей и методов, дала жизнь идеям, легшим в основу Пролога. Одним из фундаментальных достижений того времени явилось открытие Дж. А. Робинсоном принципа резолюций и его применение к автоматическому доказательству теорем. Резолюция – это правило вывода, говорящее о том, как одно высказывание может быть получено из других. Используя принцип резолюций, можно полностью автоматически доказывать теоремы, выводя их из аксиом. Необходимо лишь решать, к каким из высказываний следует применять правило вывода, а правильные следствия из них будут строиться автоматически.

Правило резолюций разрабатывалось применительно к формулам, представленным в стандартной форме. Если заданы два дизъюнкта, связанных между собой определенным образом, то это правило породит новый дизъюнкт, являющийся следствием двух первых. Главная идея состоит в том, что, если одна и та же атомарная формула появляется как в левой части одного дизъюнкта, так и в правой части другого дизъюнкта, то дизъюнкт, получаемый в результате соединения этих двух дизъюнктов, из которых вычеркнута упоминавшаяся повторяющаяся формула, является следствием указанных дизъюнктов. Например,

Из

унылый(крист); сердитый(крис):- рабочий_день(сегодня), идет_дождь(сегодня).

и

неприятный(крис):- сердитый(крис), усталый(крис).

следует

унылый(крис); неприятный(крис):- рабочий_день(сегодня), идет_дождь(сегодня), усталый(крис).

На естественном языке это звучит так. Если сегодня рабочий день и идет дождь, то Крис – унылый или сердитый. Кроме того, если Крис сердитый и усталый, то он неприятен. Поэтому, если сегодня рабочий день, идет дождь и Крис усталый, то Крис является унылым или неприятным.

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

Рассмотрим один пример применения правила резолюций при наличии переменных:

человек(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), что дает:

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

Это эквивалентно факту, гласящему, что Артур является королем.

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

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

Метод резолюций имеет одно важное формальное свойство – он является полным для доказательства несовместности множества дизъюнктов. Это значит, что если множество дизъюнктов несовместно, то используя метод резолюций всегда можно вывести из данного множества дизъюнктов пустой дизъюнкт:

:-.

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

Каким образом это свойство метода резолюций может помочь нам? Имеет место следующий факт:

Если множество формул {А₁, A₂,…, Аn} совместно, то формула В является следствием формул {A_l, A₂,…, An} тогда и только тогда, когда множество формул {А₁, A₂,…, Аn?В} - несовместно.

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

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

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

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

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

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

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

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

:-.

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

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

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

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

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

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

холостяк(Х):- мужчина(Х), неженат(Х).

:- холостяк(Х).

В действительности, рассматривая множества хорновских дизъюнктов (включая целевые утверждения), необходимо выделять лишь такие множества, в которых все дизъюнкты за исключением одного имеют заголовки. Это значит, что каждая разрешимая задача (задача доказательства теоремы), которая может быть выражена с помощью хорновских дизъюнктов, может быть представлена в таком виде, что:

• Имеется только один дизъюнкт без заголовка. Все остальные дизъюнкты имеют заголовки.

Так как совершенно не имеет значения, какие дизъюнкты считать целевыми, то можно принять решение рассматривать дизъюнкт без заголовка как целевой, а все остальные дизъюнкты – как гипотезы. Такое решение выглядит довольно естественно.

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

Оглавление книги