Применение поднятых правил логического вывода связано с необходимостью поиска подстановок, в результате которых различные логические выражения становятся идентичными. Этот процесс называется унификацией и является ключевым компонентом любых алгоритмов вывода в логике первого порядка. Алгоритм Unify принимает на входе два высказывания и возвращает для них унификатор, если таковой существует:

Рассмотрим несколько примеров того, как должен действовать алгоритм Unify. Предположим, что имеется запрос Knows {John, χ) — кого знает Джон? Некоторые ответы на этот запрос можно найти, отыскивая все высказывания в базе знаний, которые унифицируются с высказыванием Knows {John ,x). Ниже приведены результаты унификации с четырьмя различными высказываниями, которые могут находиться в базе знаний.

Последняя попытка унификации оканчивается неудачей (fail), поскольку переменная χ не может одновременно принимать значения John и Elizabeth. Теперь вспомним, что высказывание Knows {x, Elizabeth) означает "Все знают Элизабет", поэтому мы обязаны иметь возможность вывести логически, что Джон знает Элизабет. Проблема возникает только потому, что в этих двух высказываниях, как оказалось, используется одно и то же имя переменной, х. Возникновения этой проблемы можно избежать, стандартизируя отличие (standardizing apart) одного из этих двух унифицируемых высказываний; под этой операцией подразумевается переименование переменных в высказываниях для предотвращения коллизий имен. Например, переменную χ в высказывании Knows (x, Elizabeth) можно переименовать в z17 (новое имя переменной), не меняя смысл этого высказывания. После этого унификация выполняется успешно: