On Tuesday, July 18, 2006 8:32 AM C Y wrote: > > Just saw an announcement on the Isabelle list > (http://www.macs.hw.ac.uk/~jbw/phd-student-ad.html) which > referenced this: > http://www.macs.hw.ac.uk/~fairouz/talks/talks2005/mathlang-general-talk. pdf > > I may be wrong, but it sounds like the problems they are > looking at there are a bit similar to the ones B-sharp is > intended to address.
It seems to me that goals of MathLang go way beyond BNatural (B# or B-sharp if you prefer). BNatural is a single-typed input language intended to replace or suppliment the existing Axiom interpreter, especially for new users of Axiom. MathLang on the other hand is apparently intended as a semi-formal middle ground between published mathematical text and a formal input language (such as BNatural, the Axiom Interpreter or an automated theorem proving system). Maybe some day this will be a possible input language for computer algebra systems, but it seems to me that having just learned to crawl, we should first set our sites on learning to walk before we try to run ... :) Regards, Bill Page. _______________________________________________ Axiom-developer mailing list [email protected] http://lists.nongnu.org/mailman/listinfo/axiom-developer
