Re: Mathematica Prove[...] Command Possible?
- To: mathgroup at smc.vnet.net
- Subject: [mg127998] Re: Mathematica Prove[...] Command Possible?
- From: "Bill Simpson" <bsimpson141421356 at gmail.com>
- Date: Sat, 8 Sep 2012 03:07:08 -0400 (EDT)
- Delivered-to: email@example.com
- Delivered-to: firstname.lastname@example.org
- Delivered-to: email@example.com
- Delivered-to: firstname.lastname@example.org
- References: <email@example.com> <firstname.lastname@example.org> <email@example.com> <firstname.lastname@example.org>
"amzoti" <amzoti at gmail.com> wrote in message news:k2cd0f$f46$1 at smc.vnet.net... > On Thursday, September 6, 2012 1:18:41 AM UTC-7, magma wrote: >> > > I have always been curious if Mathematica has ever considered a Prove >> > > command? >> >> > See: >> > http://www.risc.jku.at/research/theorema/description/ >> > Daniel >> >> As Daniel just pointed out, Theorema is the package you are looking >> for. It is in my opinion the BEST automatic theorem prover >> available...anywhere. The new upcoming version 2.0 promises to be >> spectacular! The current version 1.6 only works with Mathematica up to >> version >> 7. In addition to the link above, posted by Daniel, you can look also >> at: >> http://www.risc.jku.at/research/theorema/software/ > > Excellent, I am looking forward to seeing and using that! > > Will it be able to do all of these as well? > http://www.amazon.com/Mechanical-Geometry-Theorem-Mathematics-Applications/dp/9027726507 > Thanks ~A That book, and related books and journal articles, are describing a relatively powerful geometry theorem prover based on the work of Wen-tsun Wu which is often called the "China Prover." Google Wu "China Prover" to start to find the literature. People in the theorem proving community were surprised and impressed with the complexity of proofs that this prover cound handle. I believe there was a journalarticle titled "The Complete Method of Wu" tried to nail down all the last details of this. In the simplest form it depends on the user manually translating a geometry hypothesis into a sequence of algebraic equalities. The prover then calculates a sequence of multivariate polynomial remainders from those equalities and if the final remainder is zero then the conclusion is a linear combination of the premises and theorem is proven. The calculated coefficients of the linear combination give precise conditions for which the theorem holds. Decades ago Wu originally implemented this in Pascal. More recently it is claimed that this was easily implemented in another system, but I have never been able to find the code. I have wanted to get my hands on a working version of this prover for a long time. I suspect in the simplest form it might only be a page or two of Mathematica. In a more complete form there are issues of irreducibility that need to be addressed, but in many cases this is simple and for some proofs this does not arise at all. In the original form of the prover it was perhaps tedious to do the manual translation into the equalities. I have thought that perhaps another page of Mathematica might be enough to automate most of this. That translation is relatively straighforward. I keep meaning to try to implement the prover in Mathematica but I never get to this. If anyone is aware of an implementation or is up to writing a page or so of code to do this then it would provide a very simple powerful geometry theorem prover for Mathematica users.