Доказать методом резолюций

[Arsenii]

Имеется тавтология
$\models(A\wedge B\rightarrow C)\rightarrow(A\rightarrow (B\rightarrow C))$
Решение:
Шаг 1$\overline {(A\wedge B\rightarrow C)\rightarrow(A\rightarrow (B\rightarrow C))}$
Шаг 2$(A\wedge B\rightarrow C)\vee\overline {(A\rightarrow (B\rightarrow C))}$
Шаг 3$(\overline {A\wedge B}\vee C)\vee(A\vee (B\vee \overline {C}))$
Шаг 4$(\overline {A}\vee \overline {B}\vee C)\vee(A\vee (B\vee \overline {C}))$
Шаг 5$\overline {A}\vee \overline {B}\vee C\vee A\vee B\vee\overline{C}$

Блин в итоге получается 1. Где я ошибся

[Maslov]

Проверьте аккуратненько переход от шага 1 к шагу 2.

[Arsenii]

Maslov в сообщении #579079 писал(а):

Проверьте аккуратненько переход от шага 1 к шагу 2.

Там не снимается отрицание? Если так объясните почему, а то в конспекте, тоже в примете при переходе от импликации к дизъюнкции отрицание с первого слагаемого не снимается, не могу понять почему

[Maslov]

$\overline { a \to b} = \overline { \overline a \lor b} = a \land \overline b$

[Arsenii]

Этого соотношения у меня не было
Переделываю:
Шаг 2$\overline {\overline {(A\wedge B\rightarrow C)}\vee(A\rightarrow (B\rightarrow C))}$
Шаг 3$(A\wedge B\rightarrow C)\wedge\overline {(A\rightarrow (B\rightarrow C))}$
Шаг 4$(\overline {A\wedge B}\vee C)\wedge (A \wedge \overline {(B \rightarrow C)})$
Шаг 5$(\overline {A}\vee \overline {B}\vee C)\wedge(A\wedge(B\wedge\overline {C}))$
Так а как дальше действовать?

[Maslov]

Вы получили множество дизъюнктов $\{ \neg A \lor \neg B \lor C, A, B, \neg C \}$.

Теперь последовательно применяя правило резолюции $a \lor F, \neg a \lor G \Rightarrow F \lor G$ попробуйте вывести пустой дизъюнкт. Если это удастся, то будет означать, что отрицание Вашей исходной формулы противоречиво.

Имейте в виду, что $F$ и $G$ могут быть пустыми, т. е. $A$ можно представить как $A \lor 0$.

[Arsenii]

1)$\overline {A}\vee \overline {B}$
2)$\overline {B}\vee C$
3)$A$
4)$B$
5)$\overline {C}$
Следовательно:
1)$\overline {B}$ резолюция 1, к 1 и 3 выражениям
2)$\overline {A}$ резолюция 2, к 1 и 4 выражениям
3)$ C $ резолюция 1, к 2 и 5 выражениям
Все получается?

[Arsenii]

Посмотрите, я правильно все решил или это неправильно?

[Maslov]

Непонятно Вы как-то решили.

Какой дизъюнкт получится в результате применения правила резолюции к дизъюнктам $\neg A \lor \neg B \lor C$ и $A$?

[Arsenii]

Я сначала ввел допущения, а после находил противоречия в этих допущениях. То по правилу введения отрицания функции является ложным, а значит функция является тавтологией. А как можно было еще решать ?

[Maslov]

Arsenii в сообщении #580355 писал(а):

А как можно было еще решать ?

Вам же надо решить методом резолюций, поэтому разберитесь сначала, что это такое.

Вот тут, например, есть некоторые пояснения: «Математическая логика, метод Резолюций», ну и еще по форуму поищите.