logik2021/codego/grammars/aussagenlogik.g4

42 lines
1.3 KiB
Plaintext
Raw Normal View History

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;