python 模态逻辑 K 求解器

Question

我正在研究在 python（2.7.5 版本）中实现的模态逻辑画面求解器。所以我已经有了一个将输入字符串转换为画面格式的函数，即：

输入：

~p ^ q

已解析：

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

已解析并应用了 alpha 规则：

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

现在，我处理交集、双重否定等的 alpha 公式。我现在遇到的问题是 beta 公式 ，例如 Union.

对于 Union 公式，我需要编写一个将一个列表拆分为两个列表的函数，例如：

输入：

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

输出：

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

我一次就可以轻松完成，但是我如何递归扫描公式并生成这些列表，以便稍后我可以扫描它们并验证它们是否已关闭？

这个的最终目标是创建一个画面求解器，它生成一个图形，该图形是一个模型或 return 一个公式无法满足的答案。

Answer 1

这是一个非常有趣的项目:)。我自己现在正在写关于模态逻辑的论文。

首先，我建议您使用 InToHyLo 输入格式，这在现有求解器中是相当标准的。

InToHyLo 格式如下所示：

  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']+)

为了简化公式的解析并专注于真正的问题：求解实例。我建议您使用现有的解析器，例如 flex/bison。

通过互联网查找您的问题，（我远不是Python方面的专家）看起来库“http://pyparsing.wikispaces.com”是解析的参考。

之后，只需按如下方式使用 Bison，您的文件将被完全解析。

这是我的 Bison 文件（用于在求解器 C++ 中使用 Flex/Bison）：

/*
 *
 *  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(*); }
;

Formula:   BooleanFormula               { $$ = ; }
         | ModalFormula                 { $$ = ; }
         | UnaryFormula                 { $$ = ; }
         | LROUND Formula RROUND        { $$ = ; }
;

BooleanValue:   VALUE { $$ = new TermPtr( (Term*) new BooleanValue() ); }
;

PropositionalVariable:   IDENTIFIER { $$ = new TermPtr( (Term*) new PropositionalVar() ); }
;

BooleanFormula:   Formula BinaryBoolOperator Formula { 

                      $$ = new TermPtr( (Term*) new BooleanOp(*, *, ) );  /* can be (A OR B) or (A AND B) */
                      delete(); 
                      delete(); 
                  }

|                 Formula IMP Formula {

                      ()->Negate();
                      $$ = new TermPtr( (Term*) new BooleanOp(*, *, O_OR) ); /* A -> B can be written : (¬A v B) */
                      delete(); 
                      delete();
                  }

|                 PropositionalVariable IFF PropositionalVariable {

                      PropositionalVar *Copy1 = new PropositionalVar( *((PropositionalVar*)->getPtr()) );
                      PropositionalVar *Copy3 = new PropositionalVar( *((PropositionalVar*)->getPtr()) );

                      TermPtr Negated1( (Term*)Copy1, ->isNegated() ); 
                      TermPtr Negated3( (Term*)Copy3, ->isNegated() );

                      Negated1.Negate(); 
                      Negated3.Negate();

                      TermPtr Or1( (Term*) new BooleanOp(Negated1, *, O_OR) ); /* Or1 = (¬A v B) */
                      TermPtr Or2( (Term*) new BooleanOp(Negated3, *, O_OR) ); /* Or2 = (¬B v A) */

                      $$ = new TermPtr( (Term*) new BooleanOp(Or1, Or2, O_AND) ); /* We add : (Or1 AND OrB) */

                      delete(); 
                      delete();
                  }                           
;

ModalFormula:   ModalOperator LROUND Formula RROUND  {

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

                  $$ = new TermPtr( (Term*) new ModalOp(*, ) );
                  delete();
                }        
|
                ModalOperator UnaryFormula  {

                  $$ = new TermPtr( (Term*) new ModalOp(*, ) );
                  delete();
                }   
;

UnaryFormula:   BooleanValue                 { $$ = ; }

|               PropositionalVariable        { $$ = ; }

|
                UnaryBoolOperator UnaryFormula {

                  if ( == O_NOT) {
                    ()->Negate(); 
                  }                 

                  $$ = ; 
                }
|
                UnaryBoolOperator ModalFormula {

                  if ( == O_NOT) {
                    ()->Negate(); 
                  }                 

                  $$ = ; 
                }                
|
                UnaryBoolOperator LROUND Formula RROUND {

                  if ( == O_NOT) {
                    ()->Negate(); 
                  }                 

                  $$ = ; 
                }
;


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);   
}

通过调整它，您将能够完全递归地解析模态逻辑公式:)。

如果稍后，您想挑战现有画面求解器的求解器（例如 Spartacus）。不要忘记这些求解器几乎一直在回答最大的开放 Tableau，因此如果您想找到解决方案的 Kripke 模型，它们肯定会比您更快 ;)

我希望我能帮助你解决你的问题，我想少理论化，但不幸的是我没有掌握 python 这个 :/.

祝你的求解器一切顺利；

此致。

如果您接受我使用 InToHyLo 的提议，我最近在为模态逻辑 K 开发 Kripke 模型的检查器。您可以在这里找到：http://www.cril.univ-artois.fr/~montmirail/mdk-verifier/

最近发表于 PAAR'2016:

检查 Kripke 模型的模态逻辑 K，Jean-Marie Lagniez、Daniel Le Berre、Tiago de Lima 和 Valentin Montmirail，第五届实用研讨会论文集自动推理方面 (PAAR 2016)

Answer 2

这个问题已经有了我最初问题的选定答案。如果有人对大量不同模型逻辑的完整实现感兴趣，请阅读我的 report here。它包含很多细节，所以你不会迷路。

解析器本身的实现 (Python) 可以在我的 github repo here 中找到。代码的文档不是最好的，但如果你理解理论，你应该会发现它很容易，我希望 :)。

python 模态逻辑 K 求解器

python modal logic K solver

python

modal-logic