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

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

∃_x1∀_x2∀_x3∃_x4∀_x5∃_x6((P₁(x₁,x₂)∨¬P₂(x₃,x₄,x₅))&P₃(x₄,x₆)).

Решение:

1) примем x₁=a и удалим $_x1:

∀_x2∀_x3∃_x4∀_x5∃_x6((P₁(a,x₂)∨¬P₂(x₃,x₄,x₅))&P₃(x₄,x₆))

2) примем x₄=f₁(x₂,x₃) и удалим ∃_x4:

∀_x2∀_x3∀_x5∃_x6 ((P₁(a,x₂)∨¬P₂(x₃,f₁(x₂,x₃),x₅))&P₃(f₁(x₂,x₃),х₆))

3) примем x₆=f₂(x₂, x₃, x₅) и удалим ∃_x6:

∀_x2∀_x3∀_x5((P₁(a,x₂)∨¬P₂(x₃,f₁(x₂,x₃),x₅))&P₃(f₁(x₂,x₃),f₂(x₂,x₃,x₅)))

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

∃_z∀_w∃_x∀_y((P₁(z)∨P₂(x)∨P₃(y))&(¬P₂(w))∨P₂(х)∨P₃(y))&(¬P₂(w)∨¬P₁(z)∨P₃(y))).

Решение:

1) примем z=a и удалим квантор ∃_z:

∀_w∃_x∀_y((P₁(a)∨P₂(х)∨P₃(y))&(¬P₂(w)∨P₂(х)∨P₃(y))&(¬P₂(w)∨¬P₁(a)∨P₃(y)))

2) примем x=f(w) и удалим квантор ∃_x:

∀_w∀_y((P₁(a)∨P₂(f(w))∨P₃(y))&(¬P₂(w)∨P₂(f(w))∨P₃(y))&(¬P₂(w)∨¬P₁(a)∨P₃(y)))

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

$_x("_y(P₁.(x, y)))&$_x("_y(P₂.(x, y))).

Решение:

1) заменим связанную левым квантором $_x переменную x=v:

$_v("_y(P₁(v, y)))&$_x("_y(P₂(x, y)))

2) заменим связанную левым квантором "_y переменную y=w:

$_v("_w(P₁(v, w)))&$_x("_y(P₂(x, y)))

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

$_v"_w$_x"_y(P₁(v, w)&P₂(x, y))

4) заместим предметную переменную v на предметную постоянную ‘ a’:

"_w$_x"_y(P₁(a, w)&P₂(x, y))

5) заместим предметную переменную x функцией от w, т.е. x=f(w):

"_w"_y(P₁(a, w)&P₂(f(w), y))

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

$_x("_y(P₁(x, y)))Ú$_x("_y(P₂(x, y))).

Решение:

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

$_x("_y(P₁(x, y))Ú"_y(P₂(x, y)))

2) заменим связанную левым квантором "_y переменную y=w:

$_x("_w(P₁(x, w))Ú"_y(P₂(x, y)))

3) вынесем кванторы "_w и "_y в префикс:

$_x"_w"_y (P₁(x, w)ÚP₂(x, y))

4) заместим предметную переменную x на предметную постоянную ‘ a’:

"_w"_y (P₁(a, w)ÚP₂(a, y)).

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

$_x("_y(P₁(x, y)))®$_x("_y(P₂(x, y))).

Решение:

1) удалим связку ®:

Ø$_x("_y(P₁(x, y)))Ú$_x("_y(P₂(x, y)))

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

"_x(Ø"_y(P₁(x, y)))Ú$_x("_y(P₂(x, y)))="_x($_y(ØP₁(x, y)))Ú$_x("_y(P₂(x, y)))

3) заменим связанную левым квантором переменную х=w:

"_w($_y(ØP₁(w, y)))Ú$_x("_y(P₂(x, y)))

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

"_w($_v(ØP₁(w, v)))Ú$_x("_y(P₂(x, y)))

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

"_w$_v$_x"_y(ØP₁(w, v)Ú P₂(x, y))

6) заместим предметную переменную v функцией от w, т.е. v=f₁(w):

"_w$_x"_y(ØP₁(w, f₁(w))Ú P₂(x, y))

7) заместим предметную переменную x функцией от w, т.е. x=f₂(w):

"_w"_y(ØP₁(w, f₁(w))Ú P₂(f₂(w), y))

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

"_x("_y(P₁(x, y)))®$_x($_y(P₂(x, y))).

Решение:

1) удалим связку ®:

Ø"_x("_y(P₁(x, y)))Ú$_x($_y(P₂(x, y)))

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

$_x(Ø"_y(P₁(x, y)))Ú$_x($_y(P₂(x, y)))=$_x($_y(ØP₁(x, y)))Ú$_x($_y(P₂(x, y)))

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

$_x($_y(ØP₁(x, y))Ú$_y(P₂(x, y)))

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

$_x$_y(ØP₁(x, y)ÚP₂(x, y))

5) заместим предметные переменные x и y на предметные постоянные a и b:

(ØP₁(a, b)ÚP₂(a, b))

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

"_x(P₁(x)ÚP₂(x))®("_x(P₁(x))Ú"_y(P₂(y))).

Решение:

1) удалим связку ® по законам алгебры логики:

Ø"_x(P₁(x)ÚP₂(x))Ú"_x(P₁(x))Ú"_y(P₂(y))

2) выполним отрицание и применим закон де Моргана:

$_xØ(P₁(x)ÚP₂(x))Ú"_x(P₁(x))Ú"_y(P₂(y))=$_x(ØP₁(x)&ØP₂(x))Ú"_x(P₁(x))Ú"_y(P₂(y))

3) заменим связанную левым квантором $_x переменную x=v:

$_v(ØP₁(v)&ØP₂(v))Ú"_x(P₁(x))Ú"_y(P₂(y)),

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

$_v"_x"_y(ØP₁(v)&ØP₂(v)ÚP₁(x)ÚP₂(y)),

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

$_v"_x"_y((ØP₁(v)ÚP₁(x)ÚP₂(y))&(ØP₂(v)ÚP₁(x)ÚP₂(y)))

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

$_x(P₁(x))&$_x(P₂.(x))®$_x(P₁(x)&P₂.(x)).

Решение:

1) удалим связку ®:

Ø($_x(P₁(x))&$_x(P₂.(x)))Ú$_x(P₁(x)&P₂.(x))

2) выполним отрицание и применим закон де Моргана:

"_x(ØP₁(x))Ú"_x(ØP₂.(x))Ú$_x(P₁(x)&P₂.(x))

3) заменим связанную левым квантором переменную x=v:

"_v(ØP₁(v))Ú"_x(ØP₂.(x))Ú$_x(P₁(x)&P₂.(x)),

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

"_v(ØP₁(v))Ú"_w(ØP₂.(w))Ú$_x(P₁(x)&P₂.(x)),

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

"_v"_w$_x(ØP₁(v)ÚØP₂.(w)ÚP₁(x)&P₂.(x)),

6) заместим переменную x функцией от двух переменных v и w, т.е. x=f(v, w):

"_v"_w(ØP₁(v)ÚØP₂.(w)ÚP₁(f(v, w))&P₂.(f(v, w))),

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

"_v"_w((ØP₁(v)ÚØP₂.(w)ÚP₁(f(v, w)))&(ØP₁(v)ÚØP₂.(w)ÚP₂.(f(v, w)))).

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