Родитель(лиз,пат).
Goal
Предок(Y,Z).
Родитель(X,Y),
В пролог-программе представлены только посылки (посылки-факты и посылки-правила) и пока отсутствуют заключения теоремы. Заключения теоремы формулируются путем указания некоторой цели. После ввода вышеприведенной программы в пролог-систему последней можно будет задавать вопросы, касающиеся описанных в программе отношений. Поставленный системе вопрос является для нее целью (внешней целью), для достижения которой система использует информацию раздела clauses.Обычно система предлагает ввести цель с клавиатуры сразу после приглашения, например, в виде ? — (либо Цель: ). Вопрос о том, является ли Боб родителем Пат, должен быть введен так:
? — родитель(боб,пат).
Найдя соответствующий факт в программе, система ответит
Да
На вопрос
? — родитель(лиз,пат) система ответит
Нет ,
поскольку в программе ничего не говорится о том, является ли Лиз родителем Пат.
Цель для программы может быть внутренней. Тогда она указывается в разделе цели (goal), который записывается перед либо после раздела clauses и обязательно завершается точкой. Например, последний вопрос системе запишется в программе так:
Система способна ответить и на более интересные вопросы. Например, “кто является родителем Лиз?”:
? — родитель(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 после их унификации.
В посылках теоремы нет правила, предикатный символ которого был бы сопоставим с новой целью родитель(том, пат),поэтому такая цель оказывается неуспешной. Это говорит о том, что резольвенту – пустой дизъюнкт ( ) вывести из исходного множества дизъюнктов нельзя при этом варианте рассуждения. Теперь алгоритм делает возврат к исходной цели, т.е. к заключению теоремы, чтобы попробовать второй вариант вывода цели верхнего уровня предок(том,пат).Таким образом, пробуется правило
предок(X,Z) : —