aki aki - 4 months ago 14
Python Question

python modal logic K solver

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


Parsed:

['and',('not', 'p'), 'q']


Parsed and alpha rule applied:

[('not', 'p'), 'q']


Now, I dealt with alpha formulas that is intersection, double negations etc.
The problem that I am encountering now are the beta formulas , for example Union.

For the Union formula I need to write a function that splits one list in two lists, so for example:

Input:

('and', 's', ('or', (not,'r'), 'q'))


Outputs:

1st list ('s',('not','r'))
2nd list ('s','q')


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?

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.

Answer

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.univ-artois.fr/~montmirail/mdk-verifier/

It has been published recently in PAAR'2016:

On Checking Kripke Models for Modal Logic K, Jean-Marie Lagniez, Daniel Le Berre, Tiago de Lima, and Valentin Montmirail, Proceedings of the Fifth Workshop on Pratical Aspect of Automated Reasoning (PAAR 2016)