Java Antlr4 логика логики первого порядка

Question

Я хочу анализировать строки в логике первого порядка и превращать их в определенную структуру классов. Например, я хочу, чтобы разобрать формулу, такие как

∀x∃y∃z((R(x,y) ∨ Px)→(Qx→(Px∧Zx))) 

и превратить его в класс универсального, который имеет переменное поле и поле quantifiedFormula формулы, которая стоит для остальной части формулы. Однако у меня проблемы с грамматикой. Когда я анализирую, что формула с ANTLR сгенерированный код я получаю

line 1:11 extraneous input '(' expecting {'\u2200', '\u2203', '\u00ac'} 

'\ U2200' является ∀, \ u2203 есть ∃ и \ u00ac есть ¬, отрицанием знак.

Это мой файл грамматики. Я собрал его вместе с файлом FOL.g, найденным на сайте antlr3. Однако я использую 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 ; 

Answer 1

Это кажется неудивительным.

Согласно вашей грамматики, formula некоторое количество exists и forall статей, сопровождаемых bidir. Если вы проследите за производством для bidir, становится ясно, что он должен начинаться с negation и, в свою очередь, должен начинаться с NOT. Поэтому, пока вы сканируете formula, вы должны увидеть предложения, возглавляемые одним из трех токенов EXISTS, FORALL или NOT.

Ваш negation должен включать в себя возможность того, что это не отрицание. Вы можете, например, сделать NOT опциональным.