Cтраница 3
Представляет интерес свойство завершаемости метода резолюций: конечное множество S невыполнимо тогда и только тогда, когда пустой дизъюнкт может быть выведен из S с помощью резолюций. Из-леммы 1.3 следует достаточность этого условия. Пустой дизъюнкт, будучи невыполнимым, не может быть логическим следствием из выполнимого множества дизъюнктов. [31]
Лемма 1.4. Если множество дизъюнктов S невыполнимо и содержит резольвенты своих элементов, то оно обязательно содержит пустой дизъюнкт. [32]
Правила, показанные на рис. 16.7, предусматривают также обработку специальных случаев, в которых требуется избежать явного представления пустого дизъюнкта Кроме того, имеются два правила для упрощения дизъюнктов. Одно из них убирает избыточные подвыражения. [33]
Таким образом, невыполнимость множества S можно проверить, порождая логические следствия из S до тех пор, пока не получим пустой дизъюнкт. [34]
Каждый из дизъюнктов Ri, i e l: m, является возможным центральным дизъюнктом, который может привести к выводу пустого дизъюнкта. Если при этом RI пустой дизъюнкт, то решение задачи найдено. В противном случае для каждого Ri находим все возможные боковые дизъюнкты, подходящие для резольвенции с RJ в качестве центрального дизъюнкта, и продолжаем этот процесс до тех пор, пока не будет порожден пустой дизъюнкт. [35]
Метод резолюций, получив на вход логическую программу с присоединенным к ней запросом в виде множества хорновских дизъюнктов, пытается построить вывод пустого дизъюнкта, обозначаемого символом D. Если это ему удается, тогда цель допускается, в противном случае отвергается. Реализуется метод резолюций с помощью двух правил: правила резолюции и правила склейки, которые во время работы вызывают процедуру унификации - сопоставления. [36]
Если запрос касается описания некоторой вершины и описания ее нижележащих вершин по иерархической структуре, как в рассматриваемом примере, мы выводим не пустой дизъюнкт, а предикат ответа. [37]
Если в процессе вывода новых дизъюнктов ( резольвент) получают два однолитерных дизъюнкта, образующих контрарную пару, то резольвентой этих двух дизъюнктов будет пустой дизъюнкт П, или нулевая резольвента. [38]
Вывод пустого дизъюнкта может быть наглядно представлен с помощью дерева вывода, вершинами которого являются или исходные дизъюнкты, или резольвенты, а корнем - пустой дизъюнкт. [39]
Если S - конечное противоречивое множество дизъюнктов и Т - подмножество S такое, что S - Т выполнимо, то имеется вывод с поддержкой пустого дизъюнкта П из множества S, в котором Т является множеством поддержки. [40]
Приведенное только что доказательство может создать у читателя впечатление, что ИР не дает ничего по сравнению с теоремой Эрбрана, так как высота вывода пустого дизъюнкта в Ир - это в точности размер эрбрановской дизъюнкции. [41]
Мы отмечаем, что так как S состоит только из основных единичных дизъюнктов, правило резолюции применяется в D только на последнем шаге, когда получается пустой дизъюнкт Q. Так как множество S - С является - выполнимым, то С должен встретиться в D хотя бы один раз. [42]
Более детальная характеризация корректности и полноты SLD-резолюции получается путем включения в рассмотрение как решений целевого утверждения ( подстановок, дающих ответ), вычисляемых посредством вывода пустого дизъюнкта П, так и правила вычислений, используемого для их нахождения. Правило вычислений - это любое фиксированное правило, однозначно определяющее, какие из вызовов, содержащихся в текущем целевом утверждении, отрезаются на каждом шаге SLD-резолюции. [43]
Корректность и полнота общей резолюции позволяют в качестве частного случая довольно просто доказать, что SLD-резолюция также является корректной и полной в том простом смысле, что пустой дизъюнкт П выводим из множества дизъюнктов S тогда и только тогда, когда S невыполнимо. [44]
В сущности, пустое множество дизъюнктов обозначает, что к миру ( множеству высказываний) не предъявляются никакие требования ( высказывания), в то время как пустой дизъюнкт П, обозначая противоречие, тем самым вносит это противоречие в наш мир, делая его противоречивым, то есть неподтверждаемым. [45]