Задача 5 (4 баллов). Методом резолюций доказать противоречивость
следующего множества дизъюнктов: S={D1, D2, D3, D4, D5; D6, D7}, где
D1 = E(x) v V(y) v C(f(x)), D2=E(x) v S(x, f(x)), D3 = -E(a),
D4 =P(a), D5=P(f(x)) v -S(y,x), D6 = -P(x) v -V(g(x)) v -V(y),
D7 = -P(x) v -C(y).
Чтобы доказать противоречивость множества дизъюнктов S с помощью метода резолюций, мы будем последовательно применять правила резолюции к дизъюнктам, пока не получим пустой дизъюнкт, что будет означать противоречивость.
Дано множество дизъюнктов:
Из D1 и D3:
Подставляем a вместо x в D1:
Теперь применяем резолюцию:
Обозн...