＞＞ 証明の方針を与えたり「発想」する部分は今のコンピュータじゃまだできません。
＞体系が単純で簡単な証明なら総当り式でできるでしょう。

２変数以上の述語記号を持つ述語論理の体系では不可能。
１変数以上の述語記号と２変数以上の関数記号を持つ述語論理の体系でも不可能。
述語記号・関数記号が全て１変数の述語論理の体系であれば、可能。

最後の場合は、任意に与えられた論理式がその体系で証明可能かどうか
を判定するアルゴリズムを作れる。
文献：前原昭二著「数理論理学-数学的理論の論理的構造-」培風館