Re: Intent to package: metamath
Marcus Brinkmann wrote:
> Fred wrote:
> > I personally don't like them but it should be possible to add
> > one which recognizes the MetaMath languge.
>
> Do you mean you don't like the "concept" of a proof finder in general or
> the mentioned proof finders in particular?
First off I am not a mathematician, so my opinions on this subject
are probably not worth much.
Bad choise of words on my part, "like" was misleading.
My attitude is strictly pragmatic and should not be construed to imply
that theorem provers are not useful, just not useful to me for what
I want to do now.
My interest in tools like MetaMath is specifically in helping me to
understand abstract mathematics, something which the theorem provers
are not intended for (at least not someone at my level).
But, if I were to see (for example) how theorem provers could help
in developing formal methods for proving program correctness
I would quickly become very interested.
> I think carefully analyzation of a proof finders result can give inspiration
> for new definitions or a new set of axioms... brute force won't work very
> well, but statistical evaluations could lead to results.
According to Norm <ndm@shore.net> (who does know something about
these issues) two well regarded systems are:
- Isabelle <http://www.cl.cam.ac.uk/Research/HVG/Isabelle/>
- Otter <http://www-unix.mcs.anl.gov/AR/otter/>
Note: Do NOT take this as an intent to package either of these by me.
Fred
Reply to: