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

Форма записи дизъюнктов

Очевидно, что для записи формул, представленных в стандартной форме, необходим соответствующий способ. Рассмотрим его. Прежде всего, стандартная форма представляет совокупность дизъюнктов. Договоримся записывать дизъюнкты последовательно один за другим, помня при этом, что порядок записи не имеет значения. В свою очередь, дизъюнкт является совокупностью литералов, часть из которых содержит отрицание, а часть не содержат его. Примем соглашение записывать сначала литералы без отрицания, а затем литералы с отрицанием. Эти две группы литералов будем разделять знаком ':-'. Литералы без отрицания при записи будем отделять друг от друга точкой с запятой (;) (помня, конечно, при этом, что порядок записи литералов в каждой группе неважен), а литералы с отрицанием будем записывать без знака отрицания (~), разделяя литералы запятыми. Запись каждого дизъюнкта будет заканчиваться точкой. При такой форме записи дизъюнкт, содержащий отрицания литералов K, L,… и литералы А, В,… мог бы быть представлен так:

A; B;…:- K, L,…

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

(А # В #…) # (~К # -L #…)

что эквивалентно

(A # B # …) # ~(K & L & …)

Это в свою очередь эквивалентно (К & L &…) -› (А # В #…)

Если записать ',' вместо 'и', ';' вместо 'или' и ':-' вместо 'является следствием', то дизъюнкт естественным образом примет следующий вид:

A; B;…:- K, L,…

С учетом этих соглашений формула

(человек(адам) & человек(ева)) &((человек(Х) # ~мать(Х,Y)) # ~человек(Y))

записывается так:

человек(адам):-.

человек(ева):-.

человек(Х):- мать(Х,Y), человек(Y).

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

выходной(Х); работает(крис,X):-.

выходной(Х); сердитый(крис); унылый(крис):-.

Сразу не так очевидно, чему это может соответствовать в Прологе. Этот вопрос будет подробнее рассмотрен в следующем разделе.

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

человек(f1(X)); король(Х):-.

король(Х):- почитает(f1(Х),Х).

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

В 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₂,…, A_n } тогда и только тогда, когда множество формул { А₁, A₂,…, А_n ⌉ В } - несовместно.

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

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

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

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

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

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

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

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

:-.

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

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

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

Дата добавления: 2014-12-08