2021-05-09 18:22:30 +02:00
|
|
|
|
grammar aussagenlogik;
|
|
|
|
|
|
|
|
|
|
// Standardtokens:
|
2021-05-18 11:31:01 +02:00
|
|
|
|
NUMBER: [0-9];
|
|
|
|
|
ZERO: ~[a-zA-Z0-9][0]; // negatives Look-Behind nötig, um konfliktierendes Lexing zu vermeiden
|
|
|
|
|
ONE: ~[a-zA-Z0-9][1]; // ""
|
2021-05-09 18:22:30 +02:00
|
|
|
|
WHITESPACE: [ \r\n\t]+ -> skip;
|
|
|
|
|
LBRACE: '(';
|
|
|
|
|
RBRACE: ')';
|
|
|
|
|
LCURLYBRACE: '{';
|
|
|
|
|
RCURLYBRACE: '}';
|
2021-05-15 10:58:23 +02:00
|
|
|
|
TEXT: [a-zA-Z0-9\\_];
|
2021-05-09 18:22:30 +02:00
|
|
|
|
|
|
|
|
|
// Symbole (erlaube mehrere Varianten)
|
|
|
|
|
SYMB_NOT: ('!'|'~'|'not');
|
|
|
|
|
SYMB_AND: ('&'+|'^'|'and');
|
|
|
|
|
SYMB_OR: ('|'+|'v'|'or');
|
2021-05-15 00:05:03 +02:00
|
|
|
|
SYMB_IFF: ([<][-]+[>]|[<][=]+[>]|'iff');
|
|
|
|
|
SYMB_IMPL: (~[<][-]+[>]|~[<][=]+[>]);
|
2021-05-09 18:22:30 +02:00
|
|
|
|
|
|
|
|
|
// Rules
|
|
|
|
|
start: open <EOF> | closed <EOF>;
|
|
|
|
|
|
|
|
|
|
closed: atomic | not | LBRACE open RBRACE;
|
2021-05-15 00:05:03 +02:00
|
|
|
|
open: and2 | and | or2 | or | implies | iff;
|
2021-05-09 18:22:30 +02:00
|
|
|
|
|
|
|
|
|
// Schemata für atomische Ausdrücke
|
2021-05-15 10:58:23 +02:00
|
|
|
|
atomic: taut | contradiction | atom | generic;
|
2021-05-18 11:31:01 +02:00
|
|
|
|
taut: (ONE|'true');
|
|
|
|
|
contradiction: (ZERO|'false');
|
|
|
|
|
atom: 'A' NUMBER+;
|
2021-05-15 10:58:23 +02:00
|
|
|
|
// als 'generische' Formeln schreibe bspw. {F}, {G}, usw.
|
|
|
|
|
generic: LCURLYBRACE TEXT+ RCURLYBRACE | LCURLYBRACE TEXT* ( generic TEXT* )+ RCURLYBRACE;
|
|
|
|
|
// FIXME: liest Zahlen schlecht ein
|
2021-05-09 18:22:30 +02:00
|
|
|
|
|
|
|
|
|
// 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;
|
2021-05-15 00:05:03 +02:00
|
|
|
|
// Schema für Implikation: F1 ⟷ F2
|
|
|
|
|
iff: closed symb=SYMB_IFF closed;
|