Условие задачи
Доказать справедливость рассуждения методом резолюции
Либо Петя поехал отдыхать на юг, либо, если Петя не сдал вовремя сессию, то ему пришлось каникулы провести дома. Если Петя поехал отдыхать на юг, то он сдал сессию вовремя. Следовательно, если Петя не сдал сессию вовремя, то ему пришлось каникулы провести дома.
Введем буквенные обозначения для атомарных высказываний:
Подставляем обозначения для атомов:
Либо A, либо, если не B то C.
Если А, то B
Формализация рассуждения.
Aν (¬B→ C), A→B ├ ¬B → C
В формализованном рассуждении из четырёх посылок следует заключение
¬B → C
Aν (¬B→ C),
A→B
¬B → C
Ответ
Доказываем логическое следствие заключения B C из посылок A (B C), AB
Доказательство методом резолюции выполняется только от противного: к произведению всех посылок добавляем отрицание заключения:
Приводим к КНФ:
