Для того, чтобы запустить программу на выполнение, нужно сформулировать цель. Цель состоит из взаимосвязанных предикатов. Пролог — система будет пытаться доказать цель, то есть логически вывести ее из имеющихся утверждений. Если цель состоит из конъюнкции предикатов (подцелей), то он будет доказывать подцели , выбирая их слева направо.
Если цель является фактом:
Goal: likes (mary, kiwi)
FALSE
Goal: likes (beth, apples)
TRUE
то ответ будет TRUE или FALSE.
Если цель содержит переменные, то Пролог выдаст или значения переменных, при которых цель истинна, или сообщение
No solutions (Нет решений)
Goal: likes (beth, X)
X= apples
Goal: likes(X, kiwi)
No solutions
Рассмотрим, как Пролог будет пытаться доказать цель «любит (бет, яблоки)» (рис 1.1).
Вначале Пролог будет пытаться сопоставить термы предиката цели и первого утверждения программы. Они сопоставимы. Затем сопоставляются термы объектов утверждения и цели. Сопоставление происходит слева направо. Объект «бет» цели несопоставим с объектом «мэри». Вся попытка сопоставить цель с первым утверждением неуспешна. Движемся слева направо — выбираем второе утверждение. Предикаты «любит» сопоставимы, объекты «бет» сопоставимы, при сопоставлении переменной X и объекта «яблоки», X получает значение «яблоки».
Переменная X стала СВЯЗАННОЙ или ОЗНАЧЕННОЙ.
Успешно сопоставив цель и голову правила «любит (бет, X)» с присвоением X значения «яблоки», Пролог переходит к доказательству тела правила, (голова правила будет истинна, если истинно тело). Для доказательства тела правила Пролог сам генерирует ПОДЦЕЛЬ «любит (мэри, яблоки)» и пытается ее доказать.
Сопоставление с первым фактом программы оказывается успешным, следовательно, успешно доказаны тело (и голова) правила и цель «любит (бет, яблоки)». Программа сообщит TRUE, хотя такого факта в программе в явном виде не было.
рис 1.1
Сопоставление — это процесс, проверяющий идентичность двух термов.
Если эти термы — константы или числа, то они сопоставимы, только когда они являются одним и тем же объектом.
Если один терм — константа, а другой — перемененная того же типа (в Турбо — Прологе каждый объект имеет строго определенный тип), то они сопоставимы, и переменная получает значение константы.
Два предиката сопоставимы, если:
— имеют одинаковый предикатный терм (главный функтор),
— одинаковую арность (число аргументов),
— все их соответствующие компоненты сопоставимы.
Значения переменных определяются при сопоставлении компонент.