logik2021/codego/grammars/aussagenlogik.g4

46 lines
1.4 KiB
ANTLR
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

grammar aussagenlogik;
// Standardtokens:
NUMBER: [0-9]+;
WHITESPACE: [ \r\n\t]+ -> skip;
LBRACE: '(';
RBRACE: ')';
LCURLYBRACE: '{';
RCURLYBRACE: '}';
TEXT: [a-zA-Z0-9\\_];
// Symbole (erlaube mehrere Varianten)
SYMB_NOT: ('!'|'~'|'not');
SYMB_AND: ('&'+|'^'|'and');
SYMB_OR: ('|'+|'v'|'or');
SYMB_IFF: ([<][-]+[>]|[<][=]+[>]|'iff');
SYMB_IMPL: (~[<][-]+[>]|~[<][=]+[>]);
// Rules
start: open <EOF> | closed <EOF>;
closed: atomic | not | LBRACE open RBRACE;
open: and2 | and | or2 | or | implies | iff;
// 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}, usw.
generic: LCURLYBRACE TEXT+ RCURLYBRACE | LCURLYBRACE TEXT* ( generic TEXT* )+ RCURLYBRACE;
// FIXME: liest Zahlen schlecht ein
// 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;
// Schema für Implikation: F1 ⟷ F2
iff: closed symb=SYMB_IFF closed;