grammar aussagenlogik;

// Standardtokens:
NUMBER: [0-9]+;
WHITESPACE: [ \r\n\t]+ -> skip;
LBRACE: '(';
RBRACE: ')';
LCURLYBRACE: '{';
RCURLYBRACE: '}';

// Symbole (erlaube mehrere Varianten)
SYMB_NOT:  ('!'|'~'|'not');
SYMB_AND:  ('&'+|'^'|'and');
SYMB_OR:   ('|'+|'v'|'or');
SYMB_IMPL: ('->'|'=>');

// Rules
start: open <EOF> | closed <EOF>;

closed: atomic | not | LBRACE open RBRACE;
open: and2 | and | or2 | or | implies;

// Schemata für atomische Ausdrücke
atomic: taut | contradiction | atom; //| generic;
taut:  ('1'|'true');
contradiction: ('0'|'false');
atom: 'A0' | 'A1' | 'A' NUMBER; // muss A0, A1 wegen falsum/verum extra auflisten
// // als 'generische' Formeln schreibe bspw. {F}, {G}, {F1}, usw.
// // generic: LCURLYBRACE (.*?) RCURLYBRACE;
// FIXME: dieses Schema führt zu Konflikten

// Schema für Negation: ¬ F
not:                symb=SYMB_NOT  closed;
// Schemata für Konjunktion: F1 ⋀ F2 bzw. F1 ⋀ F2 ⋀ ... ⋀ Fn
and2:      closed   symb=SYMB_AND  closed;
and:     ( closed ( symb=SYMB_AND  closed )+ );
// Schemata für Disjunktion: F1 ⋁ F2 bzw. F1 ⋁ F2 ⋁ ... ⋁ Fn
or2:       closed   symb=SYMB_OR   closed;
or:      ( closed ( symb=SYMB_OR   closed )+ );
// Schema für Implikation: F1 ⟶ F2
implies:   closed   symb=SYMB_IMPL closed;