Java Antlr4 Logikgrammatik erster Ordnung

Question

Ich möchte Strings in Logik erster Ordnung analysieren und sie in eine bestimmte Klassenstruktur umwandeln. Zum Beispiel möchte ich eine Formel wie

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

und schalten Sie ihn in eine Universal-Klasse analysieren, die eine Variable-Feld und ein Formel quantifiedFormula Feld hat, die für den Rest der Formel steht. Ich habe Probleme mit der Grammatik. Wenn ich die Formel mit dem antlr analysieren Code generiert ich

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

'\ U2200' ∀ ist, \ u2203 heißt ∃ und \ u00ac heißt ¬, die Negation Zeichen.

Das ist meine Grammatikdatei. Ich habe es nach der FOL.g-Datei zusammengestellt, die auf der Website von antlr3 gefunden wurde. Ich benutze jedoch antl4.

Grammatik 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

Das scheint nicht überraschend.

Nach Ihrer Grammatik, ein formula ist eine gewisse Anzahl von exists und forall durch eine bidir gefolgt Klauseln. Wenn Sie die Produktionen für bidir verfolgen, wird klar, dass es mit einem negation starten muss und dass wiederum mit NOT beginnen muss. Während Sie also die formula scannen, müssen Sie Klauseln mit einem der drei Tokens EXISTS, FORALL oder NOT sehen.

Ihr negation muss die Möglichkeit enthalten, dass es keine Negation ist. Sie könnten zum Beispiel NOT optional machen.