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

[nbyte]

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

$$\[S = \{ r \vee \neg s \vee \neg u,\neg p \vee q \vee \neg u,p \vee \neg u \vee \neg s,\neg q \vee \neg r \vee p \vee \neg s,s,\neg s \vee u,\neg s \vee q,\neg p\} \] $$

Нужно доказать, что множество противоречащее при помощи метода резолюций.

В какой последовательности нужно выписывать пары формул из множества S и применять формулу вывода?
И что нужно получить в результате, чтобы доказать?

[Xaositect]

Так.
Метод резолюций применяется для доказательства противоречивости множеств Хорновских дизъюнкций.
Правило резолюции: из дизъюнкций $a\vee B$ и $\neg a\vee C$ мы можем образовать дизъюнкт $B\vee C$. При этом дизъюнкции $B$ и $C$ могут быть пустыми (например, применяя резолюцию к $a$ $\neg a \vee b$, получим $b$, а применяя к $a$ и $\neg a$ мы получим пустую дизъюнкцию $0$). Если после нескольких применений правила резолюций мы получим пустую дизъюнкцию, то система противоречива.

Насчет стратегии вывода - попробуйте взять одну дизъюнкцию, и применять правило резолюции к ней и остальным дизъюнкциям по очереди, затем с получившейся дизъюнкцией аналогично, и т.д. Если не получилось, возьмите другую начальную дизъюнкцию.

[nbyte]

Может можете как-то по другому объяснить.
А то мне тут ну не как не доходит.

Я себе представляю это так:
Беру две формулы, где у одной некая переменная с отрицание, а у другой без отрицания. Применяю (формула1)$\vee$(формула2). Получаю какаюту формулу, а так дальше?

[EtCetera]

nbyte
У Вас есть список дизъюнктов. Вы находите среди них какую-либо пару, в которой один дизъюнкт содержит переменную, а другой - ее отрицание. На основе этих двух дизънктов получаете один новый (по правилу, подробно описанному Xaositect). Новый дизъюнкт Вы вносите в список. И начинаете поиски подходящей пары снова.
Все это действо продолжается до тех пор, пока на некотором шаге в списке не окажется пара $a$ и $\neg a$.

[nbyte]

ММмм так.
А можно ещё тогда спросить (вопрос при решении появился)
Можно-ли сражу к одной формуле применить 2 формулы. Тоесть если выпиисать три формулы и к одно применить сразу 2?

-- Чт ноя 12, 2009 20:14:00 --

Наконец-то вышло решить