Всем привет!
Задали задание:
"доказать секвенцию исчисление высказываний методом резолюций"
А۷(¬В۷¬С)├ А۷¬(В&С)

Решение:
А۷(¬В۷¬С)├ А۷¬(В&С)
А=А۷(¬В۷¬С)=>А۷¬(В&С)
А=¬[А۷(¬В۷¬С)&¬А۷¬(В&С)]
Следовательно
¬А=(А۷(¬В۷¬С)&¬(А۷¬(В&С)))
Ищем дизъюнкты:

я на верном пути???
и вот на счет дизъюнктов у меня возникли проблемы....

ОБЩЕЗНАЧИМОСТЬ — свойство логической формулы, состоящее в том, что эта формула истинна при любой интерпретации входящих в нее нелогич. символов, т. е. предикатных и пропозициональных переменных. Логич. формулы, обладающие этим свойством, наз. общезначимыми.

Такой вывод сделала т.к. не получилось пустых резольвент.