Представление формулы в КНФ

Получение множества Ф₁ (объединение формул ) эквивалентно КНФ соответствующей формулы. Так как какая-либо интерпретация удовлетворяет формуле вида в том и только в том случае, если она удовлетворяет формулам и К₁, К₂, …, К_n одновременно, то исходную формулу Ф₁ можно заменить множеством конъюнктивных членов (дизъюнктов).

Пример. .

Исключим знаки импликации:

.

Уменьшим области действия знаков отрицания до одного предиката:

.

Произведем стандартизацию переменных:

Проведем сколемизацию:

Здесь g(z) – функция Сколема, зависящая только от x, она находится в области действия квантора.

Получим предваренную форму формулы:

.

Исключим кванторы общности:

.

Используя закон дистрибутивности, получим КНФ:

.