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:
Input：
~p ^ q
['and',('not', 'p'), 'q']
[('not', 'p'), 'q']
('and', 's', ('or', (not,'r'), 'q'))
1st list ('s',('not','r'))
2nd list ('s','q')
It' a very interesting project :). I'm myself in thesis about modal logic right now.
I'm first of all, advising you to use the InToHyLo input format, which is quite a standard in the existing solvers.
The InToHyLo format is looking as follow:
file ::= ['begin'] dml ['end']
fml ::= '(' fml ')' (* parentheses *)
 '1'  'true'  'True'  'TRUE' (* truth *)
 '0'  'false'  'False'  'FALSE' (* falsehood *)
 '~' fml  '' fml (* negation *)
 '<>' fml  '<' id '>' fml (* diamonds *)
 '[]' fml  '[' id ']' fml (* boxes *)
 fml '&' fml (* conjunction *)
 fml '' fml (* disjunction *)
 fml '>' fml (* implication *)
 fml '<>' fml (* equivalence *)
 id (* prop. var. *)
where identifiers (id) are arbitrary nonempty alphanumeric sequences: (['A''Z' 'a''z' '0''9']+)
To simplify the parsing of your formula and to focus on the real problem : Solving the instance. I advise you to use an existing parser like flex/bison
.
By looking on Internet for your problem, (I'm far from being an expert in Python) it looks like the library "http://pyparsing.wikispaces.com" is the reference for parsing.
And after, just by using Bison as follow, your file will be fully parsed.
Here is my Bison file (for using Flex/Bison in a solver C++):
/*
*
* Compile with bison.
*/
/*** Code inserted at the begin of the file. ***/
%{
#include <stdlib.h>
#include <list>
#include "Formula.h"
// yylex exists
extern int yylex();
extern char yytext[];
void yyerror(char *msg);
%}
/*** Bison declarations ***/
%union
{
bool bval;
operator_t opval;
char *sval;
TermPtr *term;
}
%token LROUND RROUND
%left IFF
%left IMP
%left OR
%left AND
%right DIAMOND
%right BOX
%right NOT
%token VALUE
%token IDENTIFIER
%type<bval> VALUE
%type<sval> IDENTIFIER
%type<term> Formula BooleanValue BooleanFormula ModalFormula PropositionalVariable UnaryFormula
%type<opval> BinaryBoolOperator UnaryBoolOperator ModalOperator
%start Start
%%
Start:
 Formula { (Formula::getFormula()).setRoot(*$1); }
;
Formula: BooleanFormula { $$ = $1; }
 ModalFormula { $$ = $1; }
 UnaryFormula { $$ = $1; }
 LROUND Formula RROUND { $$ = $2; }
;
BooleanValue: VALUE { $$ = new TermPtr( (Term*) new BooleanValue($1) ); }
;
PropositionalVariable: IDENTIFIER { $$ = new TermPtr( (Term*) new PropositionalVar($1) ); }
;
BooleanFormula: Formula BinaryBoolOperator Formula {
$$ = new TermPtr( (Term*) new BooleanOp(*$1, *$3, $2) ); /* can be (A OR B) or (A AND B) */
delete($3);
delete($1);
}
 Formula IMP Formula {
($1)>Negate();
$$ = new TermPtr( (Term*) new BooleanOp(*$1, *$3, O_OR) ); /* A > B can be written : (¬A v B) */
delete($3);
delete($1);
}
 PropositionalVariable IFF PropositionalVariable {
PropositionalVar *Copy1 = new PropositionalVar( *((PropositionalVar*)$1>getPtr()) );
PropositionalVar *Copy3 = new PropositionalVar( *((PropositionalVar*)$3>getPtr()) );
TermPtr Negated1( (Term*)Copy1, $1>isNegated() );
TermPtr Negated3( (Term*)Copy3, $3>isNegated() );
Negated1.Negate();
Negated3.Negate();
TermPtr Or1( (Term*) new BooleanOp(Negated1, *$3, O_OR) ); /* Or1 = (¬A v B) */
TermPtr Or2( (Term*) new BooleanOp(Negated3, *$1, O_OR) ); /* Or2 = (¬B v A) */
$$ = new TermPtr( (Term*) new BooleanOp(Or1, Or2, O_AND) ); /* We add : (Or1 AND OrB) */
delete($3);
delete($1);
}
;
ModalFormula: ModalOperator LROUND Formula RROUND {
$$ = new TermPtr( (Term*) new ModalOp(*$3, $1) );
delete($3);
}

ModalOperator ModalFormula {
$$ = new TermPtr( (Term*) new ModalOp(*$2, $1) );
delete($2);
}

ModalOperator UnaryFormula {
$$ = new TermPtr( (Term*) new ModalOp(*$2, $1) );
delete($2);
}
;
UnaryFormula: BooleanValue { $$ = $1; }
 PropositionalVariable { $$ = $1; }

UnaryBoolOperator UnaryFormula {
if ($1 == O_NOT) {
($2)>Negate();
}
$$ = $2;
}

UnaryBoolOperator ModalFormula {
if ($1 == O_NOT) {
($2)>Negate();
}
$$ = $2;
}

UnaryBoolOperator LROUND Formula RROUND {
if ($1 == O_NOT) {
($3)>Negate();
}
$$ = $3;
}
;
ModalOperator: BOX { $$ = O_BOX; }
 DIAMOND { $$ = O_DIAMOND; }
;
BinaryBoolOperator: AND { $$ = O_AND; }
 OR { $$ = O_OR; }
;
UnaryBoolOperator: NOT { $$ = O_NOT; }
;
/*** Code inserted at the and of the file ***/
%%
void yyerror(char *msg)
{
printf("PARSER: %s", msg);
if (yytext[0] != 0)
printf(" near token '%s'\n", yytext);
else
printf("\n");
exit(1);
}
By adapting it, you will be able to parse fully and recursively a modal logic formula :).
And if later, you want to challenge your solver to existing tableau solver (like Spartacus for example). Dont forget that theses solvers are almost all the time, answering a maximal open Tableau, so they will be for sure faster that you if you want to find a Kripke model of the solution ;)
I hope I manage to help you with your question, I would like to be less theoretical, but I unfortunately don't master python for this :/.
Wish you the best with your solver;
Best Regards.
If you accept my proposition of using the InToHyLo, I worked recently on a Checker of Kripke models for the modal logic K. That you can find here: http://www.cril.univartois.fr/~montmirail/mdkverifier/
It has been published recently in PAAR'2016:
On Checking Kripke Models for Modal Logic K, JeanMarie Lagniez, Daniel Le Berre, Tiago de Lima, and Valentin Montmirail, Proceedings of the Fifth Workshop on Pratical Aspect of Automated Reasoning (PAAR 2016)