The boolean satisfiability problem

Most annoying problem in my implementation of the query system is that it will not solve implications if the implicates are far away from each other. For instance, if the graph of known facts is something like this

Integer ----> Rational --> Real --> Complex
  ^  ^
  |  |
  |   -------
  |         |
Prime      Even

Then it will not know …

Initial implementation of the query system

I sent some patches to sympy-patches with an initial implementation of the query system. You can check it out by pulling from my branch: git pull http://fa.bianp.net/git/sympy.git master into your sympy repo. Some examples of what you can do (sample isympy session): In [1 …

Assumption system and automatic theorem proving. Should I be learning LISP ?

This is the third time I attempt to write the assumption system. Other attempts could be described as me following the rule: “For any complex problem, there is always a solution that is simple, clear, and wrong.” My first attempt (although better than the current assumption system) did use very …

Google Summer of Code

First post on my GSOC adventure. This year I got accepted in Google's summer of code program as student, and my job will be to implement the assumptions framework in SymPy. Although the project officially is only about implementing an assumptions framework, I have to prepare the ground before the …