Условие:
Для доказательства противоречивости S нужно убедиться в том, что
множество дизъюнктов S содержит пустой (ложный) дизъюнкт .
Поскольку S первоначально такого дизъюнкта не содержит, надо вывести
его, используя правило порождения новых дизъюнктов из исходных. Новые
дизъюнкты получаем методом резолюции и добавляем их к множеству S.
Дано:
D1 : ¬A v B
D2 : ¬B ∨ C
D3 : ¬C ∨ D
D4 : A ∨ D
D5 : ¬D
D6 : ¬(¬A ∨ ¬C)
Пример:
D1 : ¬A v B
D2 : ¬C v D
D3 : ¬ D v ¬B v E
D4 : ¬E
D5 : А
D6 : С
-------------------------
D7 : ¬ D v ¬B (резольвента D3, D4)
D8 : ¬C v ¬B (резольвента D2, D7)
D9 : ¬A v ¬C (резольвента D1, D8)
D10 : ¬C (резольвента D10, D5)
D11 : (резольвента D11, D6)