Специальная математика. Соловьев А.Е. - 30 стр.

6. x P(x)  Q  x ( P(x)  Q )
7. x P(x)  Q  x ( P(x)  Q )
8. x P(x)  Q  x ( P(x)  Q )
9. x Q  Q
10. x Q  Q
11. xP(x)  xR(x)  x ( P(x)  R(x) )
12. xP(x)  xR(x)  x ( P(x)  R(x) )
13. xP(x)  xR(x)  x ( P(x)  R(x) )
14. x (P(x)  R(x) )  xP(x)  xR(x)
15. x P(x)  yP(y)                        (х, у - из одной предметной области)
16. x P(x)  y P(y)
17. xy P(x, y)  xy P(x, y)
18. xy P(x, y)  xy P(x, y)
19. xy P(x, y)  xy P(x, y)
                            2.2.2. Получение дизъюнктов

Важное замечание. Рассматриваем только замкнутые предикаты, то есть предикаты, не
содержащие свободных вхождений переменных.
В общем случае необходимо пройти три этапа:
1. Получить предваренную нормальную форму.
2. Произвести сколемизацию.
3. Получить дизъюнкты.

 Предваренная нормальная форма - такая форма представления предиката, когда все
кванторы вынесены в начало за скобки (кванторная приставка), а в скобках есть только
операции дизъюнкции, конъюнкции и отрицания. При этом символы отрицания, если
таковые имеются, стоят непосредственно перед символами предикатов.
Сколемизация (от фамилии математика - Skölem) позволяет получать запись замкнутого
предиката в форме без кванторов.
Избавляемся от кванторов существования:
1) Если левее нет кванторов общности, то
соответствующая переменная заменяется константой сколема;
2) Иначе переменная заменяется функцией сколема от переменных, на которые навешаны
   кванторы общности, стоящие левее данного квантора существования.
После чего кванторы общности просто отбрасываются.

Пример:
¬x ( yP(x, y)  ¬zR(z)  Q(x)  yM(x, y)) 
 ¬x ( y¬P(x, y)  zR(z)  Q(x)  yM(x, y) ) 
 x ( (yP(x, y)  z¬R(z))  (¬Q(x)  y¬M(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(ac, y)  ¬R(z))  (¬Q(ac)  ¬M(ac, fc(y, z)))
Каждая элементарная дизъюнкция в полученном выражении является дизъюнктом.




                                           — 30 —