Cтраница 3
Оно позволяет нам соединить две формулы, удалив из одной атом А, а из другой А. Из приведенной выше таблицы видно, что правило резолюции можно рассматривать как аналог цепного правила в применении к формулам, находящимся в конъюнктивной нормальной форме. [31]
Если мы имеем два единичных дизъюнкта, то их резольвента, если она существует, есть пустой дизъюнкт Q. Более существенно, что для невыполнимого множества дизъюнктов применениями правила резолюций можно породить П - Этот результат будет доказан в § 5.6 этой главы. [32]
Пролог отличается от резолюции в разных аспектах. Некоторые предикаты обеспечивают успех непосредственно путем исполнения, без применения правила резолюции. [33]
Обратимся теперь к методу ( резолюций [4], который является локальным методом установления выводимо-епи в исчислении предикатов. В основу метода резолюций положено всего лишь одно правило вывода - правило резолюции. Оно по двум посылкам, R и R %, строит заключение JR. В качеств-е вспомогательных используются различные одно - - и двухпосылочные правила, от-ветствежные за так называемую унификацию и факторизацию литер. [34]
Следует иметь в виду, что устранение сечений облегчает поиск вывода, но может привести к резкому удлинению искомого вывода. Так для исчисления высказываний в работеЦейтин а [1] доказана возможность экспоненциального сокращения выводов при добавлении к правилу резолюций аналога правила сечения. [35]
Для уточнения сказанного заметим, что для любого исчисления 9 любой метод поиска вывода в нем может быть представлен как способ построения по каждому испытуемому на выводимость объекту S специального исчисления И. Такое представление особенно естественно для современных методов поиска вывода типа метода резолюций: аксиомами соответствующего исчисления HC S являются дизъюнкты из S, а единственным правилом - правило резолюции. [36]
В предшествующем обсуждении единственной мерой качества дизъюнкта было число содержащихся в нем литер. Определим h ( C, В) для пары ( С, В) из списка CLIST, построенного по модифицированному методу поиска в глубину, как число применений правила резолюции в минимальном доказательстве ( опровержении) с верхним упорядоченным дизъюнктом С и первым боковым дизъюнктом В. Если h ( C, В) известно, то мы можем использовать h ( C, В) для упорядочения пар в CLIST. Однако в общем случае / i ( C, В) неизвестно. Обычно h ( C, В) получается из множества известных данных. [37]
Дизъюнкты 0 и D2 называют родителями дизъюнкта D. В дизъюнкте D отсутствует пара: - A ( 0t) v A, ( 0S), при этом ( 0t) - ( 0s) и пара является тавтологией ( тождественно-истинной) и может быть удалена из дальнейших вычислений, что и выполняет правило резолюции. [38]
Целевые утверждения образуются здесь в таком же духе, как и при исполнении логической программы. Вследствие использования резолюции исполнение программы ( Р, GI) порождает каждое новое целевое утверждение Gt i так, чтобы выполнялось отношение Р, Gt Gt i - При выводе процедур с целью выбора информации на каждом шаге вместо множества процедур Р используется спецификация S, и в общем случае для работы с более произвольным синтаксисом целевых утверждений требуются более сложные правила вывода, чем правило резолюции. [39]
Этод метод более эффективен, чем предшествующие методы такие, как метод Эрбрана, используемый Гилмором. Однако неограниченное применение правила резолюций может вызвать порождение большого количества не относящихся к делу и излишних дизъюнктов. Чтобы убедиться в этом, рассмотрим простой пример. Предположим, что мы хотим показать методом резолюций, что множество S P / Q, - Р V Q, Р V - Q, - PV-Q невыполнимо. Эта процедура называется методом насыщения уровня. [40]
В этом параграфе мы покажем, что метод резолюций полон в задаче ответа на вопросы. Иными словами, если вопрос допускает ответ, то дизъюнкт-ответ будет порожден повторными применениями правила резолюции. [41]
Логическая программа начинает исполняться после того, как она подается на вход логическому интерпретатору. Интерпретатор представляет собой программу, способную строить резолютивные выводы, как правило, методом сверху вниз. Получив входную логическую программу, он предпринимает обычные шаги, необходимые для исполнения программы в режиме интерпретации: так, он осуществляет синтаксический контроль входных утверждений; хранит их в центральной памяти в соответствующей упрощенной, компактной и доступной форме; переводит входное целевое утверждение во внутреннее представление и затем начинает процесс построения вывода путем последовательного применения правила резолюции к текущему целевому утверждению и некоторой родительской процедуре, выбираемой из хранящейся в памяти версии входной программы. Если интерпретатору удается вывести пустое отрицание П, означающее, что решение получено, то он выдает какое-либо сообщение об этом вместе с найденными значениями целевых переменных. [42]
На практике такой подход почти всегда оказывается неудовлетворительным главным образом потому, что стандартное преобразование спецификации в множество дизъюнктов приводит, как правило, к значительной потере компактности и понятности. Трудно к тому же сопоставить общей резолюции какую-либо непосредственную вычислительную интерпретацию в духе решения задач, способную придать процессу вывода целенаправленность. Чаще поэтому предпочтительнее не преобразовывать спецификацию в множество дизъюнктов, а прямо из нее выводить желаемые процедуры, пользуясь теми правилами вывода, которые представляются наиболее удобными. Платой за это является тот факт, что эти правила зачастую оказываются более сложными и менее единообразными, чем правило резолюции. [43]
Метод, использованный для развертывания дерева в описанном выше примере ( рис. 38), называется методом поиска в ширину. Боковые дизъюнкты можно рассматривать как операторы, используемые для развертывания последовательных узлов дерева. Выделим все возможные боковые дизъюнкты и применим к ним правило резолюции с С в качестве центрального дизъюнкта. Rm ( и соответственно узлы) будем называть непосредственными наследниками узла С. Когда порождены все возможные непосредственные узлы-наследники узла С, мы скажем, что узел С развернут. Иначе говоря, развертывание узла означает порождение всех его непосредственных наследников. [44]