Very interesting paper, thanks! This paper brings up an important issue, which is already familiar to those in the symbolic algebra field -- the mechanical version of the proof can be (and probably usually is) completely alien & incomprehensible to a human. Thus, although the proof can be checked and rechecked, it could still be completely opaque for human readers. This isn't to say that a human-understandable proof can't be checked by a computer -- that would be my goal. It's just that a decision procedure might produce a non-human ("inhuman" ?) proof. At 12:22 PM 3/3/2006, Gareth McCaughan wrote:
On Friday 03 March 2006 18:49, Henry Baker wrote:
(High school plane geometry is decidable, as it is reducible to the theory of Real Closed Fields, but the general decision process is multiply-exponential, and hence currently not practical. But a decision procedure isn't necessary to verify a proof -- only to find one.)
Are you sure? I think I remember reading (several years ago) a book that purported to describe a practically usable algorithm for finding proofs of problems in high-school plane geometry, and that claimed it was already being used to good effect by Chinese participants in the International Mathematical Olympiads. Am I misremembering?
Aha, the following is about the same method:
http://www.mmrc.iss.ac.cn/~xgao/paper/ieee-logic.pdf
and it doesn't in fact purport to prove everything that can be proved in that domain. It's still pretty impressive, and likely to appeal to many munsters. (Was that the right term?)
-- g