Skolemizacja

Ten artykuł od 2012-02 wymaga zweryfikowania podanych informacji.

Należy podać wiarygodne źródła w formie przypisów bibliograficznych.
Część lub nawet wszystkie informacje w artykule mogą być nieprawdziwe. Jako pozbawione źródeł mogą zostać zakwestionowane i usunięte.
Sprawdź w źródłach: Encyklopedia PWN • Google Books • Google Scholar • Federacja Bibliotek Cyfrowych • BazHum • BazTech • RCIN • Internet Archive (texts / inlibrary)
Dokładniejsze informacje o tym, co należy poprawić, być może znajdują się w dyskusji tego artykułu.
Po wyeliminowaniu niedoskonałości należy usunąć szablon {{Dopracować}} z tego artykułu.

Skolemizacja to metoda pozwalająca na opuszczanie kwantyfikatorów egzystencjalnych lub też wszystkich kwantyfikatorów w formułach rachunku predykatów pierwszego rzędu zapisanych w formie preneksowej. Jej twórcą był norweski matematyk Thoralf Skolem.

Każdy kwantyfikator egzystencjalny zastępujemy świeżym symbolem funkcyjnym, którego argumenty to wszystkie dotychczas wprowadzone przez kwantyfikatory ogólne zmienne oraz zmienne wolne, jeśli jakieś są.

Po dokonaniu skolemizacji zostajemy z formułą mającą na początku same kwantyfikatory ogólne. Można je opuścić i założyć, że zmienne przez nie wprowadzane to po prostu zmienne wolne.

${\displaystyle \forall x.\exists y.\forall w.\exists z.R(x,y)\lor \neg R(x,z)\lor Q(y,w,z)}$

Skolemizacja tej formuły przebiega jak następuje:

${\displaystyle \exists y.\forall w.\exists z.R(x,y)\lor \neg R(x,z)\lor Q(y,w,z)}$ (${\displaystyle x}$ - zmienna wolna)

${\displaystyle \forall w.\exists z.R(x,y(x))\lor \neg R(x,z)\lor Q(y(x),w,z)}$ (${\displaystyle y}$ - funkcja jednoargumentowa)

${\displaystyle \exists z.R(x,y(x))\lor \neg R(x,z)\lor Q(y(x),w,z)}$ (${\displaystyle w}$ - zmienna wolna)

${\displaystyle R(x,y(x))\lor \neg R(x,z(x,w))\lor Q(y(x),w,z(x,w))}$ (${\displaystyle z}$ - funkcja dwuargumentowa).

Jeśli formuła jest sprzeczna/spełnialna, to taką samą własność ma jej postać zeskolemizowana.

Formuła X jest spełnialna wtedy i tylko wtedy, gdy spełnialna jest formuła Skol(X). Formuła X jest więc równoważna formule Skol(X) w sensie spełnialności, co nie oznacza równoważności tych formuł w sensie semantycznym.