SHPORA.net :: PDA

[ Back ]

1. Формула логики предикатов может быть приведена к равносильной формуле, имеющей предваренную нормальную форму. То есть к



формуле, у которой матрица не содержит никаких кванторов, а префикс есть последовательность кванторов.

2. Сохраняя противоречивость формулы, в ней можно избавится от квантора существования путем использования скулемовских



функций.

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

Покажем, как осуществляется уничтожение кванторов существования, с сохранением противоречивости формулы.

(Q1x1)…(Qnxn)M

• заменим самые левые кванторы существования, до квантора всеобщности на константы а1, а2,…

• внутренние кванторы существования, до которых есть(х1)(х2)…(хi)(xi+1),в М xi+1 заменить на f(x1,x2,…,xn).

Константы и функции, используемые для замены переменных квантора существования, называются скулемовскими функциями.

Результат – скулемовская стандартная форма.

Скулемовская форма, матрица которой является КНФ называется клазуальной формой.