On Tuesday, October 1, 2013 1:42:43 AM UTC-5, Keshav Kini wrote: > But as far as I know, Sage is not proof-aware in any way. I've never > heard theorem-proving people talk about making use of existing computer > algebra systems and I can't imagine how they could be useful in the > business of well-founded theorem proving when they are themselves not > verified.
Strictly FYI, Buchberger was talking about how he was using Mathematica as a base for the Theorema project over 10 years ago. http://www.ercim.eu/publication/Ercim_News/enw50/buchberger.html http://www.risc.jku.at/research/theorema/ He's shown off some pretty impressive stuff. If I could afford Mathematica (in terms of energy and time as well as money) I might be interested in learning about it. I have no idea how well-regarded Theorema is in that community, however. regards john perry -- You received this message because you are subscribed to the Google Groups "sage-devel" group. To unsubscribe from this group and stop receiving emails from it, send an email to sage-devel+unsubscr...@googlegroups.com. To post to this group, send email to sage-devel@googlegroups.com. Visit this group at http://groups.google.com/group/sage-devel. For more options, visit https://groups.google.com/groups/opt_out.
