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)のような形をした論理式は無数に存在する。
定理の証明のために、うまく公理をつかうには、ひらめきが必要になってしまう。
自動定理証明のためには、導出原理などの工夫が必要なようだ。