On Thursday, October 3, 2013 10:17:42 AM UTC-7, Keshav Kini wrote: > > rjf <fat...@gmail.com <javascript:>> writes: > > On Monday, September 30, 2013 11:42:43 PM UTC-7, Keshav Kini wrote: > > But as far as I know, Sage is not proof-aware in any way. > > > > Why would you necessarily know about this? > > I don't know, why would I? >
Why would you display both your ignorance of a subject as well as your apparent inability or unwillingness to learn about it. Maybe you should avoid posting a message beginning with "As far as I know". > > I am well aware > > that Maxima, a component of Sage, has been used to generate proofs. > > "Being used to generate proofs" is not the same as "proof-aware". > > > I guess you are not listening to the right theorem-proving people. > > Mm. > In your view is Sage "logic aware" or "polynomial aware"? > > > To return to my question, you mentioned Sage specifically as an > > example > > of a problem and a solution. I was wondering what you meant by > > that -- > > do you see Sage as posing and/or solving some particular theorem > > proving > > -related problem? > > > > I think you could spend some time with the Google... But if you need > > a particular pointer ... > > > > It has been shown that certain geometry theorem proofs can be reduced > > to algebra, > > http://en.wikipedia.org/wiki/Wu%27s_method_of_characteristic_set > > > > for some people the most prominent example among many connections > > between > > computer algebra and proofs. > > I see you have no interest in answering the question I actually asked, > so I'll leave it at that. Thanks anyway. > Oh, I thought that was a rhetorical question. Here it is again (Keshav said...) "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." How about "Interactive Theorem Proving, Automated Reasoning, and Mathematical Computation" by Jeremy Avigad which is the first of 221,000 hits from a search with terms {sage theorem proving computer} . using -- guess what -- the Google. And yes, Avigad mentions using Sage. RJF -- 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.
