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