Cтраница 1
Вывод пустого дизъюнкта может быть наглядно представлен с помощью дерева вывода, вершинами которого являются или исходные дизъюнкты, или резольвенты, а корнем - пустой дизъюнкт. [1]
Таким образом мы в процессе поиска вывода пустого дизъюнкта систематически перебираем возможные подстановки и унификации. [2]
Входное ( единичное) опровержение-это входной ( единичный) вывод пустого дизъюнкта. [3]
Каждый из дизъюнктов Ri, i e l: m, является возможным центральным дизъюнктом, который может привести к выводу пустого дизъюнкта. Если при этом RI пустой дизъюнкт, то решение задачи найдено. В противном случае для каждого Ri находим все возможные боковые дизъюнкты, подходящие для резольвенции с RJ в качестве центрального дизъюнкта, и продолжаем этот процесс до тех пор, пока не будет порожден пустой дизъюнкт. [4]
Метод резолюций, получив на вход логическую программу с присоединенным к ней запросом в виде множества хорновских дизъюнктов, пытается построить вывод пустого дизъюнкта, обозначаемого символом D. Если это ему удается, тогда цель допускается, в противном случае отвергается. Реализуется метод резолюций с помощью двух правил: правила резолюции и правила склейки, которые во время работы вызывают процедуру унификации - сопоставления. [5]
Приведенное только что доказательство может создать у читателя впечатление, что ИР не дает ничего по сравнению с теоремой Эрбрана, так как высота вывода пустого дизъюнкта в Ир - это в точности размер эрбрановской дизъюнкции. [6]
Более детальная характеризация корректности и полноты SLD-резолюции получается путем включения в рассмотрение как решений целевого утверждения ( подстановок, дающих ответ), вычисляемых посредством вывода пустого дизъюнкта П, так и правила вычислений, используемого для их нахождения. Правило вычислений - это любое фиксированное правило, однозначно определяющее, какие из вызовов, содержащихся в текущем целевом утверждении, отрезаются на каждом шаге SLD-резолюции. [7]
Какое бы правило вычислений ни применялось к программе, в Является подстановкой, дающей правильный ответ для программы, тогда и только тогда, когда она вычислима посредством вывода пустого дизъюнкта П с помощью SLD-резолюции. [8]
Если мы хотим написать машинную программу, которая будет делать за нас резолюцию и искать ответы на вопросы, то мы должны сообщить ей какие-то наводящие соображения, или эвристики, чтобы помочь в поиске вывода пустого дизъюнкта. Более подробно этот вопрос рассматривается в [19] и [86], но наиболее полезные методы таковы. [9]
Возвращаясь к примеру 1.10, в котором детектив должен доказать, что, если горничная сказала правду, то дворецкий солгал, мы видели, что дерево вывода ( см. рис. 1.2) линейно, и вывод пустого дизъюнкта был получен с помощью входной резолюции. В этом примере все дизъюнкты из S были хорновскими в отличие от примера 1.24, где дизъюнкт Р V Q - нехорновский. [10]
Литера, чье отрицание отсутствует во множестве дизъюнктов, называется чистой. Дизъюнкт, содержащий чистую литеру, естественно, не может участвовать в выводе пустого дизъюнкта и поэтому может быть удален из множества дизъюнктов. [11]