Добавил:
Upload Опубликованный материал нарушает ваши авторские права? Сообщите нам.
Вуз: Предмет: Файл:
UchebnoePosobie.doc
Скачиваний:
72
Добавлен:
11.11.2019
Размер:
6.36 Mб
Скачать

4.2.1.3 Сколемовская стандартная форма формулы

Наличие разноимен­ных кванторов усложняет вывод заключения. Для устранения кванторов существования в ПНФ и представления ее в виде F = x1x2 xn (M) разработан алгоритм Сколема, вводящий сколемовскую функцию для связывания предметной переменной квантора существования с предметными переменными кванторов всеобщности.

Алгоритм приведения формулы к виду ССФ:

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

F=x1x2xn(M), где i{; };

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

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

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

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

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

Пример: F=x1x2x3x4x5x6((P1(x1, x2)P2(x3, x4, x5))P3(x4, x6)).

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

F=x2x3x4x5x6 ((P1. (a, x2)P2.(x3, x4, x5))P3 (x4, x6));

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

F=x2x3x5x6 ((P1.(a, x2)P2 (x3, f1(x2, x3), x5))P3 (f1(x2, x3), x6));

  • заменить предметную переменную x6 на функцию f2(x2, x3, x5):

F=x2x3x5((P1(a, x2)P2(x3, f1(x2, x3), x5))P3(f1(x2, x3),

f2(x2, x3, x5))).

Множество дизъюнктов матрицы:

К={(P1(a, x2)P2(x3, f1(x2, x3), x5)); P3(f1(x2, x3), f2(x2, x3, x5))}.

Пример: F=zwxy((P1 z)P2 (х)P3.(y))(P2 (w)P2 (х)P3.(y)) (P2 (w)P1 (z)P3.(y))).

  • заменить предметную переменную z на постоянную a и удалить квантор z:

F=wxy((P1 (a)P2 (х)P3.(y))(P2 (w)P2 (х)P3.(y)) (P2 (w)P1 (a)P3.(y))).

  • заменить предметную переменную x на функцию f(w) и удалить квантор x:

F=wy((P1 (a)P2 (f(w))P3.(y))(P2 (w)P2 (f(w))P3.(y)) (P2 (w)

P1 (a)P3.(y))).

  • заменить предметную переменную x6 на функцию f2(x2, x3, x5):

F=x2x3x5((P1(a, x2)P2(x3, f1(x2, x3), x5))P3(f1(x2, x3),

f2(x2, x3, x5))).

Множество дизъюнктов матрицы:

К={(P1(a, x2)P2(x3, f1(x2, x3), x5)); P3(f1(x2, x3), f2(x2, x3, x5))}.

Пример: F=zwxy((P1 z)P2 (х)P3.(y))(P2 (w)P2 (х)P3.(y)) (P2 (w)P1 (z)P3.(y))).

  • заменить предметную переменную z на постоянную a и удалить квантор z:

F=wxy((P1 (a)P2 (х)P3.(y))(P2 (w)P2 (х)P3.(y)) (P2 (w)P1 (a)P3.(y))).

  • заменить предметную переменную x на функцию f(w) и удалить квантор x:

F=wy((P1 (a)P2 (f(w))P3.(y))(P2 (w)P2 (f(w))P3.(y)) (P2 (w)

P1 (a)P3.(y))).

Соседние файлы в предмете [НЕСОРТИРОВАННОЕ]