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

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

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

в двух предложениях, одно из которых состоит из одной литеры, а второе содержит произвольное число литер, находится контрарная пара литер (например В и ¬В), которая вычеркивается, а из оставшихся частей формируется новое предложение (например В из ¬В۷С и выводится С).