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

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

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

какие проблемы?

проблемы с дизъюнктами
¬А=(А۷(¬В۷¬С)&¬(А۷¬(В&С)))

не знаю как дальше быть....

Какие вы знаете свойства?

ой в алгоритме решений ниче про свойства нет.....
знаю что щас находим контрарную пару и вычеркиваем ее
¬А=(А۷(¬В۷¬С)&¬(А۷¬(В&С)))

как правильно вычеркнуть?

нашла кое-что:
¬(В&С)≡¬В۷¬С

выходит:
¬А=(А۷(¬В۷¬С)&¬(А۷(¬В۷¬С)))

теперь контрарная пара это:
(¬В۷¬С)
или
(А۷(¬В۷¬С)
?

ау...математические гении вы куда все пропали????(

Правильно нашли. Так. А что такое контрарная пара??

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

Тогда ничего из тех двух возможностей не является контрарной парой

тут же знак отрицания перед второй скобкой:
¬(А۷(¬В۷¬С))
все равно нет контрарной пары?

нет )

Вывод: формула А не является общезначимой.
Правильно?

Дайте определение общезначимой формулы

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

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

Ладно, тогда вроде верно.