You'll have to forgive me, I'm still a bit of novice programmer (an enthusiastic novice), but can someone briefly explain what you all mean by "wrapping"? I quite agree that building a fully functional mechanical theorem prover is far from a feasible summer project. I guess I'm more interested in developing more basic functionality that could serve as a basis for moving in that direction. If replacing the SAT solver (I assume you're referring to the one in logic/ inference.py) is a priority, that's something I'd love to work on. Thank's, Christian, for pointing me to the Predicate class in assumptions/assume.py. Best, -Cullen
On Mar 23, 1:40 pm, Joachim Durchholz <j...@durchholz.org> wrote: > Am 23.03.2012 17:04, schrieb Christian Muise: > > > Aye, wrapping should be an obvious target (you could start by wrapping a > > SAT solver to replace the prototype implementation currently in there). If > > there's any simple theorem proving technique that could be implemented, > > it's good to have something fully written in SymPy as shipping other solves > > with the library isn't recommended. > > I'd start by defining some concrete use cases that this should support. > Preferrably some that aren't covered by Coq etc. - we don't want to > compete with established theorem provers, that's not SymPy's mission. -- You received this message because you are subscribed to the Google Groups "sympy" group. To post to this group, send email to sympy@googlegroups.com. To unsubscribe from this group, send email to sympy+unsubscr...@googlegroups.com. For more options, visit this group at http://groups.google.com/group/sympy?hl=en.
