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

Практика по преобразованию предикатных формул к ПНФ

1. Преобразовать формулу:

¬∃_x1∀_x2(P₁(х₁)→∀_x3(P₂(х₁,x₃)∨P₃(x₂,x₃))).

Решение:

1) выполним операцию отрицания:

∀_x1¬∀_x2(P₁(х₁)→∀_x3 (P₂(х₁,x₃)∨P₃(x₂,x₃)))=∀_x1∃_x2(¬(P₁(х₁)→∀_x3(P₂(х₁,x₃)∨P₃(x₂,x₃))))

2) удалим логическую связку →:

∀_x1∃_x2¬(¬P₁(х₁)∨∀_x3(P₂(х₁,x₃)∨P₃(x₂,x₃)))

3) выполним операцию отрицания:

∀_x1∃_x2(P₁(х₁)&¬∀_x3(P₂(х₁,x₃)∨P₃(x₂,x₃)))=∀_x1∃_x2(P₁(х₁)&∃_x3(¬(P₂(х₁,x₃)∨P₃(x₂,x₃))))=

∀_x1∃_x2(P₁(х₁)&∃_x3(¬P₂(х₁,x₃)&¬P₃(x₂,x₃)))

4) перенесем квантор $_x3 влево:

∀_x1∃_x2∃_x3(P₁(х₁)&¬P₂(х₁,x₃)&¬P₃(x₂,x₃)).

2. Преобразовать формулу:

(∀_x(P₁(х)→∀_y(P₂(y)→P₃(z))))&(¬∀_y(P₄(x,y)→P₅(z))).

Решение:

1) удалим логические связки →:

∀_x(¬P₁(х)∨∀_y(¬P₂(y)∨P₃(z)))&¬∀_y(¬P₄(x, y)∨P₅(z))

2)выполним операцию отрицания:

∀_x(¬P₁(х)∨∀_y(¬P₂(y)∨P₃(z)))&∃_y(¬(¬P₄(x,y)∨P₅(z)))

3) применим закон де Моргана:

∀_x(¬P₁(х)∨∀_y(¬P₂(y)∨P₃(z)))&∃_y(P₄(x,y)&¬P₅(z))

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

∀_w(¬P₁(w)∨∀_y(¬P₂(y)∨P₃(z)))&∃_y(P₄(x,y)&¬P₅(z))

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

∀_w(¬P₁(w)∨∀_v(¬P₂(v)∨P₃(z)))&∃_y(P₄(x,y)&¬P₅(z))

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

∀_w∀_v(¬P₁(w)∨¬P₂(v)∨P₃(z))&∃_y(P₄(x,y)&¬P₅(z))

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

∀_w∀_v∃_y((¬P₁(w)∨¬P₂(v)∨P₃(z))&P₄(x,y)&¬P₅(z)).

3. Преобразовать формулу:

∀_x(P₁(х)«∃_y(P₂(y)))→∀_z(P₃(z)).

Решение:

1) удалим логические связки «и ®:

∀_x((P₁(х)®∃_y(P₂(y)))&(∃_y(P₂(y))® P₁(х)))®∀_z(P₃(z))=

∀_x((ØP₁(х)Ú∃_y(P₂(y)))&(¬$_y(P₂(y))ÚP₁(х)))®∀_z(P₃(z))=

Ø∀_x((ØP₁(х)Ú∃_y(P₂(y)))&(¬$_y(P₂(y))ÚP₁(х)))Ú∀_z(P₃(z))

2) по закону отрицания кванторов:

$_xØ((ØP₁(х)Ú∃_y(P₂(y)))&("_y(ØP₂(y))ÚP₁(х)))Ú∀_z(P₃(z))

3) применим закон де Моргана:

$_x (Ø(ØP₁(х)Ú∃_y(P₂(y)))ÚØ("_y(ØP₂(y))ÚP₁(х)))Ú∀_z(P₃(z))=

$_x ((P₁(х)&Ø∃_y(P₂(y)))Ú(Ø"_y(ØP₂(y))&ØP₁(х)))Ú∀_z(P₃(z))

4) по закону отрицания кванторов:

$_x ((P₁(х)&"_y(ØP₂(y)))Ú($_y(P₂(y))&ØP₁(х)))Ú∀_z(P₃(z))

5) переименуем связанную переменную левого квантора "_y - y=v:

∃_x((P₁(x)&"_v(ØP₂(v)))∨($_y(P₂(y))&ØP₁(x)))∨∀_z(P₃(z))

6) вынесем кванторы в префикс:

∃_x"_v$_y"_z((P₁(x)&ØP₂(v))∨(P₂(y)&¬P₁(х))∨P₃(z))

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

∃_x"_v$_y"_z ((P₁(x)∨P₂(y)∨P₃(z))&(ØP₂(v)∨P₂(y)∨P₃(z))&(ØP₂(v)∨ØP₁(x)∨P₃(z)))

4. Преобразовать формулу:

∀_x∃_y(P₁(х, y))&Ø(∃_x∀_y(P₂(x, y))).

Решение:

1) выполним отрицание:

∀_x∃_y(P₁(х, y))&∀_xØ(∀_y(P₂(x, y)))=∀_x∃_y(P₁(х, y))&∀_x∃_y(ØP₂(x, y))

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

∀_x(∃_y(P₁(х, y))&∃_y(ØP₂(x, y)))

3) переименуем связанную переменную y=z:

∀_x(∃_z(P₁(х, z))&∃_y(ØP₂(x, y)))

4) вынесем кванторы влево:

∀_x∃_z∃_y(P₁(х, z)&ØP₂(x, y)).

Наличие разноименных кванторов в префиксе не позволяет осуществлять вывод заключения, опираясь только на матрицу. Однако есть эффективный алгоритм Сколема, удаляющий из префиксной части кванторы существования и преобразующий формулу к виду:

F = ∀_x1∀_x2…∀_xn (M).

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

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

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

Шаг 1: представить формулу F в виде ПНФ, т. е. F=ℜ_x1ℜ_x2…ℜ_xn(M), где ℜ_i∈{∀, ∃}, а М=D₁&D₂&D₃&…,

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

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

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

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

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

Дата добавления: 2014-01-04