Алгоритм Сколема

Шаг 1. Представить формулу F  в виде ПНФ, т.е.

       F=Âx1Âx2¼Âxn(M), где    ÂiÎ{«; $}Шаг 2. Найти в префиксе самый левый квантор существования:

a) если квантор находится на первом месте префикса, то вместо переменной, связанной кван­тором существования, подставить всюду предметную по­стоянную a, отличную от встречающихся предметных постоянных в матрице формулы, а квантор существования удалить;

б) если квантор находится не на первом месте префикса, т.е. «x1«x2¼»xi-1$xi .., то выбрать (i-1)-местный функциональный символ, отлич­ный от функциональных символов матрицы М и выполнить замену предметной переменной xi, связанной кванто­ром существования, на функцию f(x1;x2 ;¼ xi-1 ) и квантор существования удалить.

Шаг 3. Найти следующий справа квантор существования и перей­ти к исполнению шага 2, иначе конец.

Формулу ПНФ, полученную в результате введения сколемовской функции называют сколемовской стандартной формой формулы (ССФ).

Пример:

F=$x1″x2″x3$x4″x5$x6 ((P21 (x1; x2) ÚùP32(x3; x4; x5))&P  23(x4; x6)).

1) заменить предметную переменную x1 на постоянную a:

F=»x2″x3$x4″x5$x6 ((P21. (a; x2)ÚùP32.(x3; x4; x5))&P23 (x4; x6));

2) заменить предметную переменную x4 на функцию f2  1.(x2;x3):

F=»x2″x3″x5$x6 ((P21.(a; x2)ÚùP32 (x3; f 21(x2; x3); x5))&P23 (f21(x2; x3); x6));

4)    заменить предметную переменную x6 на функцию

 f32(x2; x3 ; x5 ):

 F=»x2″x3″x5((P21(a; x2)ÚùP32(x3; f21(x2; x3); x5))&

&P23(f21(x2; x3);f32(x2; x3 ; x5 ))).

К={(P21(a; x2)ÚùP32(x3; f21(x2; x3); x5)); P23(f21(x2; x3);f32(x2; x3 ; x5 ))}.

 

Логика - доступно для всех