Алгоритм приведения к предваренной нормальной форме
Шаг 1. Используя законы 21 и 20, исключить эквиваленцию и импликацию.
Шаг 2. Занести отрицание к атомарным формулам, пользуясь законами 17-19 и 26-27.
Шаг 3. С помощью законов 22-23, 28-31 вынести кванторы вперед, используя при необходимости переименование связанных переменных (законы 32-33).
Рассмотрим пример. Пусть
F=("x)P(x)®($y)("z)(P(y)&Q(y,z)).
Выполнив шаг 1 (с помощью закона 20), получим формулу
F1=Ø("x)P(x)Ú($y)("z)(P(y)&Q(y,z)).
С помощью закона 26 перейдем к формуле
F2=($x)ØP(x)Ú($y)("z)(P(y)&Q(y,z)).
Тем самым, шаг 2 также выполнен. Применим закон 30 слева направо Q1=$, Q2=$, u=y, получим формулу
F3=($x)($y)[ØP(x)Ú("z)(P(y)ÚQ(y,z))].
(Пользуемся тем, что ØP(x) не содержит y, а ("z)(P(y)&Q(Y,z)) не содержит х. Так как формула ØP(x) не содержит z, то применение закона 26 слева направо дает формулу
F4=($x)($y)("z)[ØP(x)ÚÚ(P(y)&Q(y,z))].
Это и есть искомая формула, имеющая ПНФ и равносильная формуле F.
В предыдущем примере выполнение шага 3 можно организовать по-другому. В формуле F2 связанную переменную y заменим на переменную х (закон 33), получим формулу
F3/=($x)ØP(x)Ú($x)("z)(P(x)&Q(x,z)).
Используя закон 23, перейдем к формуле
F4/=($x)[ØP(x)Ú("z)(P(x)&Q(x,z))].
Затем, как и в предыдущем абзаце, с помощью закона 28 вынесем квантор по z за квадратную скобку. Получим формулу
F5/=($z)("z)[ØP(x)Ú(P(x)&Q(x,z)].
Формула F5/, как и формула F4, имеет предваренную нормальную форму и равносильна формуле F. В некоторых ситуациях формула F5/ предпочтительнее формулы F4, поскольку содержит меньше кванторов. (Кстати, бескванторную часть формулы F5/ можно упростить).
Дата добавления: 2015-09-27 | Просмотры: 761 | Нарушение авторских прав
|