![]() |
Главная Случайная страница Контакты | Мы поможем в написании вашей работы! | |
|
Шаг 1. Представить формулу F в виде ПНФ, т. е.
F = x 1 x 2¼Â xn (M), где ÂiÎ{"; $}.
Шаг 2. Найти в префиксе самый левый квантор существования:
a) если квантор находится на первом месте префикса, то вместо переменной, связанной квантором существования, подставить всюду предметную постоянную a, отличную от встречающихся предметных постоянных в матрице формулы, а квантор существования удалить;
б) если квантор находится не на первом месте префикса, т. е. " x 1" x 2¼" xi -1 $ xi.., то выбрать (i –1)-местный функциональный символ, отличный от функциональных символов матрицы М и выполнить замену предметной переменной xi, связанной квантором существования, на функцию f (x 1, x 2,¼, xi -1) и квантор существования удалить.
Шаг 3. Найти следующий справа квантор существования и перейти шагу 2, иначе конец.
Формулу ПНФ, полученную в результате введения сколемовской функции называют сколемовской стандартной формой формулы (ССФ).
Пример.
1) заменить предметную переменную x 1 на постоянную a:
2) заменить предметную переменную x 4 на функцию :
3) заменить предметную переменную x 6 на функцию
:
Задание 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)) |
Дата публикования: 2015-03-26; Прочитано: 484 | Нарушение авторского права страницы | Мы поможем в написании вашей работы!