Обобщающий пример

Приведение матрицы к КНФ

Исключение кванторов общности

Получение предваренной формы - важный этап в деле преобразования исходной формулы ИП. Дальнейшая работа будет проводиться с матрицей, все переменные которой относятся к тому или иному квантору общности. Роль цепочки кванторов (префикса) в данном случае - в простом напоминании об этом факте. К тому же порядок кванторов общности роли не играет. Если все это принять во внимание, то префикс вообще можно убрать и предположить по соглашению, что все переменные относятся к своим кванторам общности. Остается одна матрица.

Если теперь рассматривать матрицу как логическое выражение, связывающее посредством пропозициональных связок некоторое количество литералов, то процесс приведения любой матрицы к конъюнктивной нормальной форме будет мало чем отличаться от такого же процесса в рамках исчисления высказываний. Процесс этот всегда возможен, и конечный итог известен: матрица будет представлена в виде конъюнкции дизъюнктов (каузальная форма). Дизъюнкт, напомним, в исчислении предикатов называется предложением. Знаки конъюнкции можно опустить, и все множество полученных предложений представить в виде столбца, рассматривая каждое из них как некую исходную гипотезу (как это мы делали с дизъюнктами в процессе логического вывода в ИВ).

Привести заданное выражение к системе предложений.

x { y [ P (x,y) xQ (x, h (y))] x yR (a,y,x)}.

Освобождаемся от импликаций.

x { y [(x,y) xQ (x,h (y))] x yR (a,y,x)}.

Переносим и снимаем отрицания (согласно (6.6) и др. правилам).

x { y

x { y .

Окончательно:

x { y .

Проводим стандартизацию: каждый квантор должен иметь свою переменную. С этой целью переименуем в средней формуле (для ) x на u, в последней формуле - x на z, y на w:

x { y }.

Исключаем кванторы существования. Заметим, что квантор y находится в сфере действия x и распространяется на квадратные скобки, а квантор w - в сфере действия x и z, соответственно вводим функции Сколема.

x { }.

Выносим кванторы общности влево, за скобки, образуем предваренную форму.

x u z { }.

Опускаем кванторы общности, полученную матрицу приводим к КНФ.

=
(раскрывая конъюнкцию по дизъюнкции)
= (P (x,f (x)) R (a,g (x,z) ,z)) ( (u,h (f (x))) R (a,g (x,z) ,z))

Окончательно получаем систему предложений:

1. P (x,f (x)) R (a,g (x,z) ,z)),

2. `Q (u,h (f(x))) R (a,g (x,z) ,z)).

Хорошо, что мы научились приводить выражение в предваренной форме к системе предложений. Но для того, чтобы идти дальше и проводить с ними процесс резолюции, нам необходимо уметь находить контрарные литералы, что при участии многоместных предикатов с различными переменными становится делом весьма непростым. Пусть, например, имеются предложения:

1. Q (u) P (A),

2.`Q (w) P (w),

3.`Q (x) `P (x)

4. Q (y) `P (y).

Судя по предикатным символам, здесь вполне возможна резолюция. Но различные переменные не дают нам делать это непосредственно. Необходимо делать подстановки.

Дата добавления: 2014-01-20