From fa286a6335c21cabd9554b4872a6e785057716e2 Mon Sep 17 00:00:00 2001
From: raj_mathe <raj.dahya@math.uni-leipzig.de>
Date: Sun, 9 May 2021 18:22:30 +0200
Subject: [PATCH] =?UTF-8?q?master=20>=20master:=20codego=20->=20schema=20h?=
 =?UTF-8?q?inzugef=C3=BCgt?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 codego/grammars/aussagenlogik.g4 | 41 ++++++++++++++++++++++++++++++++
 1 file changed, 41 insertions(+)
 create mode 100644 codego/grammars/aussagenlogik.g4

diff --git a/codego/grammars/aussagenlogik.g4 b/codego/grammars/aussagenlogik.g4
new file mode 100644
index 0000000..a37334a
--- /dev/null
+++ b/codego/grammars/aussagenlogik.g4
@@ -0,0 +1,41 @@
+grammar aussagenlogik;
+
+// Standardtokens:
+NUMBER: [0-9]+;
+WHITESPACE: [ \r\n\t]+ -> skip;
+LBRACE: '(';
+RBRACE: ')';
+LCURLYBRACE: '{';
+RCURLYBRACE: '}';
+
+// Symbole (erlaube mehrere Varianten)
+SYMB_NOT:  ('!'|'~'|'not');
+SYMB_AND:  ('&'+|'^'|'and');
+SYMB_OR:   ('|'+|'v'|'or');
+SYMB_IMPL: ('->'|'=>');
+
+// Rules
+start: open <EOF> | closed <EOF>;
+
+closed: atomic | not | LBRACE open RBRACE;
+open: and2 | and | or2 | or | implies;
+
+// 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}, {F1}, usw.
+// // generic: LCURLYBRACE (.*?) RCURLYBRACE;
+// FIXME: dieses Schema führt zu Konflikten
+
+// 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;