Канонические представления формул логики предикатов

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

Предваренная нормальная формула (ПНФ)

Предваренной (или пренексной) формулой называется формула вида

j: Q₁(x₁)Q₂(x₂)…Q_n(x_n) s,

где Q_iÎ{", $} кванторы, s - формула без кванторов. Выражение (Q₁(x₁)Q₂(x₂)…Q_n(x_n)) называется префиксом формулы j, а s - матрицей предваренной нормальной формы, если она находится в конъюнктивной нормальной форме (КНФ). Таким образом, в предваренной формуле все кванторы находятся в начале формулы. Бескванторная формула также считается предваренной.

Теорема о предваренной форме. Для всякой формулы А существует предваренная формула В и А~В (А равносильна В).

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

1. Преобразование формул, устраняющее логические связки ® и «.

2. Пронесение отрицания вглубь подформул, чтобы отрицания находились только над атомами.

3. Вынесение кванторов за скобки в порядке их следования в формуле с учетом общезначимых эквивалентностей логики предикатов.

4. При необходимости переименование связанных переменных в подформулах во избежание коллизии переменных.

5. Представление полученной бескванторной формулы в КНФ.

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

Следующим шагом является преобразование предложения j в универсальное предложение j*, которое содержит только кванторы общности, находится в предваренной форме и выполнимо тогда и только тогда, когда выполнимо j. Кванторы в префиксе ПНФ должны следовать в том порядке, в каком они встречаются в формуле.

Кванторы можно выносить в разном порядке, так что вид кванторной приставки зависит от способа получения предваренной формы. (?)