Hi,
> > Minh, William and I just had a short conversation on #sage-devel about COQ
> > ( http://en.wikipedia.org/wiki/Coq ), then about SAT Solvers in Sage...
I just want to mention that on the contrary to what has been said on irc, the
primary goal of Coq is not to automatically prove thing but to helps people
proving things. Coq is not an automatic prover but a proof assistant... One
can prove very advanced things with it (eg: 4 colors theorem or a constructive
version of the proof that C is algebraically closed). I had some experiment to
see what is possible to do with it for proving combinatorics, and I'm
currently involved in a project where we are exploring how is it
possible/feasible/easy to certify combinatorics software.
Cheers,
Florent
--~--~---------~--~----~------------~-------~--~----~
To post to this group, send an email to sage-devel@googlegroups.com
To unsubscribe from this group, send an email to
sage-devel-unsubscr...@googlegroups.com
For more options, visit this group at http://groups.google.com/group/sage-devel
URL: http://www.sagemath.org
-~----------~----~----~----~------~----~------~--~---
