Le 01/10/2013 08:42, Keshav Kini a écrit : > 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. If any CAS were to be used in such an endeavour I imagine it > would be something with a more principled code structure than Sage, like > Axiom. And indeed, Wikipedia tells me that there are plans to formalize > Axiom in Coq or ACL2.
A CAS need not be proof-aware to actually find relations, prove them and present proof-certificates ; for very specific and interesting examples, see the book "A=B" by Petrovsek, Wilf and Zeilberger, which is available in all good libraries, and also on: http://www.math.upenn.edu/~wilf/AeqB.html I must admit that reading the mathematica and maple examples was painful... does sage have those algorithms? Snark on #sagemath -- 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.
