шпаргалка

Скулемовска стандартная форма

[ Назад ]

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



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

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



функций.

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

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

(Q1x1)…(Qnxn)M

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

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

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

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

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



КАТЕГОРИИ:

Network | английский | архитектура эвм | астрономия | аудит | биология | вычислительная математика | география | Гражданское право | демография | дискретная математика | законодательство | история | квантовая физика | компиляторы | КСЕ - Концепция современного естествознания | культурология | линейная алгебра | литература | математическая статистика | математический анализ | Международный стандарт финансовой отчетности МСФО | менеджмент | метрология | механика | немецкий | неорганическая химия | ОБЖ | общая физика | операционные системы | оптимизация в сапр | органическая химия | педагогика | политология | правоведение | прочие дисциплины | психология (методы) | радиоэлектроника | религия | русский | сертификация | сопромат | социология | теория вероятностей | управление в технических системах | физкультура | философия | фотография | французский | школьная математика | экология | экономика | экономика (словарь) | язык Assembler | язык Basic, VB | язык Pascal | язык Си, Си++ |