sympy.logic - Part 2

(contd from last post)
Ok. A little late on this one. As promised, the part-2 about the features of sympy.logic, one of the lesser-used modules of sympy.logic. Today's post contains information about some stuff that was there before I worked on the module, and some stuff that we worked in. Anyways, here goes-

IV) Equality of boolean expressions

This is a function that became quite a headache for us while were trying to implement it. We thought of many algorithms and kept refuting them, until we settled on a good one. I coded it, and Christopher improved it (based on the SymPy architecture) considerably. It may still have a few bugs (one is right here), but it gets the job done nonetheless.

Lets take an example to see how it works
Take the function that I discussed in part I) of last post. Its SOP form was -
Or(And(Not(a), d), And(c, d))
and its POS form was-
And(Or(Not(a), c), d)
Lets take the POS form to be And(Or(Not(x), y), z), just to get a change of variables.

So, function1 = Or(And(Not(a), d), And(c, d)) and function2 = And(Or(Not(x), y), z)
According to the docstring of the bool_equal function, it "Returns True if the two expressions represent the same logical behavior for some correspondence between the variables of each (which may be different)"
In the above functions, the mapping a : x, c : y, d : z will give the SAME outputs for every input for the variables (a,c,d) or (x,y,z). How do we check this equality?

>>> from sympy.logic import *
>>> from sympy import symbols
>>> a, c, d, x, y, z = symbols('a c d x y z')      <- Remember all SymPy variables are called Symbols?
>>> function1 = Or(And(Not(a), d), And(c, d))
>>> function2 = And(Or(Not(x), y), z)
>>> bool_equal(function1, function2)

Output - True

Want to check the mapping?

>>> bool_equal(function1, function2, info = True)
(And(Or(Not(a), c), d), {c: y, a: x, d: z})

If there is more than one mapping which may make the expressions equal, any ONE is returned. The function that is returned as the first return is the simplified version of the functions (in terms of one set of variables). As the function is already the simplest here, it gets returned as it is.

V) Inferences from knowledge bases

This is a very handy feature of sympy.logic. It basically lets you 'tell it' a set of True boolean expressions, and then 'ask' it if a given input is True based on the 'knowledge' it has. First, let me introduce to two other logic classes in sympy.logic-

Implies

Implies(some expression, some expression)

Equivalent

Equivalent(some expression, some expression)

They behave exactly like the corresponding operators in logic theory. VERY useful when converting natural language statements to logic ones. They also let you convert them to And, Or and Not instances using simplify_logic or to_dnf or to_cnf functions.Ok, now about KBs-
The API is as follows-

>>> from sympy.logic.inference import PropKB
>>> from sympy.abc import x, y
>>> l = PropKB()
>>> l.tell(x & ~y)
>>> l.ask(x)
 True

Did you see what it did there? It returns True for any statement thats satisfiable given the statements it is 'told'.

One more thing.

One inefficient way to check if a statement y is valid given a set of statements x1, x2, ... xn is using the Implies class and simplify_logic.
Just use the following function -

def check_validity(statements, check):
      statements = simplify_logic(And(*statements))
output = simplify_logic(Implies(statements, check))
if output != True:
output = False
return statements, output

>>> check_validity([x|y], x)
(Or(x, y), False)

It will return the simplified version of the ANDing of all the statements in the first input, and the validity of the 'check' statement.

How did I use the above function in Database Systems? Put all the known functional dependencies in the 'statements' input and the dependency to be checked in the 'check' input (in the form of Implies objects). If the second output was not True, that would mean the functional dependency does not hold. Ofcourse there are better ways of doing this, but well, I had little time and I wanted to check some stuff pronto.

Anyways, thats all I have about sympy.logic. If you want to know more, the source is here. Do have a look.

GSoC update - 

The whole of last week was spent deciding the API of our work on frames, coordinate systems and vectors with Stefan, Prasoon and Gilbert. We have a consensus on some things now, and I am likely to start working this week on a new class to depict ScalarFields in n-dimensional space. I will post the progress by the end of next week, and I hope I will have substantial stuff to write about. Excited. Definitely. Cheers!