Получение дизъюнктов

Важное замечание. Рассматриваем только замкнутые предикаты, то естьпредикаты, не содержащие свободных вхождений переменных.

В общем случае необходимо пройти три этапа:

1. Получить предваренную нормальную форму.

2. Произвести сколемизацию.

3. Получить дизъюнкты.

Предваренная нормальная форма - такая форма представления предиката, когда все кванторы вынесены в начало за скобки (кванторная приставка), а в скобках есть только операции дизъюнкции, конъюнкции и отрицания. При этом символы отрицания, если таковые имеются, стоят непосредственно перед символами предикатов.

Сколемизация (от фамилии математика - Skölem)позволяет получать запись замкнутого предиката в форме без кванторов.

Избавляемся от кванторов существования:

1) Если левее нет кванторов общности, то

соответствующая переменная заменяется константой сколема;

2) Иначе переменная заменяется функцией сколема от переменных, на которые навешаны кванторы общности, стоящие левее данного квантора существования.

После чего кванторы общности просто отбрасываются.

Пример:

"x ("yP(x, y) Ú $zR(z) ® Q(x) & "yM(x, y)) º

º "x ($yP(x, y) & $zR(z) Ú Q(x) & "yM(x, y)) º

º $x (("yP(x, y) Ú "zR(z)) & (Q(x) Ú $yM(x, y))) º

º $x ("yz (P(x, y) Ú R(z)) & $y(Q(x) Ú M(x, y))) º

º $x"y"z$h ((P(x, y) Ú R(z)) & (Q(x) Ú M(x, h))) º

º (P(a^c, y) Ú R(z)) & (Q(a^c) Ú M(a^c, f^c(y, z)))

Каждая элементарная дизъюнкция в полученном выражении является дизъюнктом.