Здравствуйте, dilettante, Вы писали:

D>Вообще адская вещь, как подходить к доказательству даже чего-то совсем простого — например (Α∧B→C) → (A→B→C) — совершенно не понятно.

Откройте для себя секвенциальное исчисление, там свойство подформульности сильно упрощает автоматизацию доказательства.