Определение.Правилом резолюций в логике предикатов называется правило из дизъюнктов ØP(t1,...,tn)ÚF и P(s1,...,sn)ÚG выводим дизъюнкт s(F)Ús(G), где s – наиболее общий унификатор множества {P(t1,...,tn), P(s1,...,sn)}. Дизъюнкт s(F)Ús(G) называется бинарной резольвентой первых двух дизъюнктов, а литералы ØP(t1,…,tn) и P(s1,…,sn) отрезаемыми литералами.
Например, с помощью правила резолюций из дизъюнктов ØQ(a,f(x))ÚR(x) и Q(u,z)ÚØP(z) можно вывести дизъюнкт R(x)ÚØP(f(x)), используя подстановку s={u=a, z=f(x)}.
В отличие от логики высказываний, в логике предикатов нам понадобится еще одно правило.
Определение.Правилом склейки в логике предикатов называется правило: из дизъюнкта àP(t1,...,tn)Ú...ÚàP(s1,...,sn)ÚF выводим дизъюнкт s (àP(t1,...,tn)Ú s (F), где s – наиболее общий унификатор множества {P(t1,...,tn),...,P(s1,...,sn)}, à – знак отрицания или его отсутствие. Дизъюнкт s(◊P(t1,…,tn)Ús(F) называется склейкой первого дизъюнкта. (Отметим, что если знак отрицания стоит перед одной из записанных выше атомарных формул, то он стоит и перед другими.)
Например, правило склейки, примененное к дизъюнкту ØР(х,у)ÚØP(у,х)ÚØР(а,а)ÚQ(x,y,v), дает дизъюнкт ØР(а,а)ÚQ(a,a,v).
Определение вывода в логике первого порядка немного отличается от аналогичного определения в логике высказываний.
Определение. Пусть S – множество дизъюнктов.Выводом из множества дизъюнктов S называется последовательность дизъюнктов D1,D2,…,Dn, такая, что каждый дизъюнкт Di принадлежит S, выводим из предыдущих дизъюнктов по правилу резолюций или выводим из предыдущего по правилу склейки.
Как и в логике высказываний, дизъюнкт D выводим из S, если существует вывод из S, последним дизъюнктом которого является D.
является выводом из S. Отметим, что D1,D2,D5ÎS, дизъюнкт D3 выводим из D1 и D2 по правилу резолюций, дизъюнкт D6 выводим из D4 и D5 по тому же правилу, а D4 выводим из D3 по правилу склейки.
Как и в логике высказываний, в логике первого порядка есть утверждение, называемое теоремой о полноте. Фактически это утверждение совпадает с формулировкой 4.1. Тем не менее приведем его.
Теорема 4.3. Множество дизъюнктов S логики первого порядка невыполнимо тогда и только тогда, когда из S выводим пустой дизъюнкт.
Теорема имеет довольно сложное доказательство.
В данном параграфе мы ограничимся примером применения метода резолюций и рядом определений, необходимых для доказательства теоремы 4.3.
Для доказательства логичности следствия формулы G из формул F1,…,Fk метод резолюций в логике предикатов применяется почти так же, как и в логике высказываний. А именно, сначала составляется множество формул T={F1,…,Fk,ØG}. Затем каждая из формул этого множества приводится к сколемовской нормальной форме, в полученных формах вычеркиваются кванторы общности и связки конъюнкции. Получается множество дизъюнктов S. На последнем этапе находится вывод пустого дизъюнкта из множества S. Напомним, что все переменные в дизъюнктах предполагаются связанными кванторами общности. Это означает, что метод резолюций для доказательства логичности может применяться лишь в случае, когда формулы F1,…, Fk и G не имеют свободных переменных. Если все же формулы содержат свободные переменные, то их надо заменить константами (такими, которые отсутствуют в этих формулах).
Докажем, что формула G является логическим следствием множества формул F1,F2. Для этого достаточно доказать невыполнимость множества Т={F1,F2,ØG}. Каждую из формул множества Т приведем к сколемовской нормальной форме; получим формулы ("y)[П(а) & (ØC(у)ÚЗ(а,у))], ("х)("у)[ØП(х)ÚØЛ(у)ÚØЗ(х,у)], C(в) & Л(в).
Тогда множество S будет содержать дизъюнкты: D1=П(а), D2=ØC(у)ÚЗ(а,у), D3=ØП(х)ÚØЛ(у)ÚØЗ(х,у), D4=C(в), D5=Л(в). А последовательность дизъюнктов D1, D3, ØЛ(у)ÚØЗ(а,у), D5, ØЗ(а,в), D2, D4, З(а,в), □ будет выводом из S. Cледовательно, формула G является логическим следствием формул F1 и F2.
Введем, как было обещано выше, ряд определений, необходимых в следующих параграфах.
Напомним, что мы условились не писать в дизъюнктах повторяющиеся литералы. Это позволяет нам смотреть, если это необходимо, на дизъюнкт как на множество литералов. Если смотреть на дизъюнкты как на множество литералов, то результат применения правила резодюций к дизъюнктам D1 и D2 с отрезаемыми литералами L1 и L2 можно записать так D=[s(D1)-s(L1)]È[s(D2)-s(L2)], где s – наиболее общий унификатор L1 и ØL2.
Определение.Резольвентой дизъюнктов D1 и D2 называется одна из следующих бинарных резольвент:
1) бинарная резольвента дизъюнктов D1 и D2,
2) бинарная резольвента склейки D1 и дизъюнкта D2,
3) бинарная резольвента дизъюнкта D1 и склейки D2,
4) бинарная резольвента склейки D1 и склейки D2.
Приведем пример. Пусть D1=ØP(y)ÚØP(g(x))ÚR(f(y)), D2=P(g(a))ÚQ(b). Склейка дизъюнкта D1 есть дизъюнкт D1/=ØP(g(x))ÚR(f(g(x)). Бинарная резольвента D1 и D2/ равна R(f(g(a)))ÚQ(b). Следовательно, последний дизъюнкт есть резольвента дизъюнктов D1 и D2.
