Added Semantic Tableaux. Improved pl_true

1. Added satisfiability checking using a Semantic Tableaux. Semantic tableaux removes the overhead of converting a formula to CNF (or DNF) and is faster than a SAT solver. However, it can only return True or False to indicate satisfiability, and not the model.
2. Modified pl_true to give the correct result under incomplete interpretations. Previously something like <code>pl_true(a >> (b >> a))</code> would return None. This function now accurately returns whether the value is obvious (True/False) or not (None).