словами, 
содержит одиночный литерал, равный отрицанию одиночного литерала в 
Тогда грворят, что два предложения 
разрешаются, а новое предложение
является их резольвентой.
Резольвента представляет собой выведенное предложение, и процесс образования резольвенты из двух «родительских» предложений называется резольвенцией. Если два предложения разрешаются, то они могут иметь более одной резольвенты, поскольку способ выбора 
может оказаться не единственным. Но, во всяком случае, они имеют не более конечного числа резольвент. Сейчас мы дадим несколько примеров резольвенции и попытаемся связать ее с более знакомыми нам правилами вывода.
Рассмотрим два предложения
и
Выбирая подмножества
мы получаем резольвенту
а если взять
то резольвентой будет
Всего для этих двух предложений есть четыре резольвенты: три из них получаются разрешением на Р и одна разрешением на 
Резольвенция является общим правилом вывода, объединяющим подстановку, modus ponens и различные типы силлогизмов. Рассмотрим резольвенту 
двух предложений 
Если первое предложение записать в виде 
то ясно, что в этом случае резольвенция совпадает с modus ponens.
Рассмотрим теперь резольвенту 
двух предложений 
. В более привычных обозначениях (а также на русском языке) эта цепочка рассуждений выглядит так:
Такой вывод является одним из силлогизмов.
и переменные, входящие в не встречаются в 
и обратно. Пусть 
— такие два подмножества в 
что для объединения 
существует наиболее общий унификатор К. (Иными
