Cтраница 4
Таким образом, можно порождать дизъюнкты P ( f ( n) ( a)) для всех значений п, но невозможно породить другие одноэлементные дизъюнкты или пустой дизъюнкт. Следовательно, исходное множество выполнимо. [46]
Какое бы правило вычислений ни применялось к программе, в Является подстановкой, дающей правильный ответ для программы, тогда и только тогда, когда она вычислима посредством вывода пустого дизъюнкта П с помощью SLD-резолюции. [47]
Если мы хотим написать машинную программу, которая будет делать за нас резолюцию и искать ответы на вопросы, то мы должны сообщить ей какие-то наводящие соображения, или эвристики, чтобы помочь в поиске вывода пустого дизъюнкта. Более подробно этот вопрос рассматривается в [19] и [86], но наиболее полезные методы таковы. [48]
Возвращаясь к примеру 1.10, в котором детектив должен доказать, что, если горничная сказала правду, то дворецкий солгал, мы видели, что дерево вывода ( см. рис. 1.2) линейно, и вывод пустого дизъюнкта был получен с помощью входной резолюции. В этом примере все дизъюнкты из S были хорновскими в отличие от примера 1.24, где дизъюнкт Р V Q - нехорновский. [49]
Обычно интерпретатор логических программ начинает свою работу с целевого утверждения, например, такого, как - Р ( х ] & Q ( x) & R ( y), состоящего из трех подцелей Р ( х), Q ( x) и R ( y и пытается с помощью принципа резолюции вывести пустой дизъюнкт. Для этого он ищет подходящий дизъюнкт, который разрешает подцель, скажем, Р ( х) и формирует новое целевое утверждение. В образующемся дереве вывода возникают следующие виды параллелизма. [50]