[no subject]

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

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
>