Условие:
Задача 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: 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) ### Шаг 1: Применение резолюции к D1 и D3 Из D1 и D3: - D1: E(x) v V(y) v C(f(x)) - D3: -E(a) Подставляем a вместо x в D1: - E(a) v V(y) v C(f(a)) Теперь применяем резолюцию: - V(y) v C(f(a)) Обозн...