Установить правильность рассуждения построив вывод исчисления высказываний

Обозначим:
А = «Идет дождь»;
В = «Крыши мокрые».
Тогда:
А = «Дождя нет»;
В = «Крыши не мокрые».
Нужно построить следующий вывод:
A → B, B ├ A.
Построим вывод:
(1) A → B – гипотеза;
(2) B – гипотеза;
(3) В → А – из (1) по правилу контрапозиции;
(4) А – из (2) и (3) по m.p.
Проверим вывод методом резолюций . Для этого нужно проверить вывод
A → B, B, A├ .
1)Приведем к КНФ формулы A → B, B, A.
AB AB.
Формулы B, A уже находятся в КНФ.
2)Составим множество дизъюнктов:
К = {A В, В, A}.
3) Построим резолютивный вывод из K