Математическая логика и теория алгоритмов (2)

Расшифровка вопроса такая:

Нужно доказать, что из одновременного выполнения трех посылок
F₁ = А + В
F₂ = A → В
F₃ = В → А
следует выполнение
F = А • В
Т. е. нужно рассмотреть такую конструкцию:
F₁ • F₂ • F₃ → F  ❶
→ обозначает импликацию (т. е. следствие)

В методе резолюций вместо ❶ принято рассматривать
F₁ • F₂ • F₃ • ¬F = 0   ❷
¬ обозначает отрицание
Суть метода резолюций:
☛ Если справедливо ❷, то автоматически справедливо ❶

Подставляем в ❷ явные выражения для F₁, F₂, F₃ и F, получаем, что надо доказать справедливость
(А + В) • (A → В) • (В → А) • ¬(А • В) = 0   ❸
Тем самым будет доказана справедливость
[(А + В) • (A → В) • (В → А)] → (А • В)   ❹

Для импликации справедлива формула
F → G = ¬F +G
Два раза применяем ее в ❸:
(А + В) • (¬А +В) • (¬В + А) • ¬(А • В) = 0
Для ¬(А • В) применяем формулу Моргана:
¬(А • В) = ¬А + ¬В
Получаем:
(А + В) • (¬А +В) • (¬В + А) • (¬А + ¬В) = 0   ❺
Получили произведение (конъюнкцию) четырех слагаемых (дизъюнктов)

В ❺ для (А + В) • (¬А +В) и для (¬В + А) • (¬В + ¬А) применяем формулу склеивания:
(F + G) • (¬F +G) = G
Получаем:
В • ¬В = 0
0 = 0
Доказана справедливость ❸

Следовательно, по методу резолюций заключение ❹ справедливо

Любой импликант типа A -> B можно привести к какому-то дизъюнктиву! Думай в этом направлении