Предваренная нормальная форма

Для удобства анализа сложной формулы рекомендуется преобразовывать её к нормальной форме. Если в алгебре высказываний приняты две нормальные формы ДНФ и КНФ, то в алгебре предикатов ‑ кроме ДНФ и КНФ есть предварённая нормальная форма (ПНФ), суть которой сводится к разделению формулы на две части: префикс и матрицу.

Для этого все кванторы выносят влево по правилам логики предикатов, формируя префикс, а логические связки соединяют предикаты формулы, формируя матрицу. В результате будет получена формула: , где - префикс формулы при , а – матрица формулы. Затем матрицу формулы преобразуют к виду КНФ для определения истинности заключения.

Алгоритм приведения формулы к виду ПНФ:

1. Исключить логические связки и с помощью формул

, .

2. Перенести инверсии на элементарные формулы, использовать законы

, , ,

, .

3. Провести стандартизацию переменных. В пределах действия квантора имя переменной, по которой проводится квантификация, можно заменить на любое другое, не совпадающее с переменными, находящимися в этих пределах. Провести переименование переменных так, чтобы каждая связанная переменная имела уникальное имя (т.е. чтобы никакая переменная не имела бы одновременно свободных и связанных вхождений).

.

4. Вынести кванторы новых связанных переменных влево, не нарушая их последовательности.

5. Преобразовать бескванторную матрицу к виду КНФ, т. е. , где .

Пример 1. Привести формулу к виду ПНФ.

Решение. . Следовательно, предваренная нормальная форма формулы ‑ это . Матрица ПНФ содержит один элементарный дизъюнкт: .

Пример 2. Привести формулу к виду ПНФ.

Решение.

.

ПНФ ‑ это . Матрица ПНФ содержит три элементарных дизъюнкта: .

Пример 3. Привести формулу к виду ПНФ.

Решение.

.

Переименовываем связную переменную левого квантора :

.

ПНФ ‑ это . Матрица ПНФ содержит два элементарных дизъюнкта: .

Замечание. Одна формула может допускать много эквивалентных ПНФ. Вид результата зависит от порядка применения правил, а также от произвола при переименовании переменных.