aki - 1 year ago 70
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.

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)

Recommended from our users: Dynamic Network Monitoring from WhatsUp Gold from IPSwitch. Free Download