X, y, yÚu, uÚxÚØz |- uÚz

2) |- (x®((yÚ x) ® z)) ® (y®z)

3) xÚ y |- (zÙ x) ® (yÙ z)

4) Ø x, Ø y |- (x ® z) ® (y ®z)

Решение:

Секвенция 1) – недоказуема.

Проверка:

а) Алгоритм Квайна:

xÙ yÙ (yÚ u)Ù (uÚ xÚ Ø z) |- uÚ z

Пусть x = 1, тогда:

yÙ (yÚ u)Ù (uÚ Ø z) |- uÚ z

Пусть y=1, тогда:

1Ù 1Ù (uÚ Ø z) |- uÚ z

Пусть u=0, тогда:

1Ù 0Ù Ø z |- 0Ú z

Пусть z=0 тогда:

1 |- 0 – тождественно ложно => секвенция недоказуема

б) Алгоритм редукции:

Предположим: xÙ yÙ (yÚ u)Ù (uÚ xÚ Ø z) ® uÚ z = 0

Тогда xÙ yÙ (yÚ u)Ù (uÚ xÚ Ø z)=1, uÚ z=0 => u=0, z=0.

Подставим u=0, z=0 в xÙ yÙ (yÚ u)Ù (uÚ xÚ Ø z)=1:

Обязательно должно быть (uÚ xÚ Ø z)=1

(0Ú xÚ 1)=1

1=1 => непротиворечиво => секвенция недоказуема

в) Метод резолюции (оптимальный):

Докажем противоречивость:

xÙ yÙ (yÚ u)Ù (uÚ xÚ Ø z), Ø (uÚ z)

Приводим к КНФ:

x, y, (yÚ u), (uÚ xÚ Ø z), Ø u, Ø z

(1) x

(2) y

(3) yÚ u

(4) uÚ xÚ Ø z

(5) Ø u

(6) Ø z

(7) res_u(3, 5) = y

Данное множество непротиворечиво => секвенция недоказуема.

Секвенция 2) – недоказуема.

Проверка:

а) Алгоритм Квайна:

|- (x®((yÚ x) ® z)) ® (y®z)

Пусть x = 0, тогда:

|- (0®((yÚ 0) ® z)) ® (y®z)

Пусть y=1, тогда:

|- (0®((1) ® z)) ® (1®z)

Пусть z=0, тогда:

|- 0 ® 0

1 |- 0 – тождественно ложно => секвенция недоказуема

б) Алгоритм редукции (оптимальный):

Предположим: |- (x®((yÚ x) ® z)) ® (y®z) = 0

Тогда (x®((yÚ x) ® z)) ® (y®z) = 0 => x=0, y=1, z=0.

Подставим x=0, y=1, z=0 в 1:

0=0 или

1=1 => непротиворечиво => секвенция недоказуема

в) Метод резолюции:

Докажем противоречивость:

Ø (x®((yÚ x) ® z)) ® (y®z)

Приводим к КНФ:

Ø ((x®(Ø (yÚ x) Ú z)) ® (y®z))

Ø (Ø (Ø xÚ (Ø (yÚ x) Ú z)) Ú (Ø yÚ z))

Ø ((Ø Ø xÙ (Ø Ø (yÚ x) Ù Ø z)) Ú (Ø yÚ z))

Ø ((xÙ yÙ x Ù Ø z)) Ú (Ø yÚ z))

Ø ((xÙ yÙ Ø z)) Ú (Ø yÚ z))

Ø (xÙ yÙ Ø z) Ù Ø (Ø yÚ z)

(Ø xÚ Ø yÚ z)Ù (yÙ Ø z)

(1) (Ø xÚ Ø yÚ z)

(2) y

(3) Ø z

(4) res_y(1, 2) = (Ø xÚ z)

(5) res_z(1, 3) = (Ø xÚ Ø y)

Данное множество непротиворечиво => секвенция недоказуема.

Секвенция 3) –недоказуема.

Проверка:

а) Алгоритм Квайна(оптимальный):

xÚ y |- (zÙ x) ® (yÙ z)

Пусть x = 1, тогда:

1Ú y |- (zÙ 1) ® (yÙ z)

Пусть y=0, тогда:

1 |- z ® 0

Пусть z=0, тогда:

1 |- 0 – тождественно ложно => секвенция недоказуема

б) Алгоритм редукции:

Предположим: xÚ y |- (zÙ x) ® (yÙ z) = 0

Тогда xÚ y =1, (zÙ x) ® (yÙ z) = 0

Тогда (zÙ x)=1, (yÙ z) = 0 => z=1, x=1, y=0

Подставим z=1, x=1, y=0 в xÚ y =1:

Обязательно должно быть (1Ú 0)=1

1=1 => непротиворечиво => секвенция недоказуема

в) Метод резолюции:

Докажем противоречивость:

xÚ y, Ø ((zÙ x) ® (yÙ z))

Приводим к КНФ:

xÚ y, Ø (Ø (zÙ x)Ú (yÙ z))

xÚ y, (Ø Ø (zÙ x)Ù Ø (yÙ z))

xÚ y, z, x, (Ø yÚ Ø z)

(1) xÚ y

(2) z

(3) x

(4) (Ø yÚ Ø z)

(5) res_y(2, 4) =Ø y

(6) res_y(1, 5) =x

Данное множество непротиворечиво => секвенция недоказуема.

Секвенция 4) – доказуема.

Проверка:

По формулам вывода:

0 |- z = > тождественно истина => секвенция доказуема

Для док-ва воспользуемся эквив-тями ИП:

(j®y)º (Ø jÚ y), Ø (jÚ y)º (Ø jÙ Ø y),

jÚ (yÙ x)º (jÚ y)Ù (jÚ x)

преобразуем:

(x®z)®(y®z) º Ø (x®z)Ú (y®z)º Ø (Ø xÚ z)Ú (Ø yÚ z)º (xÙ Ø z)Ú (Ø yÚ z) º º (x Ú Ø y Ú z) Ù (Ø z Ú Ø y Ú z) º x Ú Ø y Ú z

получили:

Ø x, Ø y |-x Ú Ø yÚ z

аксиома:

Ø y |- Ø y 11, 12

Ø x, Ø y|- Ø y 5

Ø x, Ø y |- x Ú Ø y 4

Ø x, Ø y |- x Ú Ø y Ú z

Задание №2