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

%ignore WS

// Schemata für Ausdrücke
?expr:   open | closed
?closed: atomic | not | "(" open ")"
?open:   and | and2 | or | or2 | implies

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

// 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
// Schemata für Konjunktion: F1 ⋀ F2  bzw.  F1 ⋀ F2 ⋀ ... ⋀ Fn
?and2:      closed   symb_and  closed
?and:     [ closed ( symb_and  closed )+ ]
// Schemata für Disjunktion: F1 ⋁ F2  bzw.  F1 ⋁ F2 ⋁ ... ⋁ Fn
?or2:       closed   symb_or   closed
?or:      [ closed ( symb_or   closed )+ ]
// Schema für Implikation: F1 ⟶ F2
?implies:   closed   symb_impl closed