title: python modal logic K solver
body: <p>I am working on modal logic tableau solver which is implemented in python (2.7.5 version). 
  So I already have a function that translates an input string to tableau format that is: </p>
  
  <p><strong>Input：</strong> </p>
  
  <pre><code>~p ^ q
  </code></pre>
  
  <p><strong>Parsed:</strong> </p>
  
  <pre><code>['and',('not', 'p'), 'q']
  </code></pre>
  
  <p><strong>Parsed and alpha rule applied:</strong> </p>
  
  <pre><code>[('not', 'p'), 'q']
  </code></pre>
  
  <p>Now, I dealt with alpha formulas that is intersection, double negations etc.
  The problem that I am encountering now are the <em>beta formulas</em> , for example Union.</p>
  
  <p>For the Union formula I need to write a function that splits one list in two lists, so for example:</p>
  
  <p><strong>Input:</strong> </p>
  
  <pre><code>('and', 's', ('or', (not,'r'), 'q'))
  </code></pre>
  
  <p><strong>Outputs:</strong></p>
  
  <pre><code>1st list ('s',('not','r'))
  2nd list ('s','q')
  </code></pre>
  
  <p>I can easily do it once, but how can I recursively scan the formula and generate these list so that later I can scan them and verify whether they are closed or not? </p>
  
  <p>The final goal of this is to create a tableau solver which generates a graph that is a Model or return an answer that formula is unsatisfiable. </p>