Лекция: Получение дизъюнктов

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

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

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)) ) º