9. Метод резолюций для логики первого порядка

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

Определение. Правилом резолюций в логике предикатов называется правило из дизъюнктов 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)}. Тогда последовательность D1=B(x)C(x)T(f(x)), D2=C(у)T(f(z)), D3=B(x)T(f(x))T(f(z)), D4=B(x)T(f(x)), D5=B(a), D6=T(f(a)).

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

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

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

Теорема имеет довольно сложное доказательство.

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

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

Рассмотрим пример. Пусть F1=(х)[П(х) & (у)(С(у)  З(х,у))], F2=(x)(у)[П(х) & Л(у)  З(х,у)], G=(x)(C(x)Л(х)).

Докажем, что формула G является логическим следствием множества формул F₁,F₂. Для этого достаточно доказать невыполнимость множества Т={F₁,F₂,G}. Каждую из формул множества Т приведем к сколемовской нормальной форме; получим формулы (y)[П(а) & (C(у)З(а,у))], (х)(у)[П(х)Л(у)З(х,у)], C(в) & Л(в).

Тогда множество 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₂.