293017403

Etap 5 - skolemizacja

Usunięcie kwantyfikatora istnienia.

Wprowadza się nowe symbole reprezentujące stałe, w miejsce zmiennych spod usuwanych kwantyfikatorów.

Przypadek pierwszy:

Przed: 3x: President(x)

P°^;    President(sl)

Przypadek z wielkim kwantyfikatorem (S2(x) -funkcja od zmiennej x):

Przed: Vx: Ety: father(x,y)

Po:    Vx:father(x,S2(x))

31

Etap 6 - usunięcie wielkiego kwantyfikatora

Opuszcza się w wyrażeniu kwantyfikatory wielkie i nie zmienia to znaczenia całego wyrażenia.

Przed:

Vjt: father(x, mark)

-»Po:

father(x, marek)