python modal logic K solver

Question

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 1

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)

Answer 2

This question already has a selected answer to my initial question. If someone would be interested in the full implementation of it for number of different model logics please read my report here. It contains a lot of details so you won't get lost.

The implementation of the parser itself (Python) can be found in my github repo here. The documentation for the code is not the best but if you understand the theory you should find it easy, I hope :).