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.
On Fri, Mar 23, 2012 at 11:39 AM, Damien Desfontaines <[email protected] > wrote: > 2012/3/23 Cullen Seaton <[email protected]>: > > Alright, then in the interest of working towards proving theorems, it > seems > > like an appropriate starting place might be to implement predicates > (something > > of the form l(x, y) that reads as "x has property l with respect to y") > and > > then begin working on adding quantifiers. After all the absolute logic > is in > > place, I would be be interested in working more on logics with multiple > truth > > values (which I am admittedly a little less familiar with). I would also > like > > to begin by adding functions that can perform logical deduction. Does > this > > seem like an appropriate amount of work for the summer? Best regards, > > -Cullen > > A theorem verifyer and/or automatic prover seems to be a lot of work, in my > opinion : entire teams of researchers are needed to implement such > systems, like > Coq or Isabelle. Maybe you should consider making thoses systems interact > with > SymPy instead of re-coding everything ? > > Damien > > -- > You received this message because you are subscribed to the Google Groups > "sympy" group. > To post to this group, send email to [email protected]. > To unsubscribe from this group, send email to > [email protected]. > For more options, visit this group at > http://groups.google.com/group/sympy?hl=en. > > -- You received this message because you are subscribed to the Google Groups "sympy" group. To post to this group, send email to [email protected]. To unsubscribe from this group, send email to [email protected]. For more options, visit this group at http://groups.google.com/group/sympy?hl=en.
