Главная страница | Контакты | Случайная страница Автомобили Астрономия Биология География Дом и сад Другие языки Другое Информатика История Культура Литература Логика Математика Медицина Металлургия Механика Образование Охрана труда Педагогика Политика Право Психология Религия Риторика Социология Спорт Строительство Технология Туризм Физика Философия Финансы Химия Черчение Экология Экономика Электроника

Предваренная нормальная форма. Сколемовская стандартная форма.

Для облегчения анализа сложных суждений формулы алгебры предикатов рекомендуется приводить к нормальной форме. Если в алгебре высказываний приняты две нормальные формы (ДНФ - дизъюнктивная и КНФ -конъюнктивная), то в алгебре предикатов - одна предваренная нормальная форма (ПНФ), суть которой сводится к разделению формулы на две части: кванторную и безкванторную. Для этого все кванторы формулы выносят влево, используя законы и правила алгебры предикатов.

В результате этих алгебраических преобразований может быть получена формула вида: Â_x1 Â_x2 ¼Â_xn(M), где ÂÎ{"; $}, а М – матрица формулы. Кванторную часть формулы Â_x1 Â_x2 ¼Â_xnиногда называют префиксом ПНФ.

В последующем матрицу формулы преобразуют к виду КНФ, что облегчает механизм по принципу резолюции.

Пример:

F=$_x"_y((P²₁.(х; y)ÚùP₂.(х))&P₃(y)) формула, приведенная к ПНФ; F="_x(P²₁.(х; y)Ú$_x(P₂ (х))&$_y(P₃ (y)) формула, неприведенная к ПНФ.

"_x(P₁.(х)) &"_x(P₂(x))="_x(P₁.(х) &P₂(x)) слева от знака равенства формула, неприведенная к ПНФ, а справа, равносильная ей формула, но приведенная к ПНФ.

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

Шаг 1. Исключить всюду логические связки «и ® по правилам:

(F₁«F₂)=(F₁®F₂)& (F₂®F₁)=(ùF₁ÚF₂)&(ùF₂ÚF₁);

(F₁®F₂)=(ù F₁ÚF₂);

Шаг 2. Продвинуть отрицание до элементарной формулы по правилам:

ù"x(F)=$x(ùF); ù(F₁ÚF₂)=(ùF₁&ùF₂);

ù$x(F)="x(ùF);. ù(F₁&F₂)=(ùF₁ÚùF₂);

Шаг 3. Переименовать связанные переменные по правилу:

“ найти самое левое вхождение предметной переменной такое, что это вхождение связано некоторым квантором, но существует еще одно вхождение этой же переменной; затем сделать замену связанного вхождения на вхождение новой переменной “, операцию повторять пока возможна замена связанных переменных;

Шаг 4. Вынести кванторы влево по законам алгебры логики.

Шаг 5. Преобразовать бескванторную матрицу к виду КНФ. Алгоритм приведения матрицы формулы к виду КНФ приведен в алгебре высказываний.

Пример: F=("_x(P₁ (х)®"_y(P₂ (y)®P₃ (z))))&(ù"_y(P²₄ (x; y)®P₅.(z))).

Привести формулу к виду ПНФ.

l) удалить логические связки “®”:

F=("_x(ùP₁ (х)Ú"_y(ù P₂ (y)ÚP₃ (z))))&(ù"_y(ù P²₄ (x; y)ÚP₅.(z)));

2) применить закон де Моргана ù "_x(F(x))=$_x( ù F(x)):

F=("_x(ùP₁.(х)Ú"_y(ù P₂ (y)ÚP₃ (z))))&($_y(ù(ù P²₄ (x; y)ÚP₅.(z)));

3) применить закон де Моргана ù(F₁ÚF₂)=(ùF₁&ùF₂):

F="_x(ùP₁.(х)Ú"_y(ù P₂ (y)ÚP₃ (z)))&($_y(P²₄ (x; y)&(ùP₅.(z))));

4) переименовать связанную переменную x=w:

F="_w(ùP₁ (w)Ú"_y(ù P₂ (y)ÚP₃ (z)))&($_y(P²₄ (x; y)&(ù P₅.(z))));

5) переименовать связанную переменную y=v:

F="_w(ùP₁ (w)Ú"_v(ùP₂ (v)ÚP₃ (z)))&($_y(P²₄ (x; y)&(ùP₅.(z))));

6) вынести квантор "_v влево:

F="_w"_v(ùP₁ (w)ÚùP₂ (v)ÚP₃ (z))&($_y(P²₄ (x; y)&(ùP₅.(z))));

7) вынести квантор $_y влево:

F="_w"_v$_y(ùP₁ (w)ÚùP₂ (v)ÚP₃ (z))&P²₄ (x; y)&ùP₅.(z).

Матрица ПНФ содержит три элементарных дизъюнкта:

K={(ùP₁ (w)ÚùP₂ (v)ÚP₃ (z)); P₄ (x; y); ùP₅.(z)}.

Пример: F = "_x(P₁ (х)«$_x(P₂ (x)))®"_y(P₃.(y)).

Привести формулу к виду ПНФ.

1) удалить логические связки “«”:

F="_x((P₁ (х)®$_x(P₂ (x)))&($_x(P₂ (х))®P₁ (x)))®"_y(P₃.(y));

2) удалить логические связки “®”:

F=ù("_x((ùP₁.(х)Ú$_x(P₂ (x)))&(ù$_x(P₂.(х))ÚP₁ (x)))Ú"_y(P₃.(y));

3) применить закон ù"x(F(x))=$x(ùF(x)):

F=$_x(ù((ùP₁.(х)Ú$_x(P₂ (x)))&(ù$_x(P₂ (х))ÚP₁ (x))))Ú"_y(P₃.(y));

4) применить закон де Моргана ù(F₁&F₂)=(ùF₁ÚùF₂):

F=$_x((ù(ùP₁ (х)Ú$_x(P₂ (x)))Ú(ù(ù$_x(P₂.(х))ÚP₁ (x))))Ú"_y(P₃.(y));

5) применить закон де Моргана ù(F₁ÚF₂)=(ùF₁&ùF₂):

F=$_x((P₁ (х)&(ù$_x(P₂ (x))))Ú($_x(P₂ (х))&(ùP₁ (x))))Ú"_y(P₃.(y));

6) применить закон ù$_x(F(x))= "_x (ùF(x)):

F=$_x((P₁ (х)&"_x(ùP₂.(x)))Ú($_x(P₂ (х))&(ùP₁ (x))))Ú"_y(P₃.(y));

7) переименовать связанную переменную x=z:

F=$_z((P₁.(z)&"_x(ù P₂ (x)))Ú($_x(P₂.(х))&(ùP₁.(z))))Ú"_y(P₃.(y));

8) переименовать связанную переменную x=w:

F=$_z(P₁ (z)&"_w(ùP₂ (w))Ú$_x(P₂ (х)&ùP₁ (z)))Ú"_y(P₃.(y));

9) вынести квантор "_w, $_x и "_y влево:

F=$_z"_w$_x"_y(P₁ (z)&ùP₂ (w)ÚP₂ (х)&ùP₁ (z)ÚP₃.(y));

10) преобразовать матрицу к виду КНФ:

F=$_z"_w$_x"_y((P₁ (z)ÚP₂ (х)ÚP₃.(y))&(ùP₂ (w)ÚP₂ (х)ÚP₃.(y))& (ùP₂ (w)ÚùP₁ (z)ÚP₃.(y))).

Матрица ПНФ содержит три элементарных дизъюнкта:

K={(P₁ (z)ÚP₂ (х)ÚP₃.(y)); (ùP₂ (w)ÚP₂ (х)ÚP₃.(y)); (ùP₂ (w)ÚùP₁ (z)ÚP₃.(y))}.

Пример: F="_x$_y(P²₁ (х; y))&ù($_x"_y(P²₂(x; y))).

Привести формулу к виду ПНФ.

1) применить закон ù$_x(F(x))="_x(ùF(x)):

F="_x$_y(P²₁(х; y))&("_xù("_y(P22(x; y))));

2) применить закон ù"_x(F(x))= $_x(ùF(x)):

F="_x$_y(P²₁(х; y))&("_x$_y(ù(P²₂(x; y))));

1) вынести квантор "_x по закону дистрибутивности:

F="_x($_y(P²₁(х; y))&$_y(ù(P²₂(x; y))));

4) переименовать связанную переменную y=v:

F="_x($_z(P²₁(х; z))&$_y(ù(P²₂(x; y))));

5) вынести кванторs $_z и $_y влево:

"_x$_z$_y(P²₁(х; z)&ùP²₂(x; y)).

Матрица ПНФ содержит два элементарных дизъюнкта:

K={P²₁(х; z); ùP²₂(x; y)}.

Пример: M=P₁(z)&ùP₂(w)ÚP₂(х)&ùP₁.(z)ÚP₃.(y);

1) по закону дистрибутивности:

M=P₁.(z)&ùP₂ (w)Ú(P₂ (х)ÚP₃.(y))&(ù P₁ (z)Ú(P₃.(y));

2) по закону дистрибутивности:

M=(P₁.(z)&ùP₂.(w)ÚP₂.(х)ÚP₃.(y))&(P₁.(z)&ùP₂.(w)ÚùP₁.(z)Ú P₃.(y));

3) по закону дистрибутивности:

M =(P₁.(z)ÚP₂.(x)ÚP₃.(y))&(ù P₂.(w)ÚP₂.(x)ÚP₃.(y))&

(P₁.(z)ÚùP₁.(z)ÚP₃.(y))&(ùP₂.(w)ÚùP₁.(z)ÚP₃.(y));

4) по закону исключенного третьего:

M=(P₁.(z)ÚP₂.(x)ÚP₃.(y))&(ùP₂.(w)ÚP₂.(x)ÚP₃.(y))&

&(ù P₂.(w)ÚùP₁.(z)ÚP₃.(y)).

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

K={(P₁.(z)ÚP₂.(x)ÚP₃.(y)); (ùP₂.(w)ÚP₂.(x)ÚP₃.(y)); (ù P₂.(w)ÚùP₁.(z)ÚP₃.(y))}.

Дизъюнкты матрицы содержат контрарные атомы P₁.(z) и ùP₁.(z), P₂.(x) и ùP₂.(w), свободные переменные которых могут быть одинаковыми или разными.

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

Наличие разноименных кванторов усложняет вывод заключения. Поэтому рассмотрим класс формул, содержащих только кванторы всеобщности. Формула F называется " - формулой, если она представлена в ПНФ и содержит только кванторы всеобщности, т.е.

F = " _x1 " _x2 ¼ " _xn (M).

Для устранения кванторов существования из префикса формулы разработан алгоритм Сколема, вводящий сколемовскую функцию для связывания предметной переменной квантора существования с другими предметными переменными.

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

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

F =Âx₁Âx₂¼Âx_n(M), где Â_iÎ{"; $}Шаг 2. Найти в префиксе самый левый квантор существования:

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

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

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

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

Пример:

F=$_x1"_x2"_x3$_x4"_x5$_x6 ((P²₁ (x₁; x₂) ÚùP³₂(x₃; x₄; x₅))&P ²₃(x₄; x₆)).

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

F="_x2"_x3$_x4"_x5$_x6 ((P²₁. (a; x₂)ÚùP³₂.(x₃; x₄; x₅))&P²₃ (x₄; x₆));

2) заменить предметную переменную x₄ на функцию f² ₁.(x₂;x₃):

F="_x2"_x3"_x5$_x6 ((P²₁.(a; x₂)ÚùP³₂ (x₃; f ²₁(x₂; x₃); x₅))&P²₃ (f²₁(x₂; x₃); x₆));

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

f³₂(x₂; x3; x₅):

F="_x2"_x3"_x5((P²₁(a; x₂)ÚùP³₂(x₃; f²₁(x₂; x₃); x₅))&

&P²₃(f²₁(x₂; x₃);f³₂(x₂; x₃; x₅))).

К={(P²₁(a; x₂)ÚùP³₂(x₃; f²₁(x₂; x₃); x₅)); P²₃(f²₁(x₂; x₃);f³₂(x₂; x₃; x₅))}.