Главная | Обратная связь

Исчисление предикатов.

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

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

В результате этих алгебраических преобразований может быть получена формула вида: Â_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₅ ))}.

 

Унификация

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

Пусть задано множество дизъюнктов. Каждый дизъюнкт составлен из литералов.

Пример. Пусть имеем следующее множество дизъюнктов:

дизъюнкт дизъюнкт

_____.А.___________ А

S = (P(x, f(y), b) ÚP(x, f(a), b), ØP(c, f(a), b)}

литерал литерал литерал

Термы литерала могут быть переменными, постоянными или выражениями, состоящим из функциональных букв и термов. Например, для литерала Р(х, f(y), b) имеем, что х - переменная, f(y) - сложный терм, b-постоянная.

Подстановочный частный случай литерала получается при подстановке в литералы термов вместо переменных. Пусть имеем литерал P(x, f(y), b). Его частными случаями будут:

P₁= P(z,f(w), b),

P₂ = P(x, f(a), b),

P₃ = P(g(z), f(a), b),

Р₄ = Р(с, f(а), b) - константный частный случай литерала или атом, т.к. нет переменных.

Подстановки, примененные в рассматриваемом примере, можно обозначить следующим образом:

_q1 = {z/x, w/y}, здесь z подставляется вместо х, а w вместо у;

q₂ = {а/у};

qз = {g(z)/x, а/у};

q₄ = {с/х, а/у}. Применение подстановки в к литералу Р обозначаем Р_q. Тогда имеем

Pq₁=Pj, Рq_з=Р₃,

рq₂=р₂, рq₄=р₄

Если q - подстановка и она применяется к каждому из литералов L_iто полученные частные случаи обозначаются через {L_i}_q.

Последовательное применение двух подстановок q₁ и q₂ дает новую подстановку q₃, которую обозначаем q₃ = q1 ° q₂.

Множество {L_i} литералов называется унифицируемым, если существует такая подстановка в, что (L₁) _q= (L₂) _q= ... = (L_n) _q

В этом случае подстановку вназывают унификатором для {L_i}.

Пусть имеем множество литералов {Р(х, f(y), b), Р(х, f(b), b)}, где L₁ = Р(х, f(y), b), L₂ = P(x, f(b), b). Подстановка q = {a/x, b/y} является, очевидно, унификатором для этого множества литералов.

Унификатор s для множества выражений {E₁,E₂,...,E_k} называется наиболее общим унификатором тогда и только тогда, когда для каждого унификатора q для этого множества существует такая подстановка l, что q =s°l.

Существует алгоритм, называемый алгоритмом унификации, который приводит к наиболее общему унификатору для унифицируемого множества литералов {L_i} и сообщает о неудаче, если это множество не унифицируемо.

Алгоритм унификации: Алгоритм начинает работу с пустой подстановки и шаг за шагом строит наиболее общий унификатор, если таковой существует. Предположим, что на k-ом шаге получена подстановка q_k. Если все литералы из {L_i} в результате становятся идентичными, то q = q_к и есть наиболее общий унификатор. В противном случае каждый из литералов в {Li}q_k рассматривается как цепочка символов и выделяется

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

{P(a, f(a, g(z)), h(x)), P(a, f(a, u), g(w))}

­_______________­

Затем конструируется множество рассогласования, содержащее правильно построенные выражения из каждого литерала, который начинается с этой позиции (правильно построенное выражение представляет собой либо терм, либо литерал). Так для рассмотренного примера множеством рассогласования будет

{g(z), u}.

Далее модифицируем (если можно) подстановку θ_k, чтобы сделать равным два элемента из множества рассогласования. Это можно сделать только тогда, когда множество рассогласования содержит переменную, которую можно положить равной одному из его термов. Если множество рассогласования не содержит переменных, то множество {L_i} унифицировать нельзя.