On Fri, May 25, 2012 at 3:23 AM, Freek Wiedijk <[email protected]> wrote:
> Hi Grant,
>
> >Are you familiar with Michael Beeson's MathXpert (formerly MathPert)?
>
> Yes, MathXpert-level mathematics is exactly what I had in
> mind when I was talking about "high school mathematics".
> The main difference between what MathXpert provides and what
> I was asking for, is that MathXpert is about simplifying
> expressions and solving equations, while what I was asking
> for is also to establish whether some statement (equation
> or inequality) follows from other statements.
>
OK, well I think this pretty well answers my question about Freek's paper.
Of course the problem domain of a proof assistant is much broader than the
job of a problem-solver and/or teaching aid for high school mathematics,
and that may make the technology improvements considerably harder to build.
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
