Рассмотрим вначале логику высказываний. Напомним, что литералом мы называли атомарную формулу или ее отрицание, дизъюнктом – дизъюнкцию литералов. Дизъюнкт может состоять из одного литерала. На дизъюнкт мы иногда будем смотреть, как на множество литералов, т.е. не будем различать дизъюнкты, которые получаются один из другого с помощью коммутативности и ассоциативности дизъюнкции, а также идемпотентности. Последнее означает, например, что дизъюнкты XÚØYÚX и XÚØY равны. Нам понадобится особый дизъюнкт – пустой, т.е. дизъюнкт, не содержащий литералов. Его мы будем обозначать "квадратиком" □. Будем считать, что пустой дизъюнкт ложен при любой интерпретации. Это означает, что формула F&□ равносильна □, а формула FÚ□ равносильна F. Пустой дизъюнкт есть фактически то же самое, что и атомарная формула 0, но в контексте метода резолюций принято использовать □.

Определение. Литералы L и ØL называются противоположными.

Метод резолюций в логике высказываний основан на правиле резолюций.

Определение. Правилом резолюций в логике высказываний называется следующее правило: из дизъюнктов ХÚF и ØXÚG выводим дизъюнкт FÚG.

Например, из дизъюнктов ØXÚYÚZ и XÚØY выводим дизъюнкты YÚZÚØY. Обратим внимание на то, что в первых двух дизъюнктах есть еще одна пара противоположных литаралов. Условимся, что можно применять правило резолюций не обязательно к самым левым литералам (поскольку мы не различаем дизъюнкты, отличающиеся порядком записи литералов). Тогда правило резолюций, примененное к Y и ØY, даст ØXÚZÚX. Условимся еще о следующем: в дизъюнктах не писать повторяющиеся литералы и не писать □, если есть другие литералы.

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

D,D₂,...,D_n

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

Например, если S={ØXÚYÚZ, ØYÚU, X}, то последовательность D₁=ØXÚYÚZ, D₂=ØYÚU, D₃=ØXÚZÚU, D₄=X, D₅=ZÚU – вывод из S. Дизъюнкт ZÚU выводим из S.

Применение метода резолюций основано на следующем утверждении, которое называется теоремой о полноте метода резолюций.

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

Доказательство. Докажем вначале достаточность.

Отметим, что правило резолюций сохраняет истинность. Это означает, что если j(ØXÚF)=1 и j(XÚG)=1 для некоторой интерпретации j, то j(FÚG)=1. Действительно, пусть j(ØXÚF)=1 и j(XÚG)=1. Тогда если j(F)=1, то и j(FÚG)=1. Если же j(F)=0, то j(ØX)=1, поскольку j(ØXÚF)=1. Но в этом случае j(X)=0 и j(G)=1, так как j(XÚG)=1. Если же j(G)=1, то и j(FÚG)=1.

Пусть из S выводим пустой дизъюнкт. Предположим противное: множество S выполнимо, т.е. существует интерпретация y, при которой все дизъюнкты из S истинны. Выводимость пустого дизъюнкта из S означает, что существует последовательность дизъюнктов D₁,…,D_n=□, каждый дизъюнкт которой принадлежит S или получается из предыдущих по правилу резолюций. Если дизъюнкт D_j из этой последовательности принадлежит S, то по предположению y(D_j)=1. Если же он получается из предыдущих по правилу резолюций, то также y(D_j)=1, поскольку правило резолюций сохраняет истинность. При i=n получаем, что y(□)=1. Противоречие показывает, что предположение о выполнимости множества S – ложное предположение. Следовательно, S невыполнимо. Достаточность доказана.

Докажем необходимость. Доказательство проведем индукцией по следующему параметру: d(S)=сумма числа вхождений литералов в дизъюнкты из S минус число дизъюнктов.

Пусть множество дизъюнктов S невыполнимо. Если пустой дизъюнкт принадлежит S, то он выводим из S (вывод в этом случае состоит из одного пустого дизъюнкта) и необходимость теоремы доказана. Будем считать в силу этого, что □ÏS. При этом предположении каждый дизъюнкт содержит хотя бы один литерал и поэтому d³1.

База индукции: d(S)=1. Если d(S)=1, то все дизъюнкты состоят из одного литерала. Поскольку множество S невыполнимо, то в нем должна найтись пара противоположных литералов X и ØX. В таком случае пустой дизъюнкт выводим из S, соответствующий вывод содержит три дизъюнкта: X, ØX, □.

Шаг индукции: d(S)>1. Предположим, что для любого множества дизъюнктов Т такого, что d(Т)<d(S) необходимость теоремы доказана. Пусть

S={D₁,D₂,…,D_k-1,D_k}.

Так как d(S)>1, то в S существует хотя бы один неодноэлементный дизъюнкт. Будем считать, что это дизъюнкт D_k, т.е. D_k=LÚD_k′, где L – литерал и D_k′¹□. Наряду с множеством дизъюнктов S рассмотрим еще два множества дизъюнктов

S₁={D₁,D₂,…,D_k-1,L},

S₂={D₁,D₂,…,D_k-1,D_k^/}.

Ясно, что S₁ и S₂ невыполнимы и что d(S₁)<a(S) и d(S₂)<a(S). По предположению индукции из S₁ и S₂ выводим пустой дизъюнкт. Пусть

A₁,A₂,…,A_i,…,A_l-1,A_l=□                    (1)

вывод пустого дизъюнкта из S₁ и

B₁,B₂,…,B_j,…B_m-1,B_m=□                  (2)

вывод пустого дизъюнкта из S₂. Если в первом выводе не содержится дизъюнкта L, то эта последовательность дизъюнктов будет выводом из S и необходимость теоремы доказана. Будем считать, что L содержится в первом выводе, пусть A_i=L. Аналогично предполагаем, что B_j=D_k′.

Если дизъюнкт Е получается из дизъюнктов Е₁ и Е₂ по правилу резолюций, то будем говорить, что Е непосредственно зависит от Е₁ (и от Е₂). Транзитивное замыкание отношения непосредственной зависимости назовем отношением зависимости (Другими словами, E зависит от Е^/, если существуют дизъюнкты Е₁,…,Е_n такие, что E=E₁,…,E_n=E^/ и Е₁ непосредственно зависит от Е₂,…,E_n-1 непосредственно зависит от E_n)_. Преобразуем второй вывод следующим образом: к дизъюнкту B_j и всем дизъюнктам, которые от него зависят, добавим литерал L. Новая последовательность дизъюнктов

B₁,B₂,…,B_j^/=D_k^/ÚL, B^/_j+1 ,…,B_m^/                    (3)

будет выводом из S. Если дизъюнкт B_m не зависит от B_j, то B_m^/ =□. Это означает, что из S выводим пустой дизъюнкт и необходимость теоремы доказана. Предположим, что B_m зависит от B_j. Тогда B_m^/=L. Преобразуем теперь первый вывод: на место дизъюнкта A_i (равного L) в этой последовательности подставили последовательность (3). Получим последовательность

A₁,…,A_i-1,B₁,…,B_j^/,B^/_j+1,…,B_m^/=L,A_i+1,…,A_l=□.

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

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

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

Проиллюстрируем сказанное на примере. Покажем, что формула G=Z является логическим следствием формул F₁=ØXÚY®X&Z, F₂=ØY®Z. Сформируем множество формул T={F₁,F₂,ØG}. Приведем формулы F₁ и F₂ к КНФ (формула ØG сама имеет эту форму). Мы получим, что

F₁ равносильна X&(ØYÚZ),

F₂ равносильна (YÚZ).

Тогда множество дизъюнктов S равно

{X, ØYÚZ, YÚZ, ØZ}.

Из множества S легко выводится пустой дизъюнкт:

ØYvZ, ØZ, ØY, YÚZ, У, □.

Следовательно, формула G является логическим следствием формул F₁, и F₂.