Процесс унификации в языке Prolog работает путём последовательного сопоставления вопроса с фактами и правилами базы знаний с целью доказательства его реализуемости. 2

На каждом шаге выбирается очередной терм и отыскивается соответствующее выражение в базе знаний. 3 При этом переменные либо могут получить значение, либо вновь стать свободными. 3

Некоторые правила унификации термов: 3

1. Если термы term1 и term2 — константы, то они унифицируемы (сопоставимы), только если они равны. 3
2. Если term1 — терм, а Y — переменная, то они унифицируемы, при этом Y принимает значение term1. 3
3. Если term1 и term2 — составные термы, то они унифицируемы тогда и только тогда, когда у них одинаковые имена функторов, набор аргументов и каждая пара аргументов унифицируема. 3

Для отождествления двух термов в Прологе используется предикат равенство «=». 3 Он интерпретируется как оператор присваивания или как оператор проверки на равенство в зависимости от того, являются ли значения термов свободными или связанными. 3