(Матлогика) Доказать истинность выражения

[j0n]

Помогите пожалуйста доказать истинность заключения методом дедукции и резолюции
$(B\rightarrow A);(B\rightarrow(\rceil A\vee C))\vdash (B\rightarrow(\rceil B\vee C))$

Предполагаю, что методом дедукции доказывается так:
1) $F_1 = B\rightarrow A$ - посылка
2) $F_2 = B\rightarrow(\rceil A\vee C)$ - посылка
3) $F_3 = A\rightarrow(\rceil B\vee C)$ - заключение по формулам F1 и F2
4) $F_4 = B\rightarrow(\rceil B\vee C)$ - заключение по формулам F1 и F3

Примерно так. Только не знаю, правильное ли это доказательство. И еще не знаю, по каким аксиомам или теоремам доказать пункты 3 и 4

Теперь про метод резолюций. Алгоритм такой:

$F_1;F_2;...;F_n\vdash B$
Шаг 1. принять отрицание заключения, т.е. $\rceil B$;
Шаг 2. привести все формулы посылок и отрицания заключения к конъюнктивной нормальной форме;
Шаг 3. выписать множество дизъюнктов всех посылок и отрицания заключения:
$K =\left\{ D_1; D_2; . . . D_k\right\} $;
Шаг 4. выполнить анализ пар множества $K$ по правилу:
“если существуют дизъюнкты $D_i$ и $D_j$, один из которых ($D_i$) содержит литеру $A$, а другой ($D_j$) - контрарную литеру $\rceil A$, то соединить эту пару логи­ческой связкой дизъюнкции $(D_i\vee \rceil D_j)$ и сформировать новый дизъюнкт - резольвенту, исключив контрарные литеры $A$ и $\rceil A$;
Шаг5. если в результате соединения дизъюнктов, содержащих контрарные литеры, будет получена пустая резольвента - , то конец (доказательство подтвердило противоречие), в противном случае включить резольвенту в множество дизъюнктов $K$ и перейти к шагу 4.

Алгоритм приведения к нормальной форме
Шаг 1. Устранить логические связки “$\leftrightarrow$” и “$\rightarrow$” всюду по правилам:
$F_1\leftrightarrow F_2 =(F_1\rightarrow F_2)\wedge (F_2\rightarrow F_1)=(\rceil F_1\vee F_2)\wedge (\rceil F_2\vee F_1)=$
$=(\rceil F_1\wedge \rceil F_2)\vee (F_1\wedge F_2)$;
$F_1\rightarrow F_2 =\rceil F_1\vee F_2 =\rceil (F_1 \wedge (\rceil F_2))$.
Шаг 2. Продвинуть отрицание до элементарной формулы (пропозициональной переменной) по правилам:
$\rceil (\rceil F) = F$ ;
$\rceil (F_1\vee F_2 ) = (\rceil F_1)\wedge (\rceil F_2)$;
$\rceil (F_1\wedge F_2) = (\rceil F_1)\vee(\rceil F_2)$.
Шаг 3. Применить закон дистрибутивности:
a) для КНФ: $F_1\vee (F_2\wedge F_3) = (F_1\vee F_2)\wedge (F_1\vee F_3)$;
b) для ДНФ: $F_1\wedge (F_2\vee F_3) = (F_1\wedge F_2)\vee (F_1\wedge F_3)$.

Проблема возникает на втором шаге. Формулы посылок никак не приводятся к КНФ, а только к ДНФ:
$B\rightarrow A = \rceil B\vee A$ - ДНФ
$B\rightarrow(\rceil A\vee C) = \rceil B\vee \rceil A\vee C$ - ДНФ
$B\rightarrow(\rceil B\vee C) = B\wedge C$ - КНФ
Поэтому дальше не получается(((

[j0n]

помогите пожалуйста с доказательством по методу резолюций (точней как привести к КНФ).
с дедукцией разобрался, сам доказал.

-- Пт дек 18, 2009 12:33:43 --

$B\rightarrow(\rceil B\vee C) = B\wedge C$ - эта строчка неправильная
$\rceil (B\rightarrow(\rceil B\vee C)) = B\wedge \rceil C$

-- Пт дек 18, 2009 12:41:01 --

че то я стормозил..... все отлично получается