Boyer-Moore theorem prover

というのがあるそうで、例えば、PLUS演算の結合性
(EQUAL (PLUS X (PLUS Y Z)) (PLUS (PLUS X Y) Z))
が証明できると書いてある。

こないだのLispは、勿論数学的帰納法が使えないので、上の式を証明することはできないけれど、帰納法の各ステップなら、「殆ど証明可能」

(lisp '(= (+ 0 (+ J K)) (+ (+ 0 J) K)))

=>(= (+ J K) (+ J K))
(lisp '(-> (= (+ I (+ J K)) (+ (+ I J) K)) (= (+ (s I) (+ J K)) (+ (+ (s I) J) K))))

=>true

前者も、更に帰納法を使えば証明できる

#'( (= %x %x) . true )
というルールを加えなかったのは、"="は数値の比較のみに限定したいと考えたから。けど、単純な項書き換え系では、データ型の判定はできない。項書き換え系をデータ型付に拡張すればいいんだろうか

Boyer-Moore theorem proverは結構強力で
http://www.cs.utexas.edu/users/moore/best-ideas/nqthm/
によれば、そこそこhardな定理も証明されているらしい。けど、これらは、命題を形式化して放り込んでやれば、答えが返ってくるようなものではなく、人間が無数の補題を用意してやって初めて証明できたんだと思う。そういう意味では、「自動証明」とは程遠い。詳しい原理は知らないけど、多分、基本的には、項書き換えによる等式推論+帰納法なんだと思う。