Студопедия Главная Случайная страница Обратная связь

Разделы: Автомобили Астрономия Биология География Дом и сад Другие языки Другое Информатика История Культура Литература Логика Математика Медицина Металлургия Механика Образование Охрана труда Педагогика Политика Право Психология Религия Риторика Социология Спорт Строительство Технология Туризм Физика Философия Финансы Химия Черчение Экология Экономика Электроника

Сколемовская нормальная форма (СНФ)




Опр. Формула G имеет СНФ, если G = ( x)…( xn) H,

где формула Н не содержит кванторов и имеет КНФ (конъюктивную нормальную форму).

Теорема: Для всякой формулы F существует формула G, имеющая СНФ и одновременно выполнимая (или невыполнимая) с F.

Алгоритм приведения к СНФ:

1. Привод к ПНФ

2. Привести матрицу Н к ПНФ

3. Исключить кванторы

1) Если левее квантора (существования) нет квантора (всеобщности), то переменную, связанную этим квантором заменяем не встречающейся в формуле константой, а квантификацию отбрасываем. х(Р(х)) Р(а)

2) Если левее квантора находятся n кванторов , то переменная, связанная этим квантором заменяется на n-местный функциональный символ, зависящий от переменных, связанных этими кванторами , а сама квантификация отбрасывается.

Ех: после 2го шага имеем:

F = ( x) ( y) ( z) ( u) ( v) H (x, y, z, u, v)

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

Тогда в формуле Н заменим:

х – на с

z – на f(y)

v – на g(y,u)

F = ( x) ( y) ( z) ( u) ( v) H (x, y, z, u, v)

тогда G = ( y) ( u) H (c, y, f(y), u, g(y, u))

Ех: привести функцию к СНФ

F = ( x) ( y) [P(x, y) ( z) (Q(x, z)) R(y))]

Применяя законы:

A B A B;

(A Q x B) Q x (A B), если A не содержит x, получаем формулу:

F1 = ( x) ( y) ( z) [ P(x, y) (Q(x, z) R(y))]

которая имеет ПНФ

приводим к КНФ

F2 = ( x) ( y) ( z) [( P(x, y) Q(x, z)) ( P(x, y) R(y))]

сделаем подстановку x = a, z = f(y), получим

G = ( y) [ P(a, y) Q(a, f(y))) ( P(a, y) R(y))]







Дата добавления: 2015-04-19; просмотров: 1401. Нарушение авторских прав

codlug.info - Студопедия - 2014-2017 год . (0.312 сек.) русская версия | украинская версия