Подстановкой называют конечное множество вида θ = {t1/x1; t2/x2;… tn/xn}, где ti – терм, xi – предметная переменная, отличная от ti. Выполнив подстановку по всем предметным переменным, можно получить новые формулы, которые допускают унификацию в смысле формирования контрарных пар, т. е. P(x) P(x)Множество подстановок можно формировать последовательно, просматривая каждый раз только одну предметную переменную. Рассмотренный метод имеет наиболее общий характер унификации и играет важную роль в языке Пролог, так как обобщает механизм вызова процедур, используемых в обычных языках программирования. Обычно аргументы вызова процедуры – это выражения, которые подставляют вместо формальных параметров и могут быть только именами переменных. Однако в прологе разрешается, чтобы сами формальные параметры были термами, и потому процесс вызова “логической процедуры” включает совмещение термов, являющихся аргументами вызова, с термами из заголовка вызова процедуры с помощью метода унификации. Если унификация оканчивается неудачей из-за того, что никакая подстановка не сможет совместить нужные литеры, то вызова не произойдёт, но будет сделана попытка совмещения с другим определением процедуры, если такая имеется.