42 lines
1.3 KiB
ANTLR
42 lines
1.3 KiB
ANTLR
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;
|