rjf <fate...@gmail.com> writes: > On Sunday, September 29, 2013 9:53:07 AM UTC-7, Keshav Kini wrote: > > > > Could you elaborate on what relevance you see Sage having to > truth > maintenance and theorem proving? > > > Typically the people who work in these areas feel that they have a > great deal to > offer to mathematicians. See the MKM conference proceedings. They > also feel that they might make great use of computer algebra systems > or > other mathematics-oriented programs to assist in their activities. > So it > is potentially a 2-way street.
Hmm, OK. 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. But the above is just "as far as I know". My experience with theorem proving is mainly from the CS / PLT perspective, and I've never heard of MKM so clearly I don't have a sufficiently broad view of the subject. I'll endeavor to further edify myself. 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? -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.
