The logic module is slowly becoming useful. This week I managed to get some basic inference in propositional logic working. This should be enough for the assumption sysmtem (although having first-order inference would be cool). You can pull from my branch: `` git pull http://fa.bianp.net/git/sympy.git logic`` Here are some examples of what it can do: First, importing and defining our symbols

In [1]: A, B, C = symbols('ABC')
In [2]: from sympy.logic import *

It works with Symbols just as you would expect

In [3]: And(A, B)
Out[3]: And(A, B)

It applies De Morgan Rules automatically

In [4]: Not(Or(A, B))
Out[4]: And(Not(A), Not(B))

converts to conjuntive normal form (CNF)

In [5]: to_cnf(Implies(A, And(B, C)))
Out[5]: And(Or(B, Not(A)), Or(C, Not(A)))

Some basic inference:

In [6]: pl_true( Or(A, B), {A : True})  # what can we say about Or(A, B) if A is True ?
Out[6]: True

In [7]: pl_true ( And(A, B), {B: False}) # what is And(A, B) if B is False
Out[7]: False

To be discussed: - I'm not sure if we should override &&, || on Symbol so that we can do A && B instead of And(A, B). If would make the code cleaner, but also I don't want to bloat Symbol any more. What do you think ? I'm very proud of this in the sense that it is a nice clean module that will hopefully serve as the foundation of the new assumption system.