68
(10)	Г, V2 W	(9), удаление →
(11)	Г W	(4), (7), (10), удаление

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

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

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

Конъюнктивной нормальной формой (КНФ) называется конъюнкция конечного числа дизъюнктов.

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

– сначала из формулы исключаются все импликации

(используется равносильность U→V¬U V);

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

69

пропозициональным переменным; при этом снимаются двойные отрицания;

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

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

(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).

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

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

70

Пусть 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).

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

Теорема. Пусть Г – множество дизъюнктов (возможно,

бесконечное и содержащее бесконечное множество

71

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