Prologで自動定理証明?

論理学の定理は、形式論的には、公理と推論規則から導かれるものだ。
たとえば、ヒルベルト流では、

A ⊃ (B ⊃ A)
(A ⊃ (B ⊃ C)) ⊃ ((A ⊃ B) ⊃ (A ⊃ C))
(¬A ⊃ ¬B) ⊃ (B ⊃ A)

という三つの公理と、次のMP(modus ponens)という一つの推論規則を用いる。
A と (A ⊃ B) が定理ならば、Bも定理である。

で、公理を事実、推論規則をルールとしてPrologに実装してやれば、自動的に定理を証明してくれるかな?と思ったのだが...

実装例

theorem( imp( P, imp(Q,P) ) ).
theorem(imp(imp( P, imp(Q,R) ),  imp( imp(P,Q), imp(P,R)))).
theorem(imp(imp(neg(P),neg(Q)),imp(Q,P))).
theorem(B):- theorem(A), theorem(imp(A,B)).

上記のような実装でたとえば
theorem(imp(a,a)) #A ⊃ A
のようなものは証明できた。
しかし、証明できない式もたくさんある。

ヒルベルト流でなにか定理を証明しようとするとき、機械的に行うのは難しい(もしかして無理?)のようだ。
なぜなら、A ⊃ (B ⊃ A)のような形をした論理式は無数に存在する。
定理の証明のために、うまく公理をつかうには、ひらめきが必要になってしまう。
自動定理証明のためには、導出原理などの工夫が必要なようだ。