0
一次論理で文字列を解析し、特定のクラス構造に変換したいと考えています。例えば、私は、このようなJava Antlr4一次論理文法
∀x∃y∃z((R(x,y) ∨ Px)→(Qx→(Px∧Zx)))
ような式を解析し、変数フィールドを持つユニバーサルクラスと式の残りの略式quantifiedFormulaフィールドにそれを有効にします。私は文法に悩まされています。私はANTLRでその式がコードを生成し解析するとき、私は
line 1:11 extraneous input '(' expecting {'\u2200', '\u2203', '\u00ac'}
'\ u2200は、' \ u2203 IS∃と\ u00ac IS¬、否定記号、∀で取得します。
これは私の文法ファイルです。私はantlr3サイトにあるFOL.gファイルに沿ってまとめました。私はantl4を使用しています。
文法FOL;
options{
language=Java;
output=AST;
ASTLabelType = CommonTree;
backtrack=true;
}
tokens{
PREDICATE,
FUNCTION
}
/*------------------------------------------------------------------
* PARSER RULES
*------------------------------------------------------------------*/
condition: formula EOF ;
formula
: (forall | exists)* bidir ;
forall : FORALL VARIABLE ;
exists : EXISTS VARIABLE ;
bidir : implication (BIDIR implication)*;
implication
: disjunction (IMPL disjunction)*;
disjunction
: conjunction (OR conjunction)* ;
conjunction
: negation (AND negation)* ;
negation
: NOT (predicate | LPAREN* formula RPAREN*) ;
predicate
: PREPOSITION predicateTuple (PREDICATE PREPOSITION predicateTuple)
| PREPOSITION ;
predicateTuple
: LPAREN term (',' term)* RPAREN ;
term : function | VARIABLE ;
function: CONSTANT functionTuple (FUNCTION CONSTANT functionTuple)
| CONSTANT;
functionTuple
: LPAREN (CONSTANT | VARIABLE) (',' (CONSTANT | VARIABLE))* RPAREN;
/*------------------------------------------------------------------
* LEXER RULES
*------------------------------------------------------------------*/
LPAREN: '(';
RPAREN: ')';
FORALL: '\u2200';
EXISTS: '\u2203';
NOT:'\u00ac';
IMPL: '\u2192';
BIDIR: '\u2194';
OR: '\u2228';
AND: '\u2227';
EQ: '=';
VARIABLE: (('q'..'z')) CHARACTER* ;
CONSTANT: (('a'..'p')) CHARACTER* ;
PREPOSITION: ('A'..'Z') CHARACTER* ;
fragment CHARACTER: ('a'..'z' | 'A'..'Z' | '_') ;
WS : (' ' | '\t' | '\r' | '\n')+ -> skip ;