Метод резолюций

Другое рассуждение (дающее ключ к пониманию метода логического вывода, назы­ваемого методом резолюций) заключается в следующем.

Чтобы доказать, что { F₁, F₂, …, F_n }Þ F, необходимо доказать, что формула (F₁ & F₂ & … & F_n) → F тавтология. Для того чтобы доказать, что данная формула является тавтологией, для этого достаточно до­казать, что ее отрицание является противоречием, т.е. что формула ù(F₁ & F₂ & … & F_n → F) – противоречие. То есть противоречием должна являться ù(ù(F₁ & F₂ & … & F_n) Ú F) или формула (F₁ & F₂ & … & F_n & ù F) т.е. противоречивым является множество формул F, состоящее из множества посылок F₁, F₂, …, F_n и отрицания заключения ù F.

Первым шагом для применения метода резолюций служит приведение пропозициональной формулы к логически эквивалентной ей конъюнктивной нормальной форме.

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

Дизъюнктом (в англоязычной литературе называют clause, что означает предложение в сложносочиненном предложении) называется дизъюнкция конечного числа литер, т. е. пропозициональных символов или их отрицаний:

D = (p₁ Ú p₂ Ú...Ú p_n).

Дизъюнкты, содержащие противоположные литеры (A Ú ù A) являются тавтологиями и их можно отбросить, т. к. они не влияют на значение формы. Если в пределах од­ного и того же дизъюнкта встречается несколько раз одна и та же литера (например, A Ú A), то достаточно записать ее лишь один раз. В результате таких упрощений будет получена приведенная или совершенная КНФ.

Пустым дизъюнктом называется константа false. Если КНФ не содержит ни одного дизъюнкта (иначе пуста), то она эквивалентна true.

КНФ общезначима (является тавтологией), если все ее дизъюнкты общезначимы.

Дизъюнкт невыполним в том и только том случае, если он пустой.

Понятие дизъюнкта важно в логическом программировании и, в частности, в языке Пролог, т. к. описание задачи осуществляется в терминах дизъюнктов, часто назы­ваемых (в переводах на русский) клаузами или клозами.