Как работает механизм унификации в Prolog?

Унификация в Прологе — это процесс последовательного сопоставления вопроса с фактами и правилами базы знаний с целью доказательства его реализуемости. pgsha.ru:8008

На каждом шаге унификации выбирается очередной терм (объект) и отыскивается соответствующее выражение в базе знаний. edu.tsu.ru При этом переменные либо могут получить значение, либо вновь стать свободными. edu.tsu.ru

Если в вопросе есть свободные переменные, то Пролог ищет значения переменных, при которых цель достижима. pgsha.ru:8008 Если в вопросе нет свободных переменных, то Пролог ищет возможность унификации цели и в качестве ответа выдаёт результативность такой унификации. pgsha.ru:8008

Процесс сопоставления первичной основной цели происходит последовательно по всем предложениям в базе знаний — сверху вниз. pgsha.ru:8008 Если цель оказывается головой какого-то предложения, тело которого состоит из нескольких предикатов, то основная цель разбивается на подцели, доказательством которых Пролог занимается по отдельности и последовательно. pgsha.ru:8008

В случае неудачи унификации срабатывает механизм бэктрекинга: Пролог обращается к стеку точек возврата и, при наличии там точек возврата, возвращается к ближайшей точке развилки. pgsha.ru:8008 При таком возврате переменные восстанавливают те значения, которые они имели в данной точке до начала унификации по текущему неуспешному пути. pgsha.ru:8008 В дальнейшем процесс унификации уже протекает по следующему (альтернативному) пути. pgsha.ru:8008