Skolemizacja

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.

Przykład

$\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:

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

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

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

$R(x,y(x))\lor \neg R(x,z(x,w))\lor Q(y(x),w,z(x,w))$ ($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.