Алгоритм преобразования предикатов в предложения

Предложение – правильно построенная формула (ППФ), состоящая из дизъюнкции литералов (предикатов) [11].

Теорема:Любая ППФ исчисления предикатов может быть преобразована во множество предложений.

Пример ППФ: .

Этапы преобразования:

1. Исключение символов импликации подстановкой вместо : .

2. Ограничение области действия символа отрицания одной атомарной формулой (закон Моргана): .

3. Разделение квантофицированных переменных: . Переменные переименовываются так, чтобы каждый квантор имел свою переменную.

4. Исключение кванторов существования путем введения сколемовской функции. Эта функция в качестве аргументов должна содержать переменные, связанные кванторами общности, в область действия которых попадает исключаемый квантор существования. Если не входит в область действия никакого , то вводится просто константа: . , – сколемовская функция.

5. Преобразование в предварительную форму: все перемещаются в начало ППФ: .

6. Приведение матрицы ППФ к конъюктивной нормальной форме. Используется замена : .

7. Исключение кванторов общности. Предполагается, что все переменные относятся к .

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

9. Переименовывание переменных. Символы переменных должны быть изменены так, чтобы каждый присутствовал только в одном предложении:

.