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

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

F = x ₁ x ₂¼Â x_n (M), где Â_iÎ{"; $}.

Шаг 2. Найти в префиксе самый левый квантор существования:

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

б) если квантор находится не на первом месте префикса, т. е. " x ₁" x ₂¼" x_{i -1} $ x_i.., то выбрать (i –1)-местный функциональный символ, отлич­ный от функциональных символов матрицы М и выполнить замену предметной переменной x_i, связанной кванто­ром существования, на функцию f (x ₁, x ₂,¼, x_{i -1}) и квантор существования удалить.

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

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

Пример.

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

2) заменить предметную переменную x ₄ на функцию :

3) заменить предметную переменную x ₆ на функцию

:

Задание 5

Найти формулы ПНФ и ССФ.

	Формула
	"x(A(x)®ù B(y))®$y(B(y)®ù A(x))
	"x(ù A(x)®$y(ù C(y)))®"x((D(x)®A(x))
	"x(A(x)®$z(B(z)))®$y(ù A(x)Úù C(y)ÚC(y) ÙB(x))
	"x(A(x)®$y(B(y)))®$x(ù A(x)®ù B(y))
	"x(A(x)®B(y)) Ù"y(A(x)®(B(y)®C(z))®$z(A(x)®C(z))
	"x(A(x)®$y(B(y)®C(z)))®"z(A(x) ÙB(y)®C(z))
	"x(A(x)®B(z)) Ù"y(C(y)®A(x))®$z(C(y)®B(z))
	"x(A(x)®B(y))®"y((C(y)ÚA(x))®(C(y)Ú$y(B(y)))
	"x(B(x))®$y(A(y)®B(x))
	"x(A(x)®B(x))®("y(C(y)®A(x))®$z(C(z)®B(x)))
	"x(A(x)®$z(B(y)®C(z)))®"y(B(y)®(A(x)®C(z)))
	("x(A(x))®$x(B(x)))®"z((B(x)®C(z))®(A(x)®C(z)))
	($x(ù A(x))®"x(ù B(x)))®(ù B(x)ÚA(x))
	("x(A(x)))®("x(B(x)))®$y(C(y) ÙA(x)®C(y) ÙB(x))
	"x(ù A(x)®$y(B(y)))®(ù B(y)®A(x))
	("x(B(x))®$x(A(x))) Ù$y((A(x)®C(y))®(ù C(y) ÙB(x)))
	"x(ù A(x)®$y(B(y)))®(B(y)ÚA(x))
	"x(ù A(x)®$y(ù B(y)))®(B(y)®A(x))
	"x(A(x)®B(x)) Ù$y(B(x)®C(y) Ù$z(C(y)®D(z)))
	("x(A(x)®B(x)) Ù"z(C(z)®A(x)))®$y(C(z)®B(y))