Equational logic syntax

EqLogic.g4

grammar EqLogic;

predicate
 : predicate substitution
 | LPAREN predicate RPAREN
 | BOOLEAN
 | ID
 | NOT predicate
 | predicate IMPLY predicate
 | predicate AND   predicate
 | predicate OR    predicate
 | predicate EQUAL predicate (leibniz | equanimity)?
 ;

substitution: LBRACK ID (COMMA ID)* SUBSTITUTE predicate (COMMA predicate)* RBRACK ;
leibniz: LEIBNIZ ID DOT predicate ;
equanimity: EQUANIMITY predicate ;

SUBSTITUTE: ':=' ;
LEIBNIZ   : 'Leibniz' ;
EQUANIMITY: 'Equanimity' ;

BOOLEAN: TRUE | FALSE ;

LBRACK : '[' ;
RBRACK : ']' ;
LPAREN : '(' ;
RPAREN : ')' ;
DOT    : '.' ;
COMMA  : ',' ;

NOT  : '~' ;
IMPLY: '?' ;
AND  : '&' ;
OR   : '|' ;
EQUAL: '=' ;
TRUE : 'true' ;
FALSE: 'false' ;

ID: [a-z]+ ;

WS: [ \t\r\n]+ -> skip ;