Принцип резолюций

Будем говорить, что множество формул логики высказываний Г выполнимо, если существует такая оценка переменных, входящих в формулы из Г, при которой все формулы из Г принимают значение «истина»; в противном случае будем говорить, что множество формул Г невыполнимо.

Формула логики высказываний называется элементарной дизъюнкцией (дизъюнктом), если она представляет собой дизъюнкцию нескольких пропозициональных переменных и/или их отрицаний. Например, X∨Y, X∨Y∨Z, X, X дизъюнкты. Любой дизъюнкт, содержащий хотя бы одну переменную, выполним. Пустой дизъюнкт (обозначим его через Λ) – единственный невыполнимый дизъюнкт. Конъюнктивной нормальной формой (КНФ) называется конъюнкция конечного числа дизъюнктов.

Для любой формулы логики высказываний можно получить равносильную ей КНФ с помощью следующего алгоритма:

– сначала из формулы исключаются все импликации (используется равносильность U→V≅U∨V);

– необходимое число раз применяются законы де Моргана до тех пор, пока отрицания не будут относиться только к пропозициональным переменным; при этом снимаются двойные отрицания;

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

Пример.Приведем к КНФ формулу

(X→Y)→(Z→(X∧Y)).

Имеем

(X→Y)→(Z→(X∧Y)) ≅ (X∨Y)∨(Z∨(X∧Y)) ≅

≅ (X∧Y)∨(Z∨(X∧Y)) ≅ (X∧Y)∨(Z∨(X∧Y)) ≅

≅ (X∧Y)∨((Z∨X)∧(Z∨Y)) ≅

≅ (X∨Z∨X) ∧ (Y∨Z∨X) ∧ (X∨Z∨Y) ∧ (Y ∨Z∨Y) ≅

≅ (X∨Z) ∧ (X∨Y∨Z) ∧ (X∨Y∨Z).􀀀

Двойственным образом определяются дизъюнктивные нормальные формы. Элементарной конъюнкцией называется конъюнкция нескольких пропозициональных переменных и/или их отрицаний. Дизъюнктивной нормальной формой (ДНФ) называется дизъюнкция конечного числа элементарных конъюнкций.

Следующее правило называется правилом резолюций. Пусть U и V дизъюнкты, а X – пропозициональная переменная. Тогда из формул X∨U и X∨V логически следует формула U∨V.

Дизъюнкт U∨V называется резольвентой дизъюнктов X∨U и X∨V.

На правиле резолюций основывается метод доказательства невыполнимости набора дизъюнктов Г (метод резолюций):

последовательно составляется список дизъюнктов, в котором каждый из дизъюнктов либо входит в набор Г, либо является резолюцией выписанных ранее дизъюнктов; появление в списке пустого дизъюнкта свидетельствует о невыполнимости множества формул Г.

Пример.Покажем, используя метод резолюций, что из формул X∨Y, X∨Z, Y∨Z логически следует X. Доказываемое утверждение равносильно невыполнимости набора формул

X∨Y, X∨Z, Y∨Z, X.

Составим соответствующий список дизъюнктов (около резолюций в скобках указаны номера дизъюнктов, из которых они получены):

(1) X∨Y; (2) X∨Z; (3) Y∨Z; (4) X;

(5) Y (1,4); (6) Z (2,4); (7) Y (3,6); (8) Λ (5,7).􀀀

Без доказательства приведем следующую теорему.

Теорема.Пусть Г – множество дизъюнктов (возможно, бесконечное и содержащее бесконечное множество пропозициональных переменных). Если множество Г невыполнимо, это может быть установлено методом резолюций: существует конечная последовательность дизъюнктов, заканчивающаяся пустым дизъюнктом, в которой каждый дизъюнкт либо содержится в Г, либо получен из предыдущих по правилу резолюций.􀀀