[mizar] Re: your mail

[Andrea Asperti <asperti@cs.unibo.it>]

Oooops.
Sorry: I made a major mistake (an erroneous reply). 
That was meant to be a private mail to Freek.
Sorry again.

				
				-- andrea



On Wed, 18 Feb 2004, Andrea Asperti wrote:

> 
> Hi Freek, 
> 
> 	I was on the point of writing to Farmer for 
> AuthoMath, and I went to his home page to get his
> e-mail (e-male). However, I did not appreciate very
> much his 
> 
> 	"A September 11 Parable", 
> 
> so, I think I will not write him, after all. 
> No answer from Trybulec.
> 
> 				-- andrea
> 
> 
> 
> 
> 
> 
> On Fri, 16 Jan 2004, Freek Wiedijk wrote:
> 
> > Hi Piotr,
> > 
> > >> I think I agree with this.  With properly automated
> > >> computations you can throw away all of the AXIOMS and [X]REAL_*
> > >> and XCMPLX_* series of articles.  I _hate_ searching through
> > >> those articles for lemmas that I know are there, but that I
> > >> can't find.
> > >
> > >Searching these articles drives me nuts at times yet I do not see how
> > >you plan to eliminate them.  Could you elaborate please?
> > 
> > Well, the magic word is "decision procedures".  I learned
> > from a nice talk by Shanker (the big one of the PVS system, I
> > think it was at TPHOLs in Oregon) that that kind of
> > automation is the most important thing for a proof checker.
> > 
> > So for our library we wrote a tactic called "Rational" (which
> > is almost identical in functionality to another Coq tactic
> > called "Field") that can prove any equation that you can
> > establish by "multiplying out everything and bringing
> > everything under a common denominator".  For instance it can
> > prove for you that
> > 
> >   (x + y)^2 = x^2 + 2*x*y + y^2
> > 
> > I guess that in Mizar that's a theorem, but the point is that
> > you don't need to search for it: you just say "Rational" and
> > it's proved.
> > 
> > Now I realize that in the REAL_* etc. articles there is much
> > more than this (inequalities, equalities that need
> > assumptions, etc.) but you can easily imagine a decision
> > procedure that is a generalization of this "Rational" thing
> > and that _can_ do all the things in those articles.
> > 
> > The technical term for this is "quantifier elimination", I
> > think.  For real problems that is completely unpractical,
> > double exponential or so, but for the things from REAL_*
> > etc., I guess it will do very well.
> > 
> > So in Mizar you could image a "requirements QUANELIM" that
> > would give you this.
> > 
> > Freek
> > 
> 
>