• Демодуляция. Для любых термов х, у и z, где Unify (x, z) =θ и mn[z] — литерал, содержащий z, справедливо следующее:

Демодуляция обычно используется для упрощения выражений с помощью коллекции утверждений, таких как х+0=х, х1=х и т.д. Это правило может быть также дополнено, чтобы можно было учитывать неединичные выражения, в которых появляется литерал со знаком равенства, как показано ниже.

• Парамодуляция. Для любых термов х, у и z, где Unify (χ, z) =θ, справедливо следующее:

В отличие от демодуляции, парамодуляция позволяет получить полную процедуру логического вывода для логики первого порядка с отношением равенства.

В третьем подходе формирование логических рассуждений с учетом равенства полностью осуществляется с помощью расширенного алгоритма унификации. Это означает, что термы рассматриваются как унифицируемые, если можно доказать, что они становятся равными при некоторой подстановке; здесь выражение "можно доказать" допускает включение в определенном объеме рассуждений о равенстве. Например, термы 1 + 2 и 2 + 1 обычно не рассматриваются как унифицируемые, но алгоритм унификации, в котором известно, что х+у=у+х, способен унифицировать их с помощью пустой подстановки. Унификация с учетом равенства (equational unification) такого рода может выполняться с помощью эффективных алгоритмов, разработанных с учетом данных конкретных используемых аксиом (коммутативность, ассоциативность и т.д.), а не с помощью явного логического вывода на основе этих аксиом. Программы автоматического доказательства теорем с использованием этого метода очень близки к системам логического программирования в ограничениях, описанным в разделе 9.4.