Скулемовска стандартная форма
1. Формула логики предикатов может быть приведена к равносильной формуле, имеющей предваренную нормальную форму. То есть к
формуле, у которой матрица не содержит никаких кванторов, а префикс есть последовательность кванторов.
2. Сохраняя противоречивость формулы, в ней можно избавится от квантора существования путем использования скулемовских
функций.
Полученное определение и называется скулемовской стандартной формой.
Покажем, как осуществляется уничтожение кванторов существования, с сохранением противоречивости формулы.
(Q1x1)…(Qnxn)M
• заменим самые левые кванторы существования, до квантора всеобщности на константы а1, а2,…
• внутренние кванторы существования, до которых есть(х1)(х2)…(хi)(xi+1),в М xi+1 заменить на f(x1,x2,…,xn).
Константы и функции, используемые для замены переменных квантора существования, называются скулемовскими функциями.
Результат – скулемовская стандартная форма.
Скулемовская форма, матрица которой является КНФ называется клазуальной формой.