rjf <fate...@gmail.com> 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? > 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. > 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. -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.
