36 lines
1.1 KiB
Plaintext
36 lines
1.1 KiB
Plaintext
|
%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
|