Начнем с формулировки правила резолюций.

Определение. Правилом резолюций в логике предикатов называется правило из дизъюнктов ØP(t₁,...,t_n)ÚF и P(s₁,...,s_n)ÚG выводим дизъюнкт s(F)Ús(G), где s – наиболее общий унификатор множества {P(t₁,...,t_n), P(s₁,...,s_n)}. Дизъюнкт s(F)Ús(G) называется бинарной револьвентой первых двух дизъюнктов, а литералы ØP(t₁,…,t_n) и P(s₁,…,s_n) отрезаемыми литералами.

Например, с помощью правила резолюций из дизъюнктов ØQ(a,f(x))ÚR(x) и Q(u,z)ÚØP(z) можно вывести дизъюнкт R(x)ÚØP(f(x)), используя подстановку s={u=a, z=f(x)}.

В отличие от логики высказываний, в логике предикатов нам понадобится еще одно правило.

Определение. Правилом склейки в логике предикатов называется правило: из дизъюнкта àP(t₁,...,t_n)Ú...ÚàP(s₁,...,s_n)ÚF выводим дизъюнкт s (àP(t₁,...,t_n)Ú s (F), где s – наиболее общий унификатор множества {P(t₁,...,t_n),...,P(s₁,...,s_n)}, à – знак отрицания или его отсутствие. Дизъюнкт s(◊P(t₁,…,t_n)Ús(F) называется склейкой первого дизъюнкта. (Отметим, что если знак отрицания стоит перед одной из записанных выше атомарных формул, то он стоит и перед другими.)

Например, правило склейки, примененное к дизъюнкту ØР(х,у)ÚØP(у,х)ÚØР(а,а)ÚQ(x,y,v), дает дизъюнкт ØР(а,а)ÚQ(a,a,v).

Определение вывода в логике первого порядка немного отличается от аналогичного определения в логике высказываний.

Определение. Пусть S – множество дизъюнктов.Выводом из множества дизъюнктов S называется последовательность дизъюнктов

D₁,D₂,…,D_n,

такая, что каждый дизъюнкт D_i принадлежит S, выводим из предыдущих дизъюнктов по правилу резолюций или выводим из предыдущего по правилу склейки.

Как и в логике высказываний, дизъюнкт D выводим из S, если существует вывод из S, последним дизъюнктом которого является D.

Приведем пример. Пусть S={ØB(x)ÚØC(x)ÚT(f(x)), C(у)ÚT(f(z)), B(a)}. Тогда последовательность

является выводом из S. Отметим, что D₁,D₂,D₅ÎS, дизъюнкт D₃ выводим из D₁ и D₂ по правилу резолюций, дизъюнкт D₆ выводим из D₄ и D₅ по тому же правилу, а D₄ выводим из D₃ по правилу склейки.

Как и в логике высказываний, в логике первого порядка есть утверждение, называемое теоремой о полноте. Фактически это утверждение совпадает с формулировкой 4.1. Тем не менее приведем его.

Теорема 4.3. Множество дизъюнктов S логики первого порядка невыполнимо тогда и только тогда, когда из S выводим пустой дизъюнкт.

Теорема имеет довольно сложное доказательство. Оно будет приведено в §6.

В данном параграфе мы ограничимся примером применения метода резолюций и рядом определений, необходимых для доказательства теоремы 4.3.

Для доказательства логичности следствия формулы G из формул F₁,…,F_k метод резолюций в логике предикатов применяется почти так же, как и в логике высказываний. А именно, сначала составляется множество формул T={F₁,…,F_k,ØG}. Затем каждая из формул этого множества приводится к сколемовской нормальной форме, в полученных формах вычеркиваются кванторы общности и связки конъюнкции. Получается множество дизъюнктов S. На последнем этапе находится вывод пустого дизъюнкта из множества S. Напомним, что все переменные в дизъюнктах предполагаются связанными кванторами общности. Это означает, что метод резолюций для доказательства логичности может применяться лишь в случае, когда формулы F_1,…, F_k и G не имеют свободных переменных. Если все же формулы содержат свободные переменные, то их надо заменить константами (такими, которые отсутствуют в этих формулах).

Рассмотрим пример. Пусть

Докажем, что формула G является логическим следствием множества формул F₁,F₂. Для этого достаточно доказать невыполнимость множества Т={F₁,F₂,ØG}. Каждую из формул множества Т приведем к сколемовской нормальной форме; получим формулы

Тогда множество S будет содержать дизъюнкты: D₁=П(а), D₂=ØC(у)ÚЗ(а,у), D₃=ØП(х)ÚØЛ(у)ÚØЗ(х,у), D₄=C(в), D₅=Л(в). А последовательность дизъюнктов D₁, D₃, ØЛ(у)ÚØЗ(а,у), D₅, ØЗ(а,в), D₂, D₄, З(а,в), □ будет выводом из S. Cледовательно, формула G является логическим следствием формул F₁ и F₂.

Введем, как было обещано выше, ряд определений, необходимых в следующих параграфах.

Напомним, что мы условились не писать в дизъюнктах повторяющиеся литералы. Это позволяет нам смотреть, если это необходимо, на дизъюнкт как на множество литералов. Если смотреть на дизъюнкты как на множество литералов, то результат применения правила резодюций к дизъюнктам D₁ и D₂ с отрезаемыми литералами L₁ и L₂ можно записать так

D=[s(D₁)-s(L₁)]È[s(D₂)-s(L₂)],

где s – наиболее общий унификатор L₁ и ØL₂.

Определение. Револьвентой дизъюнктов D₁ и D₂ называется одна из следующих бинарных револьвент:

1) бинарная револьвента дизъюнктов D₁ и D₂,

2) бинарная револьвента склейки D₁ и дизъюнкта D₂,

3) бинарная револьвента дизъюнкта D₁ и склейки D₂,

4) бинарная револьвента склейки D₁ и склейки D₂.

Приведем пример. Пусть D₁=ØP(y)ÚØP(g(x))ÚR(f(y)), D₂=P(g(a))ÚQ(b). Склейка дизъюнкта D₁ есть дизъюнкт D₁^/=ØP(g(x))ÚR(f(g(x)). Бинарная револьвента D₁ и D₂^/ равна R(f(g(a)))ÚQ(b). Следовательно, последний дизъюнкт есть револьвента дизъюнктов D₁ и D₂.

Определение. Если D – дизъюнкт, а s – подстановка, то дизъюнкт s(D) называется примером дизъюнкта D.

Следующее утверждение часто называют леммой о подъеме.

Теорема 4.4. Если D₁^/ – пример дизъюнкта D₁, D₂^/ – пример дизъюнкта D₂ и D^/ – револьвента D₁^/ и D₂^/, то существует револьвента D дизъюнктов D₁ и D₂ такая, что D^/ – пример D.

Доказательство. Если D₁ и D₂ имеют лбщие переменные, то заменой переменных в одном из дизъюнктов можно добиться того, что переменные дизъюнкта D₁ отличны от переменных дизъюнкта D₂. Будем поэтому считать, что D₁ и D₂ не имеют общих переменных.

Так как D₁^/ – пример D₁ и D₂^/ – пример D₂, то существуют подстановки a₁ и a₂ такие, что D₁^/=a₁(D₁) D₂^/=a₂(D₂). Последовательность a=(a₁,a₂) также будет подстановкой и поскольку  D₁ и D₂ не имеют общих переменных, то D₁^/=a(D₁) и D₂^/=a(D₂).

Дизъюнкт D^/ является револьвентой дизъюнктов D₁^/ и D₂^/. Это означает, что существуют литералы L₁^/ÎD₁^/ и L₂^/ÎD₂^/ и подстановка t такие, что t наиболее общий унификатор L₁^/ и ØL₂^/ и

D^/=(t(D₁^/)-t(L₁^/))È(t(D₂^/)-t(L₂^/)).                   (1)

(Если при получении револьвенты D^/ к дизъюнктам D₁^/ т D₂^/ применялись склейки, то будем считать, что они учтены подстановками a₁ и a₂.)

Пусть L₁¹,…,L₁^r – литералы дизъюнкта D₁, которые подстановкой a переводятся L₁^/, а L₂¹,…,L₂^s – литералы дизъюнкта D₂, которые подстановкой a переводятся в L₂^/. Литералы L₁¹,…,L₁^r, следовательно, унифицируемы, а поэтому существует наибелее общий унификатор b₁ для этого множества. Дизъюнкт b₁(L₁¹) (равный b₁(L₁²),…,b₁(L₁^r)) обозначим через L₁. По определению наиболее общего унификатора найдется подстановка g₁,  для которой выполняется равенство a₁=g₁◦b₁. По аналогичным соображениям, существуют подстановки b₂ и g₂ такие, что b₂ – наиболее общий унификатор множества литералов L₂¹,…,L₂^s и a₂=g₂ ◦b₂. Литерал  b₂(L₂¹) обозначим через L₂. Дегко видеть, что L₁ и L₂ не имеют общих переменных. Поскольку дизъюнкты D₁ и D₂ также не имеют общих переменных, то можно считать, что  b₁=b₂=b, g₁=g₂=g и a=g◦b. Сказанное в этом абзаце иллюстрируется рисунками 4.1 и 4.2.

Рис. 4.1

Рис. 4.2

Литералы L₁′ и ØL₂′, как отмечено выше, унифицируемы подстановкой t. Следовательно, литералы L₁ и ØL₂ также унифицируемы (подстановкой t◦g). Отсюда следует, что существует наиболеее общий унификатор s множества {L₁ ØL₂} (см.рис.4.3). Возьмем в качестве D дизъюнкт

D=[s(b(D₁))–s(L₁)]È[s(b(D₂]–s(L₂)]                      (2)

Ясно, что D – резольвента дизъюнктов D₁ и D₂. Осталось показать. Что D′ –пример D.

Рис. 4.3

Так как s – наиболее общий унификатор L₁ и ØL₂, то существует подстановка s такая, что t○g=d○s. В таком случае из последнего равенства, равенств (1), (2) и a=g○b следует, что

D′=(t(D₁′)–t(L₁′))È(t(D₂′)–t(L₂′))=[t(a(D₁))–t(a(L₁¹))]È[t(a(D₂))–(r(a(L₂¹))=

[(t◦a)(D₁)–(t◦a)(L₁¹)]È[(t◦a)(D₂)–(t◦a)(L₂¹)]=

[(t◦g◦b)(D₁)–(t◦g◦b)(L₁¹)]È[(t◦g◦b)(D₂)–(t◦g◦b)(L₂¹)]=

[(d◦s◦b)(D₁)–(d◦s◦b)(L₁¹)]È[(d◦s◦b)(D₂)–(d◦s◦b)(L₂¹)]=

d[s(b(D₁))–s(L₁)]Èd[s(b(D₂))–s(L₂)]=d(D).

Мы доказали, что D′ – пример D.

Теорема доказана.