%import common.WS
%import common.NUMBER
%import common.WORD

%ignore WS

// Schemata für Ausdrücke
// 'open'   = äußerste Klammern fehlen, wenn nötig.
// 'closed' = sonst
?expr:   open | closed
?closed: atomic | not | "(" open ")"
?open:   and | and_long | or | or_long | impl

// Schemata für atomische Ausdrücke
?atomic:  false | true | atom | generic
?false:   /0|false/                         -> kontr
?true:    /1|true/                          -> taut
?atom:    /A[0-9]+/                         -> atom
// als 'generische' Formeln schreibe bspw. {F}, {G}, {F1}, usw.
?generic: "{" /((?!({|})).)+/ "}"           -> beliebig

// Symbole (erlaube mehrere Varianten)
?symb_not:  /!|~|not/                       -> symb
?symb_and:  /&+|\^|and/                     -> symb
?symb_or:   /\|+|v|or/                      -> symb
?symb_impl: /->|=>/                         -> symb

// Schema für Negation: ¬ F
?not:                 symb_not  closed      -> neg
// Schemata für Konjunktion: F1 ⋀ F2 bzw. F1 ⋀ F2 ⋀ ... ⋀ Fn
?and:        closed   symb_and  closed      -> konj
?and_long: [ closed ( symb_and  closed )+ ] -> konj_lang
// Schemata für Disjunktion: F1 ⋁ F2 bzw. F1 ⋁ F2 ⋁ ... ⋁ Fn
?or:         closed   symb_or   closed      -> disj
?or_long:  [ closed ( symb_or   closed )+ ] -> disj_lang
// Schema für Implikation: F1 ⟶ F2
?impl:       closed   symb_impl closed      -> impl