Математическая логика, метод резолюций

[nbyte]

Здравствуйте.
Подскажите пожалуйста, хочу спросить по методу решения следующих примеров
Есть например пример

Цитата:

При помощи метода резолюций проверьте, является-ли следующая формула сама себе противоречащей $\[(\neg p \vee q)\& ((q \to r) \to (\neg p \vee r))\]$

Пробую решить так
Преобразовываю и получаю $\[(\neg p \vee q)\& (q \vee \neg p)\]$
Дальше $\[(\neg p \vee q)\& (q \vee \neg p)\] \Rightarrow \[S = \{ \neg p \vee q,q \vee \neg p\} \]$
и выписывая
1. $(\neg p \vee q)$
2. $(q \vee \neg p)$
3. $(q \vee \neg p)$ из 1. и 2. $\Rightarrow$ противоречит.

Правильно-ли я делаю? Если правильно, тогда есть-ли какие-то неточности?

[EtCetera]

nbyte
Не совсем верно. Ведь после приведения формулы к КНФ у Вас образовалось 2 одинаковых дизъюнкта ($\neg p \vee q\equiv q\vee\neg p$), из которых в списке оставляется только один в соответствии с естественным правилом $x\wedge x\wedge\dots\wedge x\equiv x$ (в Вашем случае просто $x\wedge x\equiv x$). Т.е. применять правило резолюции просто не к чему (в списке остается один дизъюнкт) и, т.о., формула не противоречит сама себе.

[nbyte]

Хммм спасибо вам EtCetera, за ценное объяснение.
Теперь тут мне вроде-бы всё ясно.