Сколемовская нормальная форма (СНФ)
Опр. Формула G имеет СНФ, если G = ( где формула Н не содержит кванторов и имеет КНФ (конъюктивную нормальную форму). Теорема: Для всякой формулы F существует формула G, имеющая СНФ и одновременно выполнимая (или невыполнимая) с F. Алгоритм приведения к СНФ: 1. Привод к ПНФ 2. Привести матрицу Н к ПНФ 3. Исключить кванторы 1) Если левее квантора 2) Если левее квантора Ех: после 2го шага имеем: F = ( предположим, что формула не содержит константы с, символов одноместной функции f и двухместной функции g. Тогда в формуле Н заменим: х – на с z – на f (y) v – на g (y,u) F = ( тогда G = ( Ех: привести функцию к СНФ F = ( Применяя законы: A (A F1 = ( которая имеет ПНФ приводим к КНФ F2 = ( сделаем подстановку x = a, z = f(y), получим G = (
|
x)…(
Р(а)
y) (
(
R(y))]
B;
Q x B) 
R(y))]
