Julien Puydt <julien.pu...@laposte.net> writes: > 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
Oh, thanks, of course you're right. If the CAS can generate certificates there's no problem. Many theorem provers seem to have the capability to farm out subcomputations to external systems, usually things like SAT solvers or what-have-you. I still don't see what theorem-proving-related problem and solution Sage already represents, though. Has anyone used it for anything theorem-proving related yet? I'd be interested to hear about it. -Keshav -- 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.
