Родитель(лиз,пат)

Система способна ответить и на более интересные вопросы. Например, “кто является родителем Лиз?”:

? — родитель(X,лиз).

На этот вопрос система не просто ответит «да» или «нет». Она скажет нам, каким должно быть значение X (ранее неизвестное), чтобы вышеприведенное утверждение было истинным, а также укажет количество решений. Поэтому мы получим ответ:

X=том 1 решен.

Вопрос «Кто дети Боба?» можно передать системе в такой форме:

? — родитель(боб,X).

В этом случае будет получен ответ:

X=энн

Х=пат 2 решен.

Программе можно задавать и более сложные вопросы, скажем, «Кто является родителем родителя Джима?». Поскольку в программе нет предиката типа родитель_родителя, вопрос можно составить из двух простых вопросов, используя связку И, например, так:

? — родитель(X,Y), родитель(Y,джим).

Ответ будет: X=боб

Y=пат 1 решен.

Если заключение теоремы не сможет использовать только посылки-факты, то алгоритм направляется к посылкам-правилам (дизъюнктам Хорна) и подменяет текущие цели новыми до тех пор, пока эти новые цели не окажутся простыми посылками-фактами.

Рассмотрим работу алгоритма доказательства теорем в пролог-системе, если, например, нужно попытаться достичь цели:

? — предок(том,пат).

Сначала алгоритм пробует найти такую посылку в теореме, из которой немедленно следует упомянутое заключение. Очевидно, единственными подходящими для этого посылками-правилами являются пр1 и пр2. Эти два правила реализуют отношение предок. Предикатные символы этих правил сопоставимы с предикатным символом заключения теоремы. Вначале алгоритм пробует посылку-правило пр1, стоящее в программе первым:

предок(X,Z): — родитель(X,Z). % пр1

Поскольку заключение - предок(том,пат), то значения переменным должны быть приписаны следующим образом:

X= том, Z= пат

Состоялась унификация {том / X, пат / Y } предикатов предок (X,Z) правила пр1 и предок(том,пат) заключения теоремы. Тогда исходная цель предок(том,пат) заменяется новой целью родитель(том,пат), так как этот предикат является резольвентой исходного заключения теоремы и головы правила пр1 после их унификации.

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