Помогите, пожалуйста, с заданием по матлогике!

Вывод в генценовском исчислении выска-зываний
1. Вывести секвенции:
¬A → B ⇒ ¬B → A,
(A → → C ⇒ (A ∨ C) ∧ (B → C), (A ∨ C) ∧ (B → C) ⇒ (A → → C

Интуиционистская логика
1. Проверить, выводимы ли формулы в интуиционистской логике. Ес- ли нет, то построить для них опровергающие модели Крипке.
¬¬¬A → ¬A,
¬(A ∧ B ∧ C) → ¬(A ∧ ∨ ¬(A ∧ C) ∨ ¬(B ∧ C), ¬¬(A ∧ ∨ (A → ∨ (B → A)
2. Вывести в интуиционистском исчислении высказываний (можно в секвенциальном) :
¬¬((A → ∨ (B → A)).