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

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): —

Дата добавления: 2014-01-04