master > master: protokoll woche 16

master > master: protokoll + READMEs überarbeitet
master > master: protokoll woche 15
2021-07-28 12:25:29 +02:00 · 2021-07-26 16:53:03 +02:00 · 2021-07-21 13:01:10 +02:00 · 2021-07-21 10:58:07 +02:00 · 2021-07-14 13:00:21 +02:00 · 2021-07-14 13:00:17 +02:00
65 changed files with 2663 additions and 924 deletions
--- a/.gitignore
+++ b/.gitignore
@@ -4,6 +4,8 @@

 !/docs
 !/notes
+!/notes/*.pdf
+!/notes/*.md
 !/protocol
 !/protocol/*.md

--- a/README.md
+++ b/README.md
@@ -4,11 +4,13 @@ Diese Repository ist für die Übungsgruppe am Mittwoch.

 - Protokolle findet man [hier](./protocol).
 - Notizen findet man [hier](./notes).
+- Symbolverzeichnis findet man in [notes/glossar.md](./notes/glossar.md).

 ## LaTeX ##

 Folgendes Einführungsvideo hat Emanuel erstellt <https://www.youtube.com/watch?v=HPUGlcZNG2k>.
-Alternativ kann es auch sinnvoll(er) mit Markdown/Pandocs zu arbeiten.
+<br>
+Alternativ zu LaTeX kann es evtl. sinnvoller sein, mit Markdown/Pandocs zu arbeiten.

 ## Wahrheitstabelle-Generator ##

@@ -23,3 +25,30 @@ Beispiele aus der Übung:

 Das Tool ist klug genug, um das Weglassen der äußersten Klammern
 und `A0 && A1 && A2` statt `((A0 && A1) && A2)` u. Ä. zu zulassen.
+
+## Zur Klausur ##
+
+- Datum: (siehe VL + Moodle)
+- Zulassung: TBA
+
+### Vorbereitung ###
+
+Empfehlung:
+
+1. die Definitionen + Resultate im den VL-Folien komplett durchgehen:
+    - prüfen, dass man die Hauptaspekte begreift;
+    - strikt zw. den paar Dingen, die wirklich zur Definition / zum Resultat gehören,
+        <br/>
+        und den Anmerkungen unterscheiden.
+2. in die assoziierten Übungsaufgaben schauen und sowohl die Lehre als auch die Anwendungen vertiefen;
+3. Stichpunkte von »häufigen Fehlern« (bspw. die man persönlich macht)
+    sowie »gewöhnlichen Missverständnissen« erstellen.
+
+Vor der Klausur gut ausschlafen und auf die Ernährung aufpassen.
+
+Während der Klausur:
+
+1. Keine Ablenkungen oder Kommunikationsquellen.
+2. Aufgaben sorgfältig durchlesen und auf Antwortformat achten (insbes. bei „leeren“ Feldern).
+3. Zeit gut managen. Mal muss man entscheiden _»Soll ich jetzt bei dieser Frage auf Kosten der anderen weitere Zeit verbringen, oder weitermachen und später darauf zurück kommen?«_
+4. Übersicht über Fortschritt vor Augen halten.
--- a/code/.gitignore
+++ b/code/.gitignore
@@ -1,12 +1,21 @@
 *
 !/.gitignore

-!/README.md
-!/build.sh
-!/test.sh
-
 !/data.env
-!/requirements
+!/README.md
+
+## Scripts
+!/scripts
+!/scripts/requirements
+!/scripts/build.sh
+!/scripts/test.sh
+
+## Für Erzeugung von Grammatiken:
+!/grammars
+!/grammars/README.md
+!/grammars/*.lark
+
+## Python Source
 !/aussagenlogik
 !/utests
 !/**/*.py
--- a/code/README.md
+++ b/code/README.md
@@ -6,24 +6,23 @@ Diese dienen nur zur Demonstration / konkreten Verwirklichung von Verfahren, die

 Der Gebrauch dieser Skripte unterliegt der Eigenverantwortung von Studierenden.

-Da ich kein Informatiker bin, sind auch einige Aspekt bestimmt nicht optimal programmiert/strukturiert.
+Da ich kein Informatiker bin,
+sind auch einige Aspekt bestimmt nicht optimal programmiert/strukturiert.
+Dafür kann jeder in seiner Kopie einfach alles anpassen.
+Das hier soll einfach funktionieren.

 ## Systemvoraussetzungen ##

 - bash (auch bash-for-windows).
 - python (mind. 3.9.x)

-Natürlich wäre eine Implementierung in einer besseren Sprache wie **go** idealer, aber vielleicht in Zukunft.
-
 ## Voreinstellungen ##

 - In einer bash-console zu diesem Ordner navigieren und folgenden Befehl ausführen:
    ```bash
-    chmod +x build.sh test.sh
-    ## oder
-    chmod +x *.sh
+    chmod +x scripts/*.sh
    ```
- In `build.sh` gibt es eine Zeile, die zur Ausführung der Python-Skripte notwendigen Module über PIP installieren lässt. (Die Liste der Packages findet man in der Datei `requirements`). Diese Zeile kann man ruhig nach der ersten Ausführung rauskommentieren.
+- In `scripts/build.sh` gibt es eine Zeile, die zur Ausführung der Python-Skripte notwendigen Module über PIP installieren lässt. (Die Liste der Packages findet man in der Datei `scripts/requirements`). Diese Zeile kann man ruhig nach der ersten Ausführung rauskommentieren.

 ## Daten ##

@@ -33,7 +32,7 @@ In `data.env` kann man Daten (aktuell: auszuwertenden Ausdruck + Interpretation/

 In einer bash-console zu diesem Ordner navigieren und
 ```bash
-./build.sh
+source scripts/build.sh
 ## oder (für Linux)
 python3 main.py
 ## oder (für Windows)
@@ -52,18 +51,24 @@ Probiere es mit Stift-und-Zettel und anhand von Beispielen die Werte händisch z

 ### Automatisierte Tests ###

-Wer etwas standardisierter seine Methoden testen will, kann automatisiertes Testing tätigen. Diese Tests sind im Unterordner `utests` eingetragen.
+Wer etwas standardisierter seine Methoden testen will, kann automatisiertes Testing tätigen.
+Diese Tests sind im Unterordner `utests` eingetragen und folgen dem Namensschema `..._test.py`.

 - In der Console (wenn noch nicht geschehen) folgenden Befehl einmalig ausführen:
    ```bash
-    chmod +x test.sh
+    chmod +x scripts/test.sh
    ```
- In `utests/u_rekursion.py` beim relevanten Testteil eine oder mehrere der Zeilen
+- In `utests/rekursion_test.py` beim relevanten Testteil eine oder mehrere der Zeilen
    ```python
    @unittest.skip('Methode noch nicht implementiert')
    ```
    rauskommentieren/löschen.
+- Jetzt
+    ```bash
+    source scripts/test.sh
+    ```
+    ausführen.

-Jetzt `test.sh` ausführen. Die unittests testen Methoden gegen mehrere vorkonstruierte Testfälle samt erwarteten Ergebnissen geprüft. Sollten einige Tests scheitern, dann Fehlermeldung durchlesen, und Methode entsprechend der Kritik überarbeiten.
+Die unit tests testen Methoden gegen mehrere vorkonstruierte Testfälle samt erwarteten Ergebnissen geprüft. Sollten einige Tests scheitern, dann Fehlermeldung durchlesen, und Methode entsprechend der Kritik überarbeiten.

-Die geschriebenen Unittests sind natürlich nicht ausführlich. Man kann diese nach Bedarf ergänzen. Am sinnvollsten baut man welche, die wirklich scheitern können, sonst sagen die Tests nichts aus.
+Die geschriebenen unit tests sind natürlich nicht ausführlich. Man kann diese nach Bedarf ergänzen. Am sinnvollsten baut man welche, die wirklich scheitern können, sonst sagen die Tests nichts aus.
--- a/code/aussagenlogik/grammar.lark
+++ b/code/aussagenlogik/grammar.lark
@@ -1,37 +0,0 @@
-%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
--- a/code/aussagenlogik/rekursion.py
+++ b/code/aussagenlogik/rekursion.py
@@ -5,21 +5,9 @@
 # IMPORTS
 # ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

-from __future__ import annotations
-from lark import Tree;
 from typing import List;

-from aussagenlogik.schema import isAtom;
-from aussagenlogik.schema import isBeliebig;
-from aussagenlogik.schema import isTrueSymbol;
-from aussagenlogik.schema import isFalseSymbol;
-from aussagenlogik.schema import isNegation;
-from aussagenlogik.schema import isConjunction;
-from aussagenlogik.schema import isLongConjunction;
-from aussagenlogik.schema import isDisjunction;
-from aussagenlogik.schema import isLongDisjunction;
-from aussagenlogik.schema import isImplication;
-from aussagenlogik.schema import SyntaxBaum;
+from aussagenlogik.syntaxbaum import SyntaxBaum;

 # ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 # GLOBALE KONSTANTEN
@@ -31,53 +19,69 @@ from aussagenlogik.schema import SyntaxBaum;
 # METHODEN
 # ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

-def rekursiv_eval(fml: SyntaxBaum, I: List[str]) -> int:
+def rekursivEval(fml: SyntaxBaum, I: List[str]) -> int:
    subfml = fml.children;
-    if isAtom(fml):
+    ########
+    # FÄLLE AUS DER VORLESUNG
+    ########
+    # Fall Atom
+    if fml.isAtom():
        name = fml.expr;
        return 1 if (name in I) else 0;
-    if isBeliebig(fml):
-        name = fml.expr;
-        return 1 if (name in I) else 0;
-    elif isTrueSymbol(fml):
-        return 1;
-    elif isFalseSymbol(fml):
-        return 0;
-    elif isNegation(fml):
-        val0 = rekursiv_eval(subfml[0], I);
+    # Fall ¬F
+    elif fml.isNegation():
+        val0 = rekursivEval(subfml[0], I);
        return 1 - val0;
-    elif isConjunction(fml):
-        val0 = rekursiv_eval(subfml[0], I);
-        val1 = rekursiv_eval(subfml[1], I);
+    # Fall F1 ⋀ F2
+    elif fml.isConjunction2():
+        val0 = rekursivEval(subfml[0], I);
+        val1 = rekursivEval(subfml[1], I);
        return min(val0, val1);
-    elif isLongConjunction(fml):
-        values = [rekursiv_eval(t, I) for t in subfml];
-        return min(values);
-    elif isDisjunction(fml):
-        val0 = rekursiv_eval(subfml[0], I);
-        val1 = rekursiv_eval(subfml[1], I);
+    # Fall F1 ⋁ F2
+    elif fml.isDisjunction2():
+        val0 = rekursivEval(subfml[0], I);
+        val1 = rekursivEval(subfml[1], I);
        return max(val0, val1);
-    elif isLongDisjunction(fml):
-        values = [rekursiv_eval(t, I) for t in subfml];
-        return max(values);
-    elif isImplication(fml):
-        val0 = rekursiv_eval(subfml[0], I);
-        val1 = rekursiv_eval(subfml[1], I);
+    ########
+    # WEITERE FÄLLE NICHT IN VORLESUNG
+    ########
+    # Sonderfall: generische Formel als Variable
+    if fml.isGeneric():
+        name = fml.expr;
+        return 1 if (name in I) else 0;
+    # Sonderfall: Tautologiesymbol
+    elif fml.isTautologySymbol():
+        return 1;
+    # Sonderfall: Kontradiktionssymbol
+    elif fml.isContradictionSymbol():
+        return 0;
+    # Fall Implikation: F1 ⟶ F2
+    elif fml.isImplication():
+        val0 = rekursivEval(subfml[0], I);
+        val1 = rekursivEval(subfml[1], I);
        return 0 if val0 == 1 and val1 == 0 else 1;
+    # Fall F1 ⋀ F2 ⋀ ... ⋀ Fn
+    elif fml.isConjunction():
+        values = [rekursivEval(t, I) for t in subfml];
+        return min(values);
+    # Fall F1 ⋁ F2 ⋁ ... ⋁ Fn
+    elif fml.isDisjunction():
+        values = [rekursivEval(t, I) for t in subfml];
+        return max(values);
    raise Exception('Evaluation nicht möglich!');

-def rekursiv_atoms(fml: Tree) -> List[str]:
+def rekursivAtoms(fml: SyntaxBaum) -> List[str]:
    ## Herausforderung: schreibe diese Funktion!
    return [];

-def rekursiv_depth(fml: Tree) -> int:
+def rekursivDepth(fml: SyntaxBaum) -> int:
    ## Herausforderung: schreibe diese Funktion!
    return 0;

-def rekursiv_length(fml: Tree) -> int:
+def rekursivLength(fml: SyntaxBaum) -> int:
    ## Herausforderung: schreibe diese Funktion!
    return 0;

-def rekursiv_parentheses(fml: Tree) -> int:
+def rekursivParentheses(fml: SyntaxBaum) -> int:
    ## Herausforderung: schreibe diese Funktion!
    return 0
--- a/code/aussagenlogik/schema.py
+++ b/code/aussagenlogik/schema.py
@@ -6,8 +6,6 @@
 # ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

 from __future__ import annotations;
-# install: lark; lark-parser; lark-parser[regex].
-# https://lark-parser.readthedocs.io/en/latest/grammar.html
 from lark import Lark;

 from aussagenlogik.syntaxbaum import SyntaxBaum;
@@ -16,10 +14,10 @@ from aussagenlogik.syntaxbaum import SyntaxBaum;
 # GLOBALE KONSTANTEN
 # ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

-## lexer
-with open('aussagenlogik/grammar.lark', 'r') as fp:
+# lexer durch LARK erzeugen
+with open('grammars/aussagenlogik.lark', 'r') as fp:
    grammar = ''.join(fp.readlines());
-    lexerAussagenlogik = Lark(grammar, start='expr', regex=True);
+    lexer = Lark(grammar, start='expr', regex=True);

 # ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 # METHODE: string -> Syntaxbaum
@@ -27,43 +25,6 @@ with open('aussagenlogik/grammar.lark', 'r') as fp:

 def stringToSyntaxbaum(expr: str) -> SyntaxBaum:
    try:
-        return SyntaxBaum(lexerAussagenlogik.parse(expr));
+        return SyntaxBaum(lexer.parse(expr));
    except:
        raise Exception('Ausdruck \033[1m{}\033[0m konnte nicht erkannt werden!'.format(expr));
-
-# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-# METHODEN: Erkennung von Formeltypen
-# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-def isAtom(fml: SyntaxBaum) -> bool:
-    return fml.kind == 'atom';
-
-def isLiteral(fml: SyntaxBaum) -> bool:
-    return isAtom(fml) or (isNegation(fml) and isAtom(fml.child));
-
-def isBeliebig(fml: SyntaxBaum) -> bool:
-    return fml.kind == 'beliebig';
-
-def isTrueSymbol(fml: SyntaxBaum) -> bool:
-    return fml.kind == 'taut';
-
-def isFalseSymbol(fml: SyntaxBaum) -> bool:
-    return fml.kind == 'kontr';
-
-def isNegation(fml: SyntaxBaum) -> bool:
-    return fml.kind == 'neg';
-
-def isConjunction(fml: SyntaxBaum) -> bool:
-    return fml.kind == 'konj';
-
-def isLongConjunction(fml: SyntaxBaum) -> bool:
-    return fml.kind in ['konj', 'konj_lang'];
-
-def isDisjunction(fml: SyntaxBaum) -> bool:
-    return fml.kind == 'disj';
-
-def isLongDisjunction(fml: SyntaxBaum) -> bool:
-    return fml.kind in ['disj', 'disj_lang'];
-
-def isImplication(fml: SyntaxBaum) -> bool:
-    return fml.kind == 'impl';
--- a/code/aussagenlogik/syntaxbaum.py
+++ b/code/aussagenlogik/syntaxbaum.py
@@ -6,7 +6,7 @@
 # ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

 from __future__ import annotations;
-from lark import Tree;
+from lark import Tree as larkTree;
 from typing import Generator;
 from typing import List;

@@ -21,37 +21,31 @@ from typing import List;
 # ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

 class SyntaxBaum(object):
-    expr: str;
    kind: str;
+    expr: str;
+    valence: int;
    children: List[SyntaxBaum];
-    tree: Tree;

-    def __init__(self, fml: Tree):
+    def __init__(self, fml: larkTree):
        self.kind = fml.data;
-        if len(fml.children) == 1 and isinstance(fml.children[0], str):
-            self.expr = fml.children[0];
-            self.children = [];
-            self.tree = Tree(self.kind, fml.children);
-        else:
-            self.children = [ SyntaxBaum(child) for child in fml.children if isinstance(child, Tree) and child.data != 'symb' ];
-            self.tree = Tree(self.kind, [child.tree for child in self.children]);
-            signature_parts = [];
-            i = 0;
-            for subfml in fml.children:
-                if isinstance(subfml, str):
-                    signature_parts.append(subfml);
-                elif subfml.data == 'symb':
-                    symb = str(subfml.children[0]);
-                    signature_parts.append(symb);
-                else:
-                    signature_parts.append('{{{}}}'.format(i));
-                    i += 1;
-            signature = ' '.join(signature_parts);
-            self.expr = signature.format(*self.children);
-            if self.kind in [ 'konj', 'konj_lang', 'disj', 'disj_lang', 'impl' ]:
-                lbrace = '(' if self.expr.startswith('(') else '( ';
-                rbrace = ')' if self.expr.endswith(')') else ' )';
-                self.expr = lbrace + self.expr + rbrace;
+        self.children = [];
+        self.valence = 0;
+        expr_parts = []
+        for child in fml.children:
+            if isinstance(child, str):
+                expr_parts.append(child);
+            ## subfml is instance larkTree:
+            elif child.data == 'symb':
+                symb = str(child.children[0]);
+                expr_parts.append(symb);
+            else:
+                subtree = SyntaxBaum(child);
+                self.children.append(subtree);
+                self.valence += 1;
+                expr_parts.append(subtree.expr);
+        self.expr = ' '.join(expr_parts);
+        if self.valence > 1:
+            self.expr = '(' + self.expr + ')';
        return;

    def __str__(self):
@@ -65,5 +59,58 @@ class SyntaxBaum(object):
    def child(self) -> SyntaxBaum:
        return self.children[0];

-    def pretty(self):
-        return self.tree.pretty(indent_str='- ');
+    # ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+    # METHOD: Pretty
+    # ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+    def pretty(self, preindent: str = '', tab: str = '  ', prepend: str = '', depth: int = 0) -> str:
+        indent = preindent + tab*depth;
+        if self.valence == 0 and self.kind in [ 'atom', 'generic' ]:
+            return indent + prepend + self.kind + ' ' + self.expr;
+        return '\n'.join(
+            [indent + prepend + self.kind] \
+            + [subtree.pretty(preindent, tab, '|__ ', depth+1) for subtree in self.children]
+        );
+
+    # ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+    # METHODS: Erkennung von Formeltypen
+    # ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+    def isIrreducible(self) -> bool:
+        return self.valence == 0;
+
+    def isAtom(self) -> bool:
+        return self.kind == 'atom';
+
+    def isLiteral(self) -> bool:
+        return self.isAtom() or (self.isNegation() and self.child.isAtom());
+
+    def isGeneric(self) -> bool:
+        return self.kind == 'generic';
+
+    def isTautologySymbol(self) -> bool:
+        return self.kind == 'taut';
+
+    def isContradictionSymbol(self) -> bool:
+        return self.kind == 'contradiction';
+
+    def isConnective(self) -> bool:
+        return self.valence > 0;
+
+    def isNegation(self) -> bool:
+        return self.kind == 'not';
+
+    def isConjunction2(self) -> bool:
+        return self.kind == 'and2';
+
+    def isConjunction(self) -> bool:
+        return self.kind in ['and', 'and2'];
+
+    def isDisjunction2(self) -> bool:
+        return self.kind == 'or2';
+
+    def isDisjunction(self) -> bool:
+        return self.kind in ['or', 'or2'];
+
+    def isImplication(self) -> bool:
+        return self.kind == 'implies';
--- a/code/grammars/README.md
+++ b/code/grammars/README.md
@@ -0,0 +1,9 @@
+# LARK #
+
+Die Grammatik wird hier in `.lark` Format präsentiert und gelext+geparsed.
+Für Python braucht man `lark`, `lark-parser`, `lark-parser[regex]` über **PIP** zu installieren.
+Siehe
+<https://lark-parser.readthedocs.io/en/latest/grammar.html>
+und
+<https://github.com/lark-parser/lark>
+für mehr Informationen zu **LARK**.
--- a/code/grammars/aussagenlogik.lark
+++ b/code/grammars/aussagenlogik.lark
@@ -0,0 +1,35 @@
+%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
--- a/code/main.py
+++ b/code/main.py
@@ -17,11 +17,11 @@ sys.path.insert(0, os.getcwd());

 from aussagenlogik.schema import stringToSyntaxbaum;
 from aussagenlogik.syntaxbaum import SyntaxBaum;
-from aussagenlogik.rekursion import rekursiv_eval;
-from aussagenlogik.rekursion import rekursiv_atoms;
-from aussagenlogik.rekursion import rekursiv_depth;
-from aussagenlogik.rekursion import rekursiv_length;
-from aussagenlogik.rekursion import rekursiv_parentheses;
+from aussagenlogik.rekursion import rekursivEval;
+from aussagenlogik.rekursion import rekursivAtoms;
+from aussagenlogik.rekursion import rekursivDepth;
+from aussagenlogik.rekursion import rekursivLength;
+from aussagenlogik.rekursion import rekursivParentheses;

 # ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 # GLOBALE KONSTANTEN
@@ -37,17 +37,17 @@ def main():
    ## Daten einlesen:
    expr, I = getData();
    ## Formel in Teilformeln zerlegen:
-    fml = stringToSyntaxbaum(expr);
+    tree = stringToSyntaxbaum(expr);
    ## Methoden ausführen:
    results = dict(
-        eval  = rekursiv_eval(fml, I),
-        atoms = rekursiv_atoms(fml),
-        d     = rekursiv_depth(fml),
-        l     = rekursiv_length(fml),
-        p     = rekursiv_parentheses(fml),
+        eval         = rekursivEval(tree, I),
+        atoms        = rekursivAtoms(tree),
+        depth        = rekursivDepth(tree),
+        length       = rekursivLength(tree),
+        nParentheses = rekursivParentheses(tree),
    );
    ## Resultate anzeigen:
-    display_results(expr, fml, I, results);
+    display_results(tree, I, results);
    return;

 # ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -60,22 +60,23 @@ def getData():
    I = eval(data['interpretation'] or '[]');
    return expr, I;

-def display_results(expr: str, fml: SyntaxBaum, I: List[str], results: dict):
+def display_results(tree: SyntaxBaum, I: List[str], results: dict):
    print(dedent(
        '''
        Syntaxbaum von
-            F := \033[92;1m{F}\033[0m:
-        '''.format(F=fml)
+        F := \033[92;1m{expr}\033[0m:
+        '''.format(expr=tree.expr)
    ));
-    print(fml.pretty());
+    print(tree.pretty('    '))
    print(dedent(
        '''
+
        Für I = [{I}] und F wie oben gilt
        eval(F, I)      = \033[94;1m{eval}\033[0m,
        \033[2matoms(F)        = \033[94;1m{atoms}\033[0m; \033[91;1m<- *\033[0m
-        \033[2mdepth(F)        = \033[94;1m{d}\033[0m;  \033[91;1m<- *\033[0m
-        \033[2mlength(F)       = \033[94;1m{l}\033[0m;  \033[91;1m<- *\033[0m
-        \033[2m#parentheses(F) = \033[94;1m{p}\033[0m;  \033[91;1m<- *\033[0m
+        \033[2mdepth(F)        = \033[94;1m{depth}\033[0m; \033[91;1m<- *\033[0m
+        \033[2mlength(F)       = \033[94;1m{length}\033[0m; \033[91;1m<- *\033[0m
+        \033[2m#parentheses(F) = \033[94;1m{nParentheses}\033[0m; \033[91;1m<- *\033[0m

        \033[91;1m*\033[0m \033[2mnoch nicht implementiert!\033[0m
        \033[1;2;4mChallenge:\033[0m \033[2mschreibe diese Methoden! (siehe README.md)\033[0m
--- a/code/scripts/build.sh
+++ b/code/scripts/build.sh
@@ -13,7 +13,7 @@ function call_python() {
 }

 function check_requirements() {
-    call_python -m pip install "$( cat requirements )" >> /dev/null;
+    call_python -m pip install "$( cat scripts/requirements )" >> /dev/null;
 }

 function run_code() {
--- a/code/scripts/requirements
+++ b/code/scripts/requirements
--- a/code/scripts/test.sh
+++ b/code/scripts/test.sh
@@ -13,12 +13,12 @@ function call_python() {
 }

 function check_requirements() {
-    call_python -m pip install "$( cat requirements )" >> /dev/null;
+    call_python -m pip install "$( cat scripts/requirements )" >> /dev/null;
 }

 function run_unittests(){
    echo -e "\033[1mUNITTESTS\033[0m\n";
-    local output="$(call_python -m unittest discover -v --top-level-directory "." --start-directory "utests" --pattern "u_*.py" 2>&1)";
+    local output="$(call_python -m unittest discover -v --top-level-directory "." --start-directory "utests" --pattern "*_test.py" 2>&1)";
    echo -e "$output";
    if ( echo "$output" | grep -E -q "^[[:space:]]*(FAIL:|FAILED)" ); then
        echo -e "[\033[91;1mERROR\033[0m] Unit tests versagt!" && return 1;
--- a/code/utests/rekursion_test.py
+++ b/code/utests/rekursion_test.py
@@ -9,11 +9,11 @@ import unittest;
 from unittest import TestCase;

 from aussagenlogik.schema import stringToSyntaxbaum;
-from aussagenlogik.rekursion import rekursiv_atoms;
-from aussagenlogik.rekursion import rekursiv_depth;
-from aussagenlogik.rekursion import rekursiv_length;
-from aussagenlogik.rekursion import rekursiv_parentheses;
-from aussagenlogik.rekursion import rekursiv_eval;
+from aussagenlogik.rekursion import rekursivEval;
+from aussagenlogik.rekursion import rekursivAtoms;
+from aussagenlogik.rekursion import rekursivDepth;
+from aussagenlogik.rekursion import rekursivLength;
+from aussagenlogik.rekursion import rekursivParentheses;

 # ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 # GLOBALE KONSTANTEN
@@ -29,34 +29,34 @@ from aussagenlogik.rekursion import rekursiv_eval;
 class TestRekursivEval(TestCase):
    def test_literale(self):
        fml = stringToSyntaxbaum('A0');
-        val = rekursiv_eval(fml, [ 'A0' ]);
+        val = rekursivEval(fml, [ 'A0' ]);
        assert val == 1;
        fml = stringToSyntaxbaum('A0');
-        val = rekursiv_eval(fml, []);
+        val = rekursivEval(fml, []);
        assert val == 0;
        fml = stringToSyntaxbaum('! A0');
-        val = rekursiv_eval(fml, [ 'A0' ]);
+        val = rekursivEval(fml, [ 'A0' ]);
        assert val == 0;
        fml = stringToSyntaxbaum('! A0');
-        val = rekursiv_eval(fml, []);
+        val = rekursivEval(fml, []);
        assert val == 1;

    def test_complex1(self):
        fml = stringToSyntaxbaum('( ! A0 || (( A0 && A3 ) || A2 ))');
-        val = rekursiv_eval(fml, [ 'A0', 'A2' ]);
+        val = rekursivEval(fml, [ 'A0', 'A2' ]);
        assert val == 1;
-        val = rekursiv_eval(fml, [ 'A0', 'A3' ]);
+        val = rekursivEval(fml, [ 'A0', 'A3' ]);
        assert val == 1;
-        val = rekursiv_eval(fml, [ 'A0' ]);
+        val = rekursivEval(fml, [ 'A0' ]);
        assert val == 0;
-        val = rekursiv_eval(fml, [ 'A4', 'A8' ]);
+        val = rekursivEval(fml, [ 'A4', 'A8' ]);
        assert val == 1;

    def test_complex2(self):
        fml = stringToSyntaxbaum('( ! A0 || (( A0 && A3 ) || ! A2 ))');
-        val = rekursiv_eval(fml, [ 'A0', 'A2' ]);
+        val = rekursivEval(fml, [ 'A0', 'A2' ]);
        assert val == 0;
-        val = rekursiv_eval(fml, [ 'A0', 'A3' ]);
+        val = rekursivEval(fml, [ 'A0', 'A3' ]);
        assert val == 1;
    pass;

@@ -68,22 +68,22 @@ class TestRekursivEval(TestCase):
 class TestRekursivAtoms(TestCase):
    def test_noduplicates(self):
        fml = stringToSyntaxbaum('( A4 && ( A4 || A4 ))');
-        val = sorted(rekursiv_atoms(fml));
+        val = sorted(rekursivAtoms(fml));
        assert len([_ for _ in val if _ == 'A4']) == 1, 'Atome dürfen nicht mehrfach vorkommen!';

    def test_nononatoms(self):
        fml = stringToSyntaxbaum('( {F} || A3 )');
-        val = sorted(rekursiv_atoms(fml));
+        val = sorted(rekursivAtoms(fml));
        assert 'F' not in val, 'Nichtatomare Formeln dürfen nicht vorkommen!';

    def test_calc1(self):
        fml = stringToSyntaxbaum('A0');
-        val = sorted(rekursiv_atoms(fml));
+        val = sorted(rekursivAtoms(fml));
        assert val == ['A0'], 'computed {}'.format(val);

    def test_calc2(self):
        fml = stringToSyntaxbaum('((( ! A0 && A3 ) || A4 ) && A8 )');
-        val = sorted(rekursiv_atoms(fml));
+        val = sorted(rekursivAtoms(fml));
        assert val == ['A0', 'A3', 'A4', 'A8'], 'computed {}'.format(val);
    pass;

@@ -95,27 +95,27 @@ class TestRekursivAtoms(TestCase):
 class TestRekursivDepth(TestCase):
    def test_calc1(self):
        fml = stringToSyntaxbaum('A0');
-        val = rekursiv_depth(fml);
+        val = rekursivDepth(fml);
        assert val == 0, 'computed {}'.format(val);

    def test_calc2(self):
        fml = stringToSyntaxbaum('!! A8');
-        val = rekursiv_depth(fml);
+        val = rekursivDepth(fml);
        assert val == 2, 'computed {}'.format(val);

    def test_calc3(self):
        fml = stringToSyntaxbaum('( ! A0 && A3 )');
-        val = rekursiv_depth(fml);
+        val = rekursivDepth(fml);
        assert val == 2, 'computed {}'.format(val);

    def test_calc4(self):
        fml = stringToSyntaxbaum('((( ! A0 && A3 ) || A4 ) && A8 )');
-        val = rekursiv_depth(fml);
+        val = rekursivDepth(fml);
        assert val == 4, 'computed {}'.format(val);

    def test_calc5(self):
        fml = stringToSyntaxbaum('! ((( ! A0 && A3 ) || A4 ) && A8 )');
-        val = rekursiv_depth(fml);
+        val = rekursivDepth(fml);
        assert val == 5, 'computed {}'.format(val);
    pass;

@@ -127,27 +127,27 @@ class TestRekursivDepth(TestCase):
 class TestRekursivLength(TestCase):
    def test_calc1(self):
        fml = stringToSyntaxbaum('A0');
-        val = rekursiv_length(fml);
+        val = rekursivLength(fml);
        assert val == 1, 'computed {}'.format(val);

    def test_calc2(self):
        fml = stringToSyntaxbaum('!! A8');
-        val = rekursiv_length(fml);
+        val = rekursivLength(fml);
        assert val == 3, 'computed {}'.format(val);

    def test_calc3(self):
        fml = stringToSyntaxbaum('( ! A0 && A3 )');
-        val = rekursiv_length(fml);
+        val = rekursivLength(fml);
        assert val == 4, 'computed {}'.format(val);

    def test_calc4(self):
        fml = stringToSyntaxbaum('((( ! A0 && A3 ) || A4 ) && A8 )');
-        val = rekursiv_length(fml);
+        val = rekursivLength(fml);
        assert val == 8, 'computed {}'.format(val);

    def test_calc5(self):
        fml = stringToSyntaxbaum('! ((( ! A0 && A3 ) || A4 ) && A8 )');
-        val = rekursiv_length(fml);
+        val = rekursivLength(fml);
        assert val == 9, 'computed {}'.format(val);
    pass;

@@ -159,26 +159,26 @@ class TestRekursivLength(TestCase):
 class TestRekursivParentheses(TestCase):
    def test_calc1(self):
        fml = stringToSyntaxbaum('A0');
-        val = rekursiv_parentheses(fml);
+        val = rekursivParentheses(fml);
        assert val == 0, 'computed {}'.format(val);

    def test_calc2(self):
        fml = stringToSyntaxbaum('!! A8');
-        val = rekursiv_parentheses(fml);
+        val = rekursivParentheses(fml);
        assert val == 0, 'computed {}'.format(val);

    def test_calc3(self):
        fml = stringToSyntaxbaum('( ! A0 && A3 )');
-        val = rekursiv_parentheses(fml);
+        val = rekursivParentheses(fml);
        assert val == 2, 'computed {}'.format(val);

    def test_calc4(self):
        fml = stringToSyntaxbaum('((( ! A0 && A3 ) || A4 ) && A8 )');
-        val = rekursiv_parentheses(fml);
+        val = rekursivParentheses(fml);
        assert val == 6, 'computed {}'.format(val);

    def test_calc5(self):
        fml = stringToSyntaxbaum('! ((( ! A0 && A3 ) || A4 ) && A8 )');
-        val = rekursiv_parentheses(fml);
+        val = rekursivParentheses(fml);
        assert val == 6, 'computed {}'.format(val);
    pass;
--- a/codego/.gitignore
+++ b/codego/.gitignore
@@ -3,22 +3,27 @@

 !/data.env
 !/README.md
-!/build.sh
-!/test.sh
+
+## Scripts
+!/scripts
+!/scripts/requirements
+!/scripts/build.sh
+!/scripts/build.sh
+!/scripts/test.sh
+
+## Für Erzeugung von Grammatiken:
+!/grammars
+!/grammars/README.md
+!/grammars/*.g4

 ## Go Source
 !/aussagenlogik
-!/aussagenlogik/rekursion
+!/aussagenlogik/recursion
 !/aussagenlogik/schema
-!/aussagenlogik/syntaxbaum
+!/aussagenlogik/formulae
 !/core
 !/core/environment
 !/core/utils
-!/grammars
 !/**/*.go
 !/go.mod
 !/go.sum
-
-## Für Erzeugung von Grammatiken:
-!/grammars/README.md
-!/grammars/*.g4
--- a/codego/README.md
+++ b/codego/README.md
@@ -6,25 +6,31 @@ Diese dienen nur zur Demonstration / konkreten Verwirklichung von Verfahren, die

 Der Gebrauch dieser Skripte unterliegt der Eigenverantwortung von Studierenden.

-Da ich kein Informatiker bin, sind auch einige Aspekt bestimmt nicht optimal programmiert/strukturiert.
+Da ich kein Informatiker bin,
+sind auch einige Aspekt bestimmt nicht optimal programmiert/strukturiert.
+Dafür kann jeder in seiner Kopie einfach alles anpassen.
+Das hier soll einfach funktionieren.

 ## Systemvoraussetzungen ##

 - bash (auch bash-for-windows).
 - golang (mind. 1.6.x)
- Java11
+- Java8+
+
+Um Schemata in Lexer und Parser zu verwandeln, wird **ANTLR4** gebraucht,
+(welches wiederum mithilfe eines Java-Archives kompiliert wird, weshalb man Java benötigt).
+Siehe
+<https://blog.gopheracademy.com/advent-2017/parsing-with-antlr4-and-go/>
+für weitere Informationen dazu.

-Dieses Projekt macht von ANTLR4 Gebrauch, um Schemata in Lexer und Parser zu verwandeln. Siehe <https://blog.gopheracademy.com/advent-2017/parsing-with-antlr4-and-go/> für mehr Informationen dazu.
 ## Voreinstellungen ##

 - In einer bash-console zu diesem Ordner navigieren und folgenden Befehl ausführen:
    ```bash
-    chmod +x build.sh test.sh
-    ## oder
-    chmod +x *.sh
+    chmod +x scripts/*.sh
    ```
- In `build.sh` gibt es eine Zeile, die zur Kompilierung des Go-Projektes notwendigen Module über **go** installieren lässt.
-(Die Liste der Packages findet man in der Datei `requirements`).
+- In `scripts/build.sh` gibt es eine Zeile, die zur Kompilierung des Go-Projektes notwendigen Module über **go** installieren lässt.
+(Die Liste der Packages findet man in der Datei `scripts/requirements`).
 Diese Zeile kann man ruhig nach der ersten Ausführung rauskommentieren.
 - Dazu kommt, dass **antlr4.jar** heruntergeladen wird.
 Mithilfe dieses Java-Archivs werden aus `grammars/*.g4` go-Skripte für die Grammatik erzeugt.
@@ -37,7 +43,7 @@ In `data.env` kann man Daten (aktuell: auszuwertenden Ausdruck + Interpretation/

 In einer bash-console zu diesem Ordner navigieren und
 ```bash
-./build.sh
+source scripts/build.sh
 ## oder
 go build main.go && ./main
 ```
@@ -56,11 +62,9 @@ compile_programme;
 run_programme;
 ```

-
-
 ## Offene Challenges ##

-In der Datei `aussagenlogik/rekursion.go` (relativ zu diesem Ordner) findet man mehrere leere Methoden (mit dem Kommentar `// Herausforderung...`). Wer es mag, kann versuchen, an seinem Rechner diese Methoden zu definieren und auszuprobieren.
+In dem Ordner `aussagenlogik/recursion` (relativ zum aktuellen Ordner) findet man mehrere leere Methoden (mit dem Kommentar `// Herausforderung...`). Wer es mag, kann versuchen, an seinem Rechner diese Methoden zu definieren und auszuprobieren.

 ### Händisch testen ###

@@ -68,18 +72,25 @@ Probiere es mit Stift-und-Zettel und anhand von Beispielen die Werte händisch z

 ### Automatisierte Tests ###

-Wer etwas standardisierter seine Methoden testen will, kann automatisiertes Testing tätigen. Diese Tests existieren parallel zu jedem Modul und folgen dem Namensschema `..._test.go`.
+Wer etwas standardisierter seine Methoden testen will, kann automatisiertes Testing tätigen.
+Diese Tests existieren parallel zu jedem Modul und folgen dem Namensschema `..._test.go`.

 - In der Console (wenn noch nicht geschehen) folgenden Befehl einmalig ausführen:
    ```bash
-    chmod +x test.sh
+    chmod +x scripts/test.sh
    ```
- In `aussagenlogik/rekursion/rekursion_test.go` beim relevanten Testteil eine oder mehrere der Zeilen
+- In `aussagenlogik/recursion/recursion_test.go` beim relevanten Testteil eine oder mehrere der Zeilen
    ```go
    test.Skip("Methode noch nicht implementiert")
    ```
    rauskommentieren/löschen.
+- Jetzt
+    ```bash
+    source scripts/test.sh
+    ```
+    ausführen.

-Jetzt `test.sh` ausführen. Die unittests testen Methoden gegen mehrere vorkonstruierte Testfälle samt erwarteten Ergebnissen geprüft. Sollten einige Tests scheitern, dann Fehlermeldung durchlesen, und Methode entsprechend der Kritik überarbeiten.
+Die unittests testen Methoden gegen mehrere vorkonstruierte Testfälle samt erwarteten Ergebnissen geprüft.
+Sollten einige Tests scheitern, dann Fehlermeldung durchlesen, und Methode entsprechend der Kritik überarbeiten.

 Die geschriebenen Unittests sind natürlich nicht ausführlich. Man kann diese nach Bedarf ergänzen. Am sinnvollsten baut man welche, die wirklich scheitern können, sonst sagen die Tests nichts aus.
--- a/codego/aussagenlogik/formulae/formulae_advanced.go
+++ b/codego/aussagenlogik/formulae/formulae_advanced.go
@@ -0,0 +1,178 @@
+package formulae
+
+import "logik/core/utils"
+
+/* ---------------------------------------------------------------- *
+ * METHOD Get Atoms
+ * ---------------------------------------------------------------- */
+
+func schemeGetAtoms(fml Formula, prevValues [](*[]Formula)) *[]Formula {
+	if fml.IsAtom() {
+		return &[]Formula{fml.Copy()}
+	} else {
+		var results = []Formula{}
+		for _, prevValue := range prevValues {
+			results = append(results, *prevValue...)
+		}
+		return &results
+	}
+}
+
+var fnGetAtoms = CreateFromSchemeFmlsValued(schemeGetAtoms)
+
+func (fml Formula) GetAtoms() []Formula {
+	return *fnGetAtoms(fml)
+}
+
+/* ---------------------------------------------------------------- *
+ * TYPE FormulaPair, FormulaPairs
+ * ---------------------------------------------------------------- */
+
+type FormulaPair struct {
+	Pos Formula
+	Neg Formula
+}
+
+type FormulaPairs []FormulaPair
+
+/* ---------------------------------------------------------------- *
+ * Methods for FormulaPairs
+ * ---------------------------------------------------------------- */
+
+func NewFormulaPairs(pairs []FormulaPair) FormulaPairs { return pairs }
+
+func (pairs FormulaPairs) Pos() []Formula {
+	var fmls = make([]Formula, len(pairs))
+	for i, pair := range pairs {
+		fmls[i] = pair.Pos
+	}
+	return fmls
+}
+
+func (pairs FormulaPairs) Neg() []Formula {
+	var fmls = make([]Formula, len(pairs))
+	for i, pair := range pairs {
+		fmls[i] = pair.Neg
+	}
+	return fmls
+}
+
+/* ---------------------------------------------------------------- *
+ * TYPE KNF, DNF, Horn
+ * ---------------------------------------------------------------- */
+
+type FormulaConjunct []Formula
+type FormulaDisjunct []Formula
+type FormulaKNF []FormulaDisjunct
+type FormulaDNF []FormulaConjunct
+type FormulaHornClause struct {
+	Pos FormulaDisjunct
+	Neg FormulaConjunct
+}
+type FormulaHorn []FormulaHornClause
+
+/* ---------------------------------------------------------------- *
+ * Methods for KNF, DNF, Horn
+ * ---------------------------------------------------------------- */
+
+func (fml FormulaDisjunct) ToFormula() Formula {
+	return Disjunction(fml)
+}
+
+func (fml FormulaConjunct) ToFormula() Formula {
+	return Conjunction(fml)
+}
+
+func (fml FormulaKNF) ToFormula() Formula {
+	var termsAsFormulae = make([]Formula, len(fml))
+	for i, term := range fml {
+		termsAsFormulae[i] = term.ToFormula()
+	}
+	return Conjunction(termsAsFormulae)
+}
+
+func (fml FormulaDNF) ToFormula() Formula {
+	var termsAsFormulae = make([]Formula, len(fml))
+	for i, term := range fml {
+		termsAsFormulae[i] = term.ToFormula()
+	}
+	return Disjunction(termsAsFormulae)
+}
+
+func (fml FormulaHornClause) ToFormula() Formula {
+	return Implies(fml.Neg.ToFormula(), fml.Pos.ToFormula())
+}
+
+func (fml FormulaHorn) ToFormula() Formula {
+	var hornclausesAsFormulae = make([]Formula, len(fml))
+	for i, hornclause := range fml {
+		hornclausesAsFormulae[i] = hornclause.ToFormula()
+	}
+	return Conjunction(hornclausesAsFormulae)
+}
+
+func getAtomsFromArrayOfLiterals(fmls []Formula) []string {
+	var atoms = []string{}
+	var m = map[string]bool{}
+	for _, fml := range fmls {
+		if fml.IsLiteral() {
+			m[fml.GetName()] = true
+		}
+	}
+	for name, _ := range m {
+		atoms = append(atoms, name)
+	}
+	utils.SortStrings(&atoms)
+	return atoms
+}
+
+func getAtomsFromArrayOfArraysOfLiterals(fmlArrays [][]Formula) []string {
+	var atoms = []string{}
+	var m = map[string]bool{}
+	for _, fmls := range fmlArrays {
+		for _, atom := range getAtomsFromArrayOfLiterals(fmls) {
+			m[atom] = true
+		}
+	}
+	for name, _ := range m {
+		atoms = append(atoms, name)
+	}
+	utils.SortStrings(&atoms)
+	return atoms
+}
+
+func (fml FormulaConjunct) GetAtoms() []string {
+	return getAtomsFromArrayOfLiterals(fml)
+}
+
+func (fml FormulaDisjunct) GetAtoms() []string {
+	return getAtomsFromArrayOfLiterals(fml)
+}
+
+func (fml FormulaHornClause) GetAtoms() []string {
+	return getAtomsFromArrayOfArraysOfLiterals([][]Formula{fml.Pos, fml.Neg})
+}
+
+func (fml FormulaKNF) GetAtoms() []string {
+	var fmlArrays = make([][]Formula, len(fml))
+	for i, term := range fml {
+		fmlArrays[i] = term
+	}
+	return getAtomsFromArrayOfArraysOfLiterals(fmlArrays)
+}
+
+func (fml FormulaDNF) GetAtoms() []string {
+	var fmlArrays = make([][]Formula, len(fml))
+	for i, term := range fml {
+		fmlArrays[i] = term
+	}
+	return getAtomsFromArrayOfArraysOfLiterals(fmlArrays)
+}
+
+func (fml FormulaHorn) GetAtoms() []string {
+	var fmlArrays = make([][]Formula, 2*len(fml))
+	for i, hornclause := range fml {
+		fmlArrays[i] = append(hornclause.Neg, hornclause.Pos...)
+	}
+	return getAtomsFromArrayOfArraysOfLiterals(fmlArrays)
+}
--- a/codego/aussagenlogik/formulae/formulae_basic.go
+++ b/codego/aussagenlogik/formulae/formulae_basic.go
@@ -0,0 +1,151 @@
+package formulae
+
+import (
+	"fmt"
+	"strings"
+)
+
+/* ---------------------------------------------------------------- *
+ * TYPE Formula
+ * ---------------------------------------------------------------- */
+
+type Formula struct {
+	kind        string
+	name        string
+	expr        string
+	valence     int
+	subformulae [](*Formula)
+}
+
+/* ---------------------------------------------------------------- *
+ * METHODS
+ * ---------------------------------------------------------------- */
+
+func (fml *Formula) SetKind(kind string) { fml.kind = kind }
+
+func (fml Formula) GetKind() string { return fml.kind }
+
+func (fml *Formula) SetExpr(expr string) { fml.expr = expr }
+
+func (fml Formula) GetExpr() string { return fml.expr }
+
+func (fml Formula) GetName() string { return fml.name }
+
+func (fml *Formula) SetSubformulae(subFmls [](*Formula)) {
+	fml.subformulae = subFmls
+	fml.valence = len(subFmls)
+}
+
+func (fml Formula) GetSubFormulae() []Formula {
+	var n int = fml.valence
+	var subFmls = make([]Formula, n)
+	for i, subFml := range fml.subformulae {
+		subFmls[i] = *subFml
+	}
+	return subFmls
+}
+
+func (fml Formula) GetAllSubFormulae() []Formula {
+	var subFml = fml.GetSubFormulae()
+	var result = []Formula{fml.Copy()}
+	for _, child := range subFml {
+		result = append(result, child.GetAllSubFormulae()...)
+	}
+	return result
+}
+
+func (fml Formula) GetAllSubFormulaeStrict() []Formula {
+	var subFml = fml.GetSubFormulae()
+	var result = []Formula{}
+	for _, child := range subFml {
+		result = append(result, child.GetAllSubFormulae()...)
+	}
+	return result
+}
+
+func (fml Formula) GetChild(indexOpt ...int) Formula {
+	var index int = 0
+	if len(indexOpt) > 0 {
+		index = indexOpt[0]
+	}
+	var subFml Formula
+	if 0 <= index && index < fml.valence {
+		subFml = *(fml.subformulae[index])
+	} else {
+		panic(fmt.Sprintf("Instance has no child of index %d !", index))
+	}
+	return subFml
+}
+
+func (fml Formula) Pretty(preindentOpt ...string) string {
+	var preindent string = ""
+	if len(preindentOpt) > 0 {
+		preindent = preindentOpt[0]
+	}
+	return fml.pretty(preindent, "  ", "", 0)
+}
+
+func (fml Formula) pretty(preindent string, tab string, prepend string, depth int) string {
+	var indent string = preindent + strings.Repeat(tab, depth)
+	switch fml.valence {
+	case 0:
+		switch kind := fml.kind; kind {
+		case "atom", "generic":
+			return indent + prepend + kind + " " + fml.expr
+		default:
+			return indent + prepend + kind
+		}
+	default:
+		var lines string = indent + prepend + fml.kind
+		prepend = "|__ "
+		for _, subFml := range fml.subformulae {
+			lines += "\n" + subFml.pretty(preindent, tab, prepend, depth+1)
+		}
+		return lines
+	}
+}
+
+// shallow copy
+func (fml Formula) Copy() Formula {
+	return Formula{
+		expr:        fml.expr,
+		kind:        fml.kind,
+		valence:     fml.valence,
+		subformulae: fml.subformulae,
+	}
+}
+
+func (fml Formula) Deepcopy() Formula {
+	var subFmls = make([](*Formula), len(fml.subformulae))
+	for i, subFml := range fml.subformulae {
+		subFmlCopy := subFml.Deepcopy()
+		subFmls[i] = &subFmlCopy
+	}
+	return Formula{
+		expr:        fml.expr,
+		kind:        fml.kind,
+		valence:     fml.valence,
+		subformulae: subFmls,
+	}
+}
+
+/* ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *
+ * METHODS: Recognition of Formula-Types
+ * ---------------------------------------------------------------- */
+
+func (fml Formula) IsIrreducible() bool         { return fml.valence == 0 }
+func (fml Formula) IsAtom() bool                { return fml.kind == "atom" }
+func (fml Formula) IsPositiveLiteral() bool     { return fml.IsAtom() }
+func (fml Formula) IsNegativeLiteral() bool     { return fml.IsNegation() && fml.GetChild().IsAtom() }
+func (fml Formula) IsLiteral() bool             { return fml.IsPositiveLiteral() || fml.IsNegativeLiteral() }
+func (fml Formula) IsGeneric() bool             { return fml.kind == "generic" }
+func (fml Formula) IsTautologySymbol() bool     { return fml.kind == "taut" }
+func (fml Formula) IsContradictionSymbol() bool { return fml.kind == "contradiction" }
+func (fml Formula) IsConnective() bool          { return fml.valence > 0 }
+func (fml Formula) IsNegation() bool            { return fml.kind == "not" }
+func (fml Formula) IsConjunction2() bool        { return fml.kind == "and2" }
+func (fml Formula) IsConjunction() bool         { return fml.kind == "and" || fml.kind == "and2" }
+func (fml Formula) IsDisjunction2() bool        { return fml.kind == "or2" }
+func (fml Formula) IsDisjunction() bool         { return fml.kind == "or" || fml.kind == "or2" }
+func (fml Formula) IsImplication() bool         { return fml.kind == "implies" }
+func (fml Formula) IsDoubleImplication() bool   { return fml.kind == "iff" }
--- a/codego/aussagenlogik/formulae/formulae_construction.go
+++ b/codego/aussagenlogik/formulae/formulae_construction.go
@@ -0,0 +1,147 @@
+package formulae
+
+/* ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *
+ * CONSTANTS
+ * ---------------------------------------------------------------- */
+
+var Tautology = Formula{
+	kind:        "taut",
+	expr:        "1",
+	valence:     0,
+	subformulae: [](*Formula){},
+}
+
+var Contradiction = Formula{
+	kind:        "contradiction",
+	expr:        "0",
+	valence:     0,
+	subformulae: [](*Formula){},
+}
+
+/* ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *
+ * METHODS: Constructions
+ * ---------------------------------------------------------------- */
+
+func Atom(name string) Formula {
+	return Formula{
+		kind:        "atom",
+		name:        name,
+		expr:        name,
+		valence:     0,
+		subformulae: [](*Formula){},
+	}
+}
+
+func NegatedAtom(name string) Formula {
+	return Negation(Atom(name))
+}
+
+func Generic(name string) Formula {
+	return Formula{
+		kind:        "generic",
+		name:        name,
+		expr:        "{" + name + "}",
+		valence:     0,
+		subformulae: [](*Formula){},
+	}
+}
+
+func Negation(fml Formula) Formula {
+	var name string
+	if fml.IsAtom() {
+		name = fml.GetName()
+	}
+	var expr = fml.expr
+	expr = "!" + expr
+	return Formula{
+		kind:        "not",
+		name:        name, // preserves name of negated atoms
+		expr:        expr,
+		valence:     1,
+		subformulae: [](*Formula){&fml},
+	}
+}
+
+func Conjunction2(fml1 Formula, fml2 Formula) Formula {
+	return Formula{
+		kind:        "and2",
+		expr:        "(" + fml1.expr + " && " + fml2.expr + ")",
+		valence:     2,
+		subformulae: [](*Formula){&fml1, &fml2},
+	}
+}
+
+func Conjunction(fmls []Formula) Formula {
+	switch len(fmls) {
+	case 0:
+		return Tautology
+	case 1:
+		return fmls[0]
+	}
+	var expr string = ""
+	var subFmls = make([](*Formula), len(fmls))
+	for i, fml := range fmls {
+		(func(i int, subFml Formula) { subFmls[i] = &subFml })(i, fml)
+		if i > 0 {
+			expr += " && "
+		}
+		expr += fml.expr
+	}
+	return Formula{
+		kind:        "and",
+		expr:        "(" + expr + ")",
+		valence:     len(subFmls),
+		subformulae: subFmls,
+	}
+}
+
+func Disjunction2(fml1 Formula, fml2 Formula) Formula {
+	return Formula{
+		kind:        "or2",
+		expr:        "(" + fml1.expr + " || " + fml2.expr + ")",
+		valence:     2,
+		subformulae: [](*Formula){&fml1, &fml2},
+	}
+}
+
+func Disjunction(fmls []Formula) Formula {
+	switch len(fmls) {
+	case 0:
+		return Contradiction
+	case 1:
+		return fmls[0]
+	}
+	var expr string = ""
+	var subFmls = make([](*Formula), len(fmls))
+	for i, fml := range fmls {
+		(func(i int, subFml Formula) { subFmls[i] = &subFml })(i, fml)
+		if i > 0 {
+			expr += " || "
+		}
+		expr += fml.expr
+	}
+	return Formula{
+		kind:        "or",
+		expr:        "(" + expr + ")",
+		valence:     len(subFmls),
+		subformulae: subFmls,
+	}
+}
+
+func Implies(fml1 Formula, fml2 Formula) Formula {
+	return Formula{
+		kind:        "implies",
+		expr:        "(" + fml1.expr + " -> " + fml2.expr + ")",
+		valence:     2,
+		subformulae: [](*Formula){&fml1, &fml2},
+	}
+}
+
+func DoubleImplication(fml1 Formula, fml2 Formula) Formula {
+	return Formula{
+		kind:        "iff",
+		expr:        "(" + fml1.expr + " <-> " + fml2.expr + ")",
+		valence:     2,
+		subformulae: [](*Formula){&fml1, &fml2},
+	}
+}
--- a/codego/aussagenlogik/formulae/formulae_generate.go
+++ b/codego/aussagenlogik/formulae/formulae_generate.go
@@ -0,0 +1,165 @@
+package formulae
+
+// NOTE: GoLang hat noch keine generics. Erst 2022.
+
+/* ---------------------------------------------------------------- *
+ * Generate int-value FN from scheme
+ * ---------------------------------------------------------------- */
+
+func CreateFromSchemeIntValued(scheme func(fml Formula, prevValues []int) int) func(fml Formula) int {
+	var fn func(fml Formula) int
+	var subFn = func(ch chan int, subFml Formula) { ch <- fn(subFml) }
+	fn = func(fml Formula) int {
+		var subFmls = fml.GetSubFormulae()
+		var n = len(subFmls)
+		var subChan = make([](chan int), n)
+		var prevValues = make([]int, len(subFmls))
+		// start parallel computations on subformulas
+		for i, subFml := range subFmls {
+			subChan[i] = make(chan int) // create Channel, since currently nil
+			go subFn(subChan[i], subFml)
+		}
+		// successively read values
+		for i := 0; i < n; i++ {
+			prevValues[i] = <-subChan[i]
+		}
+		// apply schema to get value for formula
+		return scheme(fml, prevValues)
+	}
+	return fn
+}
+
+/* ---------------------------------------------------------------- *
+ * Generate string-value FN from scheme
+ * ---------------------------------------------------------------- */
+
+func CreateFromSchemeStringValued(scheme func(fml Formula, prevValues []string) string) func(fml Formula) string {
+	var fn func(fml Formula) string
+	var subFn = func(ch chan string, subFml Formula) { ch <- fn(subFml) }
+	fn = func(fml Formula) string {
+		var subFmls = fml.GetSubFormulae()
+		var n = len(subFmls)
+		var subChan = make([](chan string), n)
+		var prevValues = make([]string, len(subFmls))
+		// start parallel computations on subformulas
+		for i, subFml := range subFmls {
+			subChan[i] = make(chan string) // create Channel, since currently nil
+			go subFn(subChan[i], subFml)
+		}
+		// successively read values
+		for i := 0; i < n; i++ {
+			prevValues[i] = <-subChan[i]
+		}
+		// apply schema to get value for formula
+		return scheme(fml, prevValues)
+	}
+	return fn
+}
+
+/* ---------------------------------------------------------------- *
+ * Generate *[]string-value Fn from scheme
+ * ---------------------------------------------------------------- */
+
+func CreateFromSchemeStringsValued(scheme func(fml Formula, prevValues [][]string) []string) func(fml Formula) []string {
+	var fn func(fml Formula) []string
+	var subFn = func(ch chan []string, subFml Formula) { ch <- fn(subFml) }
+	fn = func(fml Formula) []string {
+		var subFmls = fml.GetSubFormulae()
+		var n = len(subFmls)
+		var subChan = make([](chan []string), n)
+		var prevValues = make([][]string, len(subFmls))
+		// start parallel computations on subformulas
+		for i, subFml := range subFmls {
+			subChan[i] = make(chan []string) // create Channel, since currently nil
+			go subFn(subChan[i], subFml)
+		}
+		// successively read values
+		for i := 0; i < n; i++ {
+			prevValues[i] = <-subChan[i]
+		}
+		// apply schema to get value for formula
+		return scheme(fml, prevValues)
+	}
+	return fn
+}
+
+/* ---------------------------------------------------------------- *
+ * Generate Formula-value Fn from scheme
+ * ---------------------------------------------------------------- */
+
+func CreateFromSchemeFmlValued(scheme func(fml Formula, prevValues []Formula) Formula) func(fml Formula) Formula {
+	var fn func(fml Formula) Formula
+	var subFn = func(ch chan Formula, subFml Formula) { ch <- fn(subFml) }
+	fn = func(fml Formula) Formula {
+		var subFmls = fml.GetSubFormulae()
+		var n = len(subFmls)
+		var subChan = make([](chan Formula), n)
+		var prevValues = make([]Formula, len(subFmls))
+		// start parallel computations on subformulas
+		for i, subFml := range subFmls {
+			subChan[i] = make(chan Formula) // create Channel, since currently nil
+			go subFn(subChan[i], subFml)
+		}
+		// successively read values
+		for i := 0; i < n; i++ {
+			prevValues[i] = <-subChan[i]
+		}
+		// apply schema to get value for formula
+		return scheme(fml, prevValues)
+	}
+	return fn
+}
+
+/* ---------------------------------------------------------------- *
+ * Generate *[]Formula-value Fn from scheme
+ * ---------------------------------------------------------------- */
+
+func CreateFromSchemeFmlsValued(scheme func(fml Formula, prevValues [](*[]Formula)) *[]Formula) func(fml Formula) *[]Formula {
+	var fn func(fml Formula) *[]Formula
+	var subFn = func(ch chan *[]Formula, subFml Formula) { ch <- fn(subFml) }
+	fn = func(fml Formula) *[]Formula {
+		var subFmls = fml.GetSubFormulae()
+		var n = len(subFmls)
+		var subChan = make([](chan *[]Formula), n)
+		var prevValues = make([](*[]Formula), len(subFmls))
+		// start parallel computations on subformulas
+		for i, subFml := range subFmls {
+			subChan[i] = make(chan *[]Formula) // create Channel, since currently nil
+			go subFn(subChan[i], subFml)
+		}
+		// successively read values
+		for i := 0; i < n; i++ {
+			prevValues[i] = <-subChan[i]
+		}
+		// apply schema to get value for formula
+		return scheme(fml, prevValues)
+	}
+	return fn
+}
+
+/* ---------------------------------------------------------------- *
+ * Generate {pos: Formula, ne: Formula}-value Fn from scheme
+ * ---------------------------------------------------------------- */
+
+func CreateFromSchemeFmlPairValued(scheme func(fml Formula, prevValues []FormulaPair) FormulaPair) func(fml Formula) FormulaPair {
+	var fn func(fml Formula) FormulaPair
+	var subFn = func(ch chan FormulaPair, subFml Formula) { ch <- fn(subFml) }
+	fn = func(fml Formula) FormulaPair {
+		var subFmls = fml.GetSubFormulae()
+		var n = len(subFmls)
+		var subChan = make([](chan FormulaPair), n)
+		var prevValues = make([]FormulaPair, len(subFmls))
+		// start parallel computations on subformulas
+		for i, subFml := range subFmls {
+			subChan[i] = make(chan FormulaPair) // create Channel, since currently nil
+			go subFn(subChan[i], subFml)
+		}
+		// successively read values
+		for i := 0; i < n; i++ {
+			prevValues[i] = <-subChan[i]
+		}
+		// apply schema to get value for formula
+		return scheme(fml, prevValues)
+	}
+	return fn
+}
--- a/codego/aussagenlogik/formulae/formulae_normalforms.go
+++ b/codego/aussagenlogik/formulae/formulae_normalforms.go
@@ -0,0 +1,151 @@
+package formulae
+
+/* ---------------------------------------------------------------- *
+ * METHODS: get KNF/DNF
+ * ---------------------------------------------------------------- */
+
+func (fml Formula) GetKNFparts() FormulaKNF {
+	var subFmls []Formula
+	if fml.IsDisjunctOfLiterals() {
+		subFmls = []Formula{fml}
+	} else if fml.IsKNF() {
+		subFmls = fml.GetSubFormulae()
+	} else {
+		panic("Formula not in KNF!")
+	}
+	var terms = make([]FormulaDisjunct, len(subFmls))
+	for i, subFml := range subFmls {
+		if subFml.IsLiteral() {
+			terms[i] = []Formula{subFml}
+		} else {
+			terms[i] = subFml.GetSubFormulae()
+		}
+	}
+	return terms
+}
+
+func (fml Formula) GetDNFparts() FormulaDNF {
+	var subFmls []Formula
+	if fml.IsDisjunctOfLiterals() {
+		subFmls = []Formula{fml}
+	} else if fml.IsKNF() {
+		subFmls = fml.GetSubFormulae()
+	} else {
+		panic("Formula not in DNF!")
+	}
+	var terms = make([]FormulaConjunct, len(subFmls))
+	for i, subFml := range subFmls {
+		if subFml.IsLiteral() {
+			terms[i] = []Formula{subFml}
+		} else {
+			terms[i] = subFml.GetSubFormulae()
+		}
+	}
+	return terms
+}
+
+func (fml Formula) GetHornParts() FormulaHorn {
+	var subFmls []Formula
+	if fml.IsHornClause() {
+		subFmls = []Formula{fml}
+	} else if fml.IsHornFml() {
+		subFmls = fml.GetSubFormulae()
+	} else {
+		panic("Formula not a Horn-Formula!")
+	}
+	var parts = make([]FormulaHornClause, len(subFmls))
+	for i, subFml := range subFmls {
+		Pos := []Formula{}
+		Neg := []Formula{}
+		var subSubFml []Formula
+		if subFml.IsLiteral() {
+			subSubFml = []Formula{subFml}
+		} else {
+			subSubFml = subFml.GetSubFormulae()
+		}
+		for _, L := range subSubFml {
+			if L.IsPositiveLiteral() {
+				Pos = append(Pos, L)
+			} else {
+				Neg = append(Neg, L.GetChild())
+			}
+		}
+		parts[i] = FormulaHornClause{Pos, Neg}
+	}
+	return parts
+}
+
+/* ---------------------------------------------------------------- *
+ * METHODS: check if KNF/DNF
+ * ---------------------------------------------------------------- */
+
+func onlyLiterals(fmls []Formula) bool {
+	for _, fml := range fmls {
+		if !fml.IsLiteral() {
+			return false
+		}
+	}
+	return true
+}
+
+func numPositiveLiterals(fmls []Formula) int {
+	var n = 0
+	for _, fml := range fmls {
+		if fml.IsPositiveLiteral() {
+			n++
+		}
+	}
+	return n
+}
+
+func (fml Formula) IsConjunctOfLiterals() bool {
+	return fml.IsLiteral() || (fml.IsConjunction() && onlyLiterals(fml.GetSubFormulae()))
+}
+
+func (fml Formula) IsDisjunctOfLiterals() bool {
+	return fml.IsLiteral() || (fml.IsDisjunction() && onlyLiterals(fml.GetSubFormulae()))
+}
+
+func (fml Formula) IsHornClause() bool {
+	var literals = fml.GetSubFormulae()
+	return fml.IsLiteral() || (fml.IsDisjunction() && onlyLiterals(literals) && (numPositiveLiterals(literals) <= 1))
+}
+
+func (fml Formula) IsKNF() bool {
+	if fml.IsConjunction() {
+		for _, subFml := range fml.GetSubFormulae() {
+			if !subFml.IsDisjunctOfLiterals() {
+				return false
+			}
+		}
+		return true
+	} else {
+		return fml.IsDisjunctOfLiterals()
+	}
+}
+
+func (fml Formula) IsDNF() bool {
+	if fml.IsDisjunction() {
+		for _, subFml := range fml.GetSubFormulae() {
+			if !subFml.IsConjunctOfLiterals() {
+				return false
+			}
+		}
+		return true
+	} else {
+		return fml.IsConjunctOfLiterals()
+	}
+}
+
+func (fml Formula) IsHornFml() bool {
+	if fml.IsConjunction() {
+		for _, subFml := range fml.GetSubFormulae() {
+			if !subFml.IsHornClause() {
+				return false
+			}
+		}
+		return true
+	} else {
+		return fml.IsHornClause()
+	}
+}
--- a/codego/aussagenlogik/formulae/formulae_test.go
+++ b/codego/aussagenlogik/formulae/formulae_test.go
@@ -0,0 +1,158 @@
+package formulae_test
+
+/* ---------------------------------------------------------------- *
+ * UNIT TESTING
+ * ---------------------------------------------------------------- */
+
+import (
+	"logik/aussagenlogik/formulae"
+	"logik/aussagenlogik/schema"
+	"testing"
+
+	"github.com/stretchr/testify/assert"
+)
+
+/* ---------------------------------------------------------------- *
+ * TESTCASE KNF
+ * ---------------------------------------------------------------- */
+
+func TestRecogniseKNF(test *testing.T) {
+	var assert = assert.New(test)
+	var fml formulae.Formula
+
+	fml = schema.ParseExpr("A7")
+	assert.True(fml.IsKNF())
+	fml = schema.ParseExpr("! A7")
+	assert.True(fml.IsKNF())
+	fml = schema.ParseExpr("!! A7")
+	assert.False(fml.IsKNF())
+
+	fml = schema.ParseExpr("(A0 || ! A1 || A7)")
+	assert.True(fml.IsKNF())
+	fml = schema.ParseExpr("(A0 && ! A1 && A7)")
+	assert.True(fml.IsKNF())
+	fml = schema.ParseExpr("(A0 && !! A1 && A7)")
+	assert.False(fml.IsKNF())
+
+	fml = schema.ParseExpr("(A0 || ! A1 || A7) && (A4 || ! A5) && A1")
+	assert.True(fml.IsKNF())
+	fml = schema.ParseExpr("(A0 && ! A1 && A7) || (A4 && ! A5) || A1")
+	assert.False(fml.IsKNF())
+	fml = schema.ParseExpr("((A0 || ! A1 || A7) && (A4 || ! A5)) || A8")
+	assert.False(fml.IsKNF())
+}
+
+func TestRecogniseDNF(test *testing.T) {
+	var assert = assert.New(test)
+	var fml formulae.Formula
+
+	fml = schema.ParseExpr("A7")
+	assert.True(fml.IsDNF())
+	fml = schema.ParseExpr("! A7")
+	assert.True(fml.IsDNF())
+	fml = schema.ParseExpr("!! A7")
+	assert.False(fml.IsDNF())
+
+	fml = schema.ParseExpr("(A0 && ! A1 && A7)")
+	assert.True(fml.IsDNF())
+	fml = schema.ParseExpr("(A0 || ! A1 || A7)")
+	assert.True(fml.IsDNF())
+	fml = schema.ParseExpr("(A0 || !! A1 || A7)")
+	assert.False(fml.IsDNF())
+
+	fml = schema.ParseExpr("(A0 && ! A1 && A7) || (A4 && ! A5) || A1")
+	assert.True(fml.IsDNF())
+	fml = schema.ParseExpr("(A0 || ! A1 || A7) && (A4 || ! A5) && A1")
+	assert.False(fml.IsDNF())
+	fml = schema.ParseExpr("((A0 && ! A1 && A7) || (A4 && ! A5)) && A8")
+	assert.False(fml.IsDNF())
+}
+
+/* ---------------------------------------------------------------- *
+ * TESTCASE Horn
+ * ---------------------------------------------------------------- */
+
+func TestRecogniseHorn(test *testing.T) {
+	var assert = assert.New(test)
+	var fml formulae.Formula
+
+	fml = schema.ParseExpr("A7")
+	assert.True(fml.IsHornFml())
+	fml = schema.ParseExpr("! A7")
+	assert.True(fml.IsHornFml())
+	fml = schema.ParseExpr("!! A7")
+	assert.False(fml.IsHornFml())
+
+	fml = schema.ParseExpr("(! A0 || ! A1 || A7)")
+	assert.True(fml.IsHornFml())
+	fml = schema.ParseExpr("(A0 && ! A1 && A7)")
+	assert.True(fml.IsHornFml())
+	fml = schema.ParseExpr("(A0 && !! A1 && A7)")
+	assert.False(fml.IsHornFml())
+
+	fml = schema.ParseExpr("(A0 && ! A1 && ! A7) || (A4 && ! A5) || (! A1 && ! A8)")
+	assert.False(fml.IsHornFml())
+	fml = schema.ParseExpr("(A0 && ! A1 && ! A7) || (A4 && ! A5) || (! A1 && ! A8)")
+	assert.False(fml.IsHornFml())
+	fml = schema.ParseExpr("(A0 || ! A1 || ! A7) && (A4 || ! A5) && (! A1 || ! A8)")
+	assert.True(fml.IsHornFml())
+	fml = schema.ParseExpr("((A0 || ! A1 || A7) && (A4 || ! A5)) || A8")
+	assert.False(fml.IsHornFml())
+}
+
+func TestTransformHornToFormula(test *testing.T) {
+	var assert = assert.New(test)
+	var fml formulae.Formula
+	var horn formulae.FormulaHorn
+	var hornClauses []formulae.FormulaHornClause
+
+	fml = schema.ParseExpr("A8")
+	assert.True(fml.IsHornFml())
+	horn = fml.GetHornParts()
+	hornClauses = horn
+	assert.Equal(1, len(hornClauses))
+	assert.ElementsMatch([]string{"A8"}, hornClauses[0].Pos.GetAtoms())
+	assert.ElementsMatch([]string{}, hornClauses[0].Neg.GetAtoms())
+	assert.Equal("(1 -> A8)", horn.ToFormula().GetExpr())
+
+	fml = schema.ParseExpr("!A8")
+	assert.True(fml.IsHornFml())
+	horn = fml.GetHornParts()
+	hornClauses = horn
+	assert.Equal(1, len(hornClauses))
+	assert.ElementsMatch([]string{}, hornClauses[0].Pos.GetAtoms())
+	assert.ElementsMatch([]string{"A8"}, hornClauses[0].Neg.GetAtoms())
+	assert.Equal("(A8 -> 0)", horn.ToFormula().GetExpr())
+
+	fml = schema.ParseExpr("!A3 || A2 || !A7 || !A9")
+	assert.True(fml.IsHornFml())
+	horn = fml.GetHornParts()
+	hornClauses = horn
+	assert.Equal(1, len(hornClauses))
+	assert.ElementsMatch([]string{"A2"}, hornClauses[0].Pos.GetAtoms())
+	assert.ElementsMatch([]string{"A3", "A7", "A9"}, hornClauses[0].Neg.GetAtoms())
+	assert.Equal("((A3 && A7 && A9) -> A2)", horn.ToFormula().GetExpr())
+
+	fml = schema.ParseExpr("!A3 || !A2 || !A7 || !A9")
+	assert.True(fml.IsHornFml())
+	horn = fml.GetHornParts()
+	hornClauses = horn
+	assert.Equal(1, len(hornClauses))
+	assert.ElementsMatch([]string{}, hornClauses[0].Pos.GetAtoms())
+	assert.ElementsMatch([]string{"A2", "A3", "A7", "A9"}, hornClauses[0].Neg.GetAtoms())
+	assert.Equal("((A3 && A2 && A7 && A9) -> 0)", horn.ToFormula().GetExpr())
+
+	fml = schema.ParseExpr("!A3 && A2 && !A7 && A9 && A7")
+	assert.True(fml.IsHornFml())
+	horn = fml.GetHornParts()
+	hornClauses = horn
+	assert.Equal(5, len(hornClauses))
+	assert.Equal("((A3 -> 0) && (1 -> A2) && (A7 -> 0) && (1 -> A9) && (1 -> A7))", horn.ToFormula().GetExpr())
+
+	fml = schema.ParseExpr("(A0 || ! A1 || ! A7) && (A4 || ! A5) && (! A1 || ! A8)")
+	assert.True(fml.IsHornFml())
+	horn = fml.GetHornParts()
+	hornClauses = horn
+	assert.Equal(3, len(hornClauses))
+	assert.Equal("(((A1 && A7) -> A0) && (A5 -> A4) && ((A1 && A8) -> 0))", horn.ToFormula().GetExpr())
+}
--- a/codego/aussagenlogik/recursion/recursion_atoms.go
+++ b/codego/aussagenlogik/recursion/recursion_atoms.go
@@ -0,0 +1,35 @@
+package recursion
+
+import (
+	"logik/aussagenlogik/formulae"
+)
+
+/* ---------------------------------------------------------------- *
+ * METHOD: Atoms
+ * ---------------------------------------------------------------- */
+
+func Atoms(fml formulae.Formula) []string {
+	// Definiere Schema:
+	var schema = func(fml formulae.Formula, prevValues [][]string) []string {
+		// Herausforderung: schreibe diese Funktion!
+		return []string{}
+	}
+	// Erzeuge Funktion aus Schema und berechne Wert:
+	fn := formulae.CreateFromSchemeStringsValued(schema)
+	return fn(fml)
+}
+
+/* ---------------------------------------------------------------- *
+ * METHOD: Subformulae
+ * ---------------------------------------------------------------- */
+
+func Subformulae(fml formulae.Formula) []string {
+	// Definiere Schema:
+	var schema = func(fml formulae.Formula, prevValues [][]string) []string {
+		// Herausforderung: schreibe diese Funktion!
+		return []string{}
+	}
+	// Erzeuge Funktion aus Schema und berechne Wert:
+	fn := formulae.CreateFromSchemeStringsValued(schema)
+	return fn(fml)
+}
--- a/codego/aussagenlogik/recursion/recursion_count.go
+++ b/codego/aussagenlogik/recursion/recursion_count.go
@@ -0,0 +1,49 @@
+package recursion
+
+import (
+	"logik/aussagenlogik/formulae"
+)
+
+/* ---------------------------------------------------------------- *
+ * METHOD: Formula Depth
+ * ---------------------------------------------------------------- */
+
+func FmlDepth(fml formulae.Formula) int {
+	// Definiere Schema:
+	var schema = func(fml formulae.Formula, prevValues []int) int {
+		// Herausforderung: schreibe diese Funktion!
+		return 0
+	}
+	// Erzeuge Funktion aus Schema und berechne Wert:
+	fn := formulae.CreateFromSchemeIntValued(schema)
+	return fn(fml)
+}
+
+/* ---------------------------------------------------------------- *
+ * METHOD: Formula Length
+ * ---------------------------------------------------------------- */
+
+func FmlLength(fml formulae.Formula) int {
+	// Definiere Schema:
+	var schema = func(fml formulae.Formula, prevValues []int) int {
+		// Herausforderung: schreibe diese Funktion!
+		return 0
+	}
+	// Erzeuge Funktion aus Schema und berechne Wert:
+	fn := formulae.CreateFromSchemeIntValued(schema)
+	return fn(fml)
+}
+
+/* ---------------------------------------------------------------- *
+ * METHOD: Number of Parentheses
+ * ---------------------------------------------------------------- */
+func NrParentheses(fml formulae.Formula) int {
+	// Definiere Schema:
+	var schema = func(fml formulae.Formula, prevValues []int) int {
+		// Herausforderung: schreibe diese Funktion!
+		return 0
+	}
+	// Erzeuge Funktion aus Schema und berechne Wert:
+	fn := formulae.CreateFromSchemeIntValued(schema)
+	return fn(fml)
+}
--- a/codego/aussagenlogik/recursion/recursion_eval.go
+++ b/codego/aussagenlogik/recursion/recursion_eval.go
@@ -0,0 +1,44 @@
+package recursion
+
+import (
+	"logik/aussagenlogik/formulae"
+	"logik/core/utils"
+)
+
+/* ---------------------------------------------------------------- *
+ * METHOD: Evaluation of fomulae in models
+ * ---------------------------------------------------------------- */
+
+func Eval(fml formulae.Formula, I []string) int {
+	// Definiere (parameterisiertes) Schema:
+	var schema = func(_I []string) func(formulae.Formula, []int) int {
+		return func(fml formulae.Formula, prevValues []int) int {
+			if fml.IsAtom() || fml.IsGeneric() {
+				return utils.BoolToInt(utils.StrListContains(_I, fml.GetName()))
+			} else if fml.IsTautologySymbol() {
+				return 1
+			} else if fml.IsContradictionSymbol() {
+				return 0
+			} else if fml.IsNegation() {
+				return 1 - prevValues[0]
+			} else if fml.IsConjunction2() {
+				return utils.Min2(prevValues[0], prevValues[1])
+			} else if fml.IsConjunction() {
+				return utils.MinList(prevValues)
+			} else if fml.IsDisjunction2() {
+				return utils.Max2(prevValues[0], prevValues[1])
+			} else if fml.IsDisjunction() {
+				return utils.MaxList(prevValues)
+			} else if fml.IsImplication() {
+				return utils.BoolToInt(prevValues[0] <= prevValues[1])
+			} else if fml.IsDoubleImplication() {
+				return utils.BoolToInt(prevValues[0] == prevValues[1])
+			} else {
+				panic("Could not evaluate expression!")
+			}
+		}
+	}
+	// Erzeuge Funktion aus Schema und berechne Wert:
+	fn := formulae.CreateFromSchemeIntValued(schema(I))
+	return fn(fml)
+}
--- a/codego/aussagenlogik/recursion/recursion_nnf.go
+++ b/codego/aussagenlogik/recursion/recursion_nnf.go
@@ -0,0 +1,88 @@
+package recursion
+
+import (
+	"logik/aussagenlogik/formulae"
+)
+
+/* ---------------------------------------------------------------- *
+ * METHOD: compute NNF
+ * ---------------------------------------------------------------- */
+
+// NOTE: diese bedarf einer Art Doppeltrekursion
+func NNF(fml formulae.Formula) formulae.Formula {
+	// Definiere Schema:
+	var schema = func(fml formulae.Formula, prevValues []formulae.FormulaPair) formulae.FormulaPair {
+		// separate out positive and negative parts:
+		var pairs = formulae.NewFormulaPairs(prevValues)
+		var prevPos = pairs.Pos()
+		var prevNeg = pairs.Neg()
+		// compute value from previous positive/negative parts:
+		if fml.IsPositiveLiteral() {
+			return formulae.FormulaPair{
+				Pos: fml.Deepcopy(),
+				Neg: formulae.Negation(fml),
+			}
+		} else if fml.IsNegativeLiteral() {
+			return formulae.FormulaPair{
+				Pos: fml.Deepcopy(),
+				Neg: prevPos[0],
+			}
+		} else if fml.IsTautologySymbol() {
+			return formulae.FormulaPair{
+				Pos: formulae.Tautology,
+				Neg: formulae.Contradiction,
+			}
+		} else if fml.IsContradictionSymbol() {
+			return formulae.FormulaPair{
+				Pos: formulae.Contradiction,
+				Neg: formulae.Tautology,
+			}
+		} else if fml.IsNegation() {
+			return formulae.FormulaPair{
+				Pos: prevNeg[0],
+				Neg: prevPos[0],
+			}
+		} else if fml.IsConjunction2() {
+			return formulae.FormulaPair{
+				Pos: formulae.Conjunction2(prevPos[0], prevPos[1]),
+				Neg: formulae.Disjunction2(prevNeg[0], prevNeg[1]),
+			}
+		} else if fml.IsConjunction() {
+			return formulae.FormulaPair{
+				Pos: formulae.Conjunction(prevPos),
+				Neg: formulae.Disjunction(prevNeg),
+			}
+		} else if fml.IsDisjunction2() {
+			return formulae.FormulaPair{
+				Pos: formulae.Disjunction2(prevPos[0], prevPos[1]),
+				Neg: formulae.Conjunction2(prevNeg[0], prevNeg[1]),
+			}
+		} else if fml.IsDisjunction() {
+			return formulae.FormulaPair{
+				Pos: formulae.Disjunction(prevPos),
+				Neg: formulae.Conjunction(prevNeg),
+			}
+		} else if fml.IsImplication() {
+			return formulae.FormulaPair{
+				Pos: formulae.Disjunction2(prevNeg[0], prevPos[1]),
+				Neg: formulae.Conjunction2(prevPos[0], prevNeg[1]),
+			}
+		} else if fml.IsDoubleImplication() {
+			return formulae.FormulaPair{
+				Pos: formulae.Conjunction2(
+					formulae.Disjunction2(prevNeg[0], prevPos[1]),
+					formulae.Disjunction2(prevNeg[1], prevPos[0]),
+				),
+				Neg: formulae.Disjunction2(
+					formulae.Conjunction2(prevPos[0], prevNeg[1]),
+					formulae.Conjunction2(prevPos[1], prevNeg[0]),
+				),
+			}
+		} else {
+			panic("Could not evaluate expression!")
+		}
+	}
+	// Erzeuge Funktion aus Schema und berechne Wert:
+	fn := formulae.CreateFromSchemeFmlPairValued(schema)
+	return fn(fml).Pos
+}
--- a/codego/aussagenlogik/recursion/recursion_test.go
+++ b/codego/aussagenlogik/recursion/recursion_test.go
@@ -0,0 +1,455 @@
+package recursion_test
+
+/* ---------------------------------------------------------------- *
+ * UNIT TESTING
+ * ---------------------------------------------------------------- */
+
+import (
+	"logik/aussagenlogik/formulae"
+	"logik/aussagenlogik/recursion"
+	"logik/aussagenlogik/schema"
+	"logik/core/utils"
+	"testing"
+
+	"github.com/stretchr/testify/assert"
+)
+
+/* ---------------------------------------------------------------- *
+ * TESTCASE eval(·, ·)
+ * ---------------------------------------------------------------- */
+
+func TestEvalLiteral(test *testing.T) {
+	var assert = assert.New(test)
+	var val int
+	var fml formulae.Formula
+	var I []string
+
+	fml = schema.ParseExpr("A0")
+	I = []string{"A0"}
+	val = recursion.Eval(fml, I)
+	assert.Equal(1, val)
+
+	fml = schema.ParseExpr("A0")
+	I = []string{}
+	val = recursion.Eval(fml, I)
+	assert.Equal(0, val)
+
+	fml = schema.ParseExpr("! A0")
+	I = []string{"A0"}
+	val = recursion.Eval(fml, I)
+	assert.Equal(0, val)
+
+	fml = schema.ParseExpr("! A0")
+	I = []string{}
+	val = recursion.Eval(fml, I)
+	assert.Equal(1, val)
+}
+
+func TestEvalNegation(test *testing.T) {
+	var assert = assert.New(test)
+	var val int
+	var fml formulae.Formula
+	var I []string
+
+	fml = schema.ParseExpr("A4 || ! A4")
+	I = []string{}
+	val = recursion.Eval(fml, I)
+	assert.Equal(1, val)
+
+	fml = schema.ParseExpr("A4 && ! A4")
+	I = []string{}
+	val = recursion.Eval(fml, I)
+	assert.Equal(0, val)
+}
+
+func TestEvalConjunction(test *testing.T) {
+	var assert = assert.New(test)
+	var val int
+	var fml formulae.Formula
+	var I []string
+
+	fml = schema.ParseExpr("A0 && A1")
+	I = []string{"A0"}
+	val = recursion.Eval(fml, I)
+	assert.Equal(0, val)
+
+	fml = schema.ParseExpr("A0 && A1")
+	I = []string{"A0", "A1"}
+	val = recursion.Eval(fml, I)
+	assert.Equal(1, val)
+}
+
+func TestEvalDisjunction(test *testing.T) {
+	var assert = assert.New(test)
+	var val int
+	var fml formulae.Formula
+	var I []string
+
+	fml = schema.ParseExpr("A0 || A1")
+	I = []string{"A0"}
+	val = recursion.Eval(fml, I)
+	assert.Equal(1, val)
+
+	fml = schema.ParseExpr("A0 || A1")
+	I = []string{"A7"}
+	val = recursion.Eval(fml, I)
+	assert.Equal(0, val)
+}
+
+func TestEvalImplication(test *testing.T) {
+	var assert = assert.New(test)
+	var val int
+	var fml formulae.Formula
+	var I []string
+
+	fml = schema.ParseExpr("A0 -> A1")
+	I = []string{"A0"}
+	val = recursion.Eval(fml, I)
+	assert.Equal(0, val)
+
+	fml = schema.ParseExpr("A0 -> A1")
+	I = []string{"A0", "A1"}
+	val = recursion.Eval(fml, I)
+	assert.Equal(1, val)
+
+	fml = schema.ParseExpr("A0 -> A1")
+	I = []string{"A7"}
+	val = recursion.Eval(fml, I)
+	assert.Equal(1, val)
+}
+
+func TestEvalIff(test *testing.T) {
+	var assert = assert.New(test)
+	var val int
+	var fml formulae.Formula
+	var I []string
+
+	fml = schema.ParseExpr("A0 <-> A1")
+	I = []string{"A0"}
+	val = recursion.Eval(fml, I)
+	assert.Equal(0, val)
+
+	fml = schema.ParseExpr("A0 <-> A1")
+	I = []string{"A0", "A1"}
+	val = recursion.Eval(fml, I)
+	assert.Equal(1, val)
+
+	fml = schema.ParseExpr("A0 <-> A1")
+	I = []string{"A7"}
+	val = recursion.Eval(fml, I)
+	assert.Equal(1, val)
+}
+
+func TestEvalComplex(test *testing.T) {
+	var assert = assert.New(test)
+	var val int
+	var fml formulae.Formula
+	var I []string
+	fml = schema.ParseExpr("( ! A0 || (( A0 && A3 ) || A2 ))")
+	I = []string{"A0", "A2"}
+	val = recursion.Eval(fml, I)
+	assert.Equal(1, val)
+
+	I = []string{"A0", "A3"}
+	val = recursion.Eval(fml, I)
+	assert.Equal(1, val)
+
+	I = []string{"A0"}
+	val = recursion.Eval(fml, I)
+	assert.Equal(0, val)
+
+	I = []string{"A4", "A8"}
+	val = recursion.Eval(fml, I)
+	assert.Equal(1, val)
+
+	fml = schema.ParseExpr("( ! A0 || (( A0 && A3 ) || ! A2 ))")
+	I = []string{"A0", "A2"}
+	val = recursion.Eval(fml, I)
+	assert.Equal(0, val)
+
+	I = []string{"A0", "A3"}
+	val = recursion.Eval(fml, I)
+	assert.Equal(1, val)
+}
+
+/* ---------------------------------------------------------------- *
+ * TESTCASE Atoms(·)
+ * ---------------------------------------------------------------- */
+
+func TestAtomsNoduplicates(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	var assert = assert.New(test)
+	var fml formulae.Formula
+	var val []string
+	fml = schema.ParseExpr("( A4 && ( A4 || A4 ))")
+	val = recursion.Atoms(fml)
+	var n int = len(utils.FilterStrings(&val, func(x string) bool { return x == "A4" }))
+	assert.Equal(1, n, "Atome dürfen nicht mehrfach vorkommen!")
+}
+
+func TestAtomsNoNonAtoms(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	var assert = assert.New(test)
+	var fml formulae.Formula
+	var val []string
+	fml = schema.ParseExpr("( {F} || A3 )")
+	val = recursion.Atoms(fml)
+	utils.SortStrings(&val)
+	assert.NotContains(val, "F", "Nichtatomare Formeln dürfen nicht vorkommen!")
+}
+
+func TestAtomsCalc1(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	var assert = assert.New(test)
+	var fml formulae.Formula
+	var val []string
+	fml = schema.ParseExpr("A0")
+	val = recursion.Atoms(fml)
+	assert.ElementsMatch([]string{"A0"}, val)
+}
+
+func TestAtomsCalc2(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	var assert = assert.New(test)
+	var fml formulae.Formula
+	var val []string
+	fml = schema.ParseExpr("((( ! A8 && A3 ) || A4 ) && A0 )")
+	val = recursion.Atoms(fml)
+	assert.ElementsMatch([]string{"A0", "A3", "A4", "A8"}, val)
+}
+
+/* ---------------------------------------------------------------- *
+ * TESTCASE depth(·, ·)
+ * ---------------------------------------------------------------- */
+
+func TestDepthCalc1(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	var assert = assert.New(test)
+	var val int
+	var fml formulae.Formula
+	fml = schema.ParseExpr("A0")
+	val = recursion.FmlDepth(fml)
+	assert.Equal(0, val)
+}
+
+func TestDepthCalc2(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	var assert = assert.New(test)
+	var val int
+	var fml formulae.Formula
+	fml = schema.ParseExpr("!! A8")
+	val = recursion.FmlDepth(fml)
+	assert.Equal(2, val)
+}
+
+func TestDepthCalc3(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	var assert = assert.New(test)
+	var val int
+	var fml formulae.Formula
+	fml = schema.ParseExpr("( ! A0 && A3 )")
+	val = recursion.FmlDepth(fml)
+	assert.Equal(2, val)
+}
+
+func TestDepthCalc4(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	var assert = assert.New(test)
+	var val int
+	var fml formulae.Formula
+	fml = schema.ParseExpr("((( ! A0 && A3 ) || A4 ) && A8 )")
+	val = recursion.FmlDepth(fml)
+	assert.Equal(4, val)
+}
+
+func TestDepthCalc5(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	var assert = assert.New(test)
+	var val int
+	var fml formulae.Formula
+	fml = schema.ParseExpr("! ((( ! A0 && A3 ) || A4 ) && A8 )")
+	val = recursion.FmlDepth(fml)
+	assert.Equal(5, val)
+}
+
+/* ---------------------------------------------------------------- *
+ * TESTCASE length(·)
+ * ---------------------------------------------------------------- */
+
+func TestLengthCalc1(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	var assert = assert.New(test)
+	var val int
+	var fml formulae.Formula
+	fml = schema.ParseExpr("A0")
+	val = recursion.FmlLength(fml)
+	assert.Equal(1, val)
+}
+
+func TestLengthCalc2(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	var assert = assert.New(test)
+	var val int
+	var fml formulae.Formula
+	fml = schema.ParseExpr("!! A8")
+	val = recursion.FmlLength(fml)
+	assert.Equal(3, val)
+}
+
+func TestLengthCalc3(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	var assert = assert.New(test)
+	var val int
+	var fml formulae.Formula
+	fml = schema.ParseExpr("( ! A0 && A3 )")
+	val = recursion.FmlLength(fml)
+	assert.Equal(4, val)
+}
+
+func TestLengthCalc4(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	var assert = assert.New(test)
+	var val int
+	var fml formulae.Formula
+	fml = schema.ParseExpr("((( ! A0 && A3 ) || A4 ) && A8 )")
+	val = recursion.FmlLength(fml)
+	assert.Equal(8, val)
+}
+
+func TestLengthCalc5(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	var assert = assert.New(test)
+	var val int
+	var fml formulae.Formula
+	fml = schema.ParseExpr("! ((( ! A0 && A3 ) || A4 ) && A8 )")
+	val = recursion.FmlLength(fml)
+	assert.Equal(9, val)
+}
+
+/* ---------------------------------------------------------------- *
+ * TESTCASE #Parentheses(·)
+ * ---------------------------------------------------------------- */
+
+func TestParenthesesCalc1(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	var assert = assert.New(test)
+	var val int
+	var fml formulae.Formula
+	fml = schema.ParseExpr("A0")
+	val = recursion.NrParentheses(fml)
+	assert.Equal(0, val)
+}
+
+func TestParenthesesCalc2(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	var assert = assert.New(test)
+	var val int
+	var fml formulae.Formula
+	fml = schema.ParseExpr("!! A8")
+	val = recursion.NrParentheses(fml)
+	assert.Equal(0, val)
+}
+
+func TestParenthesesCalc3(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	var assert = assert.New(test)
+	var val int
+	var fml formulae.Formula
+	fml = schema.ParseExpr("( ! A0 && A3 )")
+	val = recursion.NrParentheses(fml)
+	assert.Equal(2, val)
+}
+
+func TestParenthesesCalc4(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	var assert = assert.New(test)
+	var val int
+	var fml formulae.Formula
+	fml = schema.ParseExpr("((( ! A0 && A3 ) || A4 ) && A8 )")
+	val = recursion.NrParentheses(fml)
+	assert.Equal(6, val)
+}
+
+func TestParenthesesCalc5(test *testing.T) {
+	test.Skip("Methode noch nicht implementiert")
+	var assert = assert.New(test)
+	var val int
+	var fml formulae.Formula
+	fml = schema.ParseExpr("! ((( ! A0 && A3 ) || A4 ) && A8 )")
+	val = recursion.NrParentheses(fml)
+	assert.Equal(6, val)
+}
+
+/* ---------------------------------------------------------------- *
+ * TESTCASE NNF
+ * ---------------------------------------------------------------- */
+
+func TestNNFatoms(test *testing.T) {
+	var assert = assert.New(test)
+	var fml formulae.Formula
+	var nnf_expected formulae.Formula
+
+	nnf_expected = formulae.Atom("A7")
+	fml = schema.ParseExpr("A7")
+	assert.Equal(nnf_expected.GetExpr(), recursion.NNF(fml).GetExpr())
+
+	fml = schema.ParseExpr("!! A7")
+	assert.Equal(nnf_expected.GetExpr(), recursion.NNF(fml).GetExpr())
+
+	nnf_expected = formulae.NegatedAtom("A7")
+	fml = schema.ParseExpr("! A7")
+	assert.Equal(nnf_expected.GetExpr(), recursion.NNF(fml).GetExpr())
+
+	fml = schema.ParseExpr("!!! A7")
+	assert.Equal(nnf_expected.GetExpr(), recursion.NNF(fml).GetExpr())
+}
+
+func TestNNFconj(test *testing.T) {
+	var assert = assert.New(test)
+	var fml formulae.Formula
+	var nnf_expected formulae.Formula
+
+	nnf_expected = formulae.Disjunction2(formulae.NegatedAtom("A0"), formulae.NegatedAtom("A1"))
+	fml = schema.ParseExpr("! (A0 && A1)")
+	assert.Equal(nnf_expected.GetExpr(), recursion.NNF(fml).GetExpr())
+
+	nnf_expected = formulae.Disjunction2(formulae.Atom("A0"), formulae.Atom("A1"))
+	fml = schema.ParseExpr("! (! A0 && ! A1)")
+	assert.Equal(nnf_expected.GetExpr(), recursion.NNF(fml).GetExpr())
+
+	nnf_expected = formulae.Conjunction2(formulae.Atom("A0"), formulae.NegatedAtom("A1"))
+	fml = schema.ParseExpr("(A0 && ! A1)")
+	assert.Equal(nnf_expected.GetExpr(), recursion.NNF(fml).GetExpr())
+}
+
+func TestNNFdisj(test *testing.T) {
+	var assert = assert.New(test)
+	var fml formulae.Formula
+	var nnf_expected formulae.Formula
+
+	nnf_expected = formulae.Conjunction2(formulae.NegatedAtom("A0"), formulae.NegatedAtom("A1"))
+	fml = schema.ParseExpr("! (A0 || A1)")
+	assert.Equal(nnf_expected.GetExpr(), recursion.NNF(fml).GetExpr())
+
+	nnf_expected = formulae.Conjunction2(formulae.Atom("A0"), formulae.Atom("A1"))
+	fml = schema.ParseExpr("! (! A0 || ! A1)")
+	assert.Equal(nnf_expected.GetExpr(), recursion.NNF(fml).GetExpr())
+
+	nnf_expected = formulae.Disjunction2(formulae.Atom("A0"), formulae.NegatedAtom("A1"))
+	fml = schema.ParseExpr("(A0 || ! A1)")
+	assert.Equal(nnf_expected.GetExpr(), recursion.NNF(fml).GetExpr())
+}
+
+func TestNNFcalcComplex(test *testing.T) {
+	var assert = assert.New(test)
+	var fml formulae.Formula
+	var nnf_expected formulae.Formula
+
+	fml = schema.ParseExpr("! (! (!A0 || A1) || ! ! A8)")
+	nnf_expected = schema.ParseExpr("((!A0 || A1) && ! A8)")
+	assert.Equal(nnf_expected.GetExpr(), recursion.NNF(fml).GetExpr())
+
+	fml = schema.ParseExpr("! (! (!A0 || !(A1 && ! A7)) && ! A8)")
+	nnf_expected = schema.ParseExpr("((!A0 || (! A1 || A7)) || A8)")
+	assert.Equal(nnf_expected.GetExpr(), recursion.NNF(fml).GetExpr())
+}
--- a/codego/aussagenlogik/rekursion/rekursion.go
+++ b/codego/aussagenlogik/rekursion/rekursion.go
@@ -1,82 +0,0 @@
-package rekursion
-
-import (
-	"log"
-	"logik/aussagenlogik/syntaxbaum"
-	"logik/core/utils"
-)
-
-/* ---------------------------------------------------------------- *
- * EXPORTS
- * ---------------------------------------------------------------- */
-
-func RekursivEval(tree syntaxbaum.SyntaxBaum, I []string) int {
-	var children = tree.GetChildren()
-	switch tree.Kind {
-	case "atom", "generic":
-		if utils.StrListContains(I, tree.Expr) {
-			return 1
-		}
-		return 0
-	case "taut":
-		return 1
-	case "contradiction":
-		return 0
-	case "not":
-		subtree0, _ := tree.GetChild()
-		val0 := RekursivEval(subtree0, I)
-		return 1 - val0
-	case "and2":
-		val0 := RekursivEval(children[0], I)
-		val1 := RekursivEval(children[1], I)
-		return utils.Min2(val0, val1)
-	case "and":
-		var val = 1
-		for _, subtree := range children {
-			var val_ = RekursivEval(subtree, I)
-			val = utils.Min2(val, val_)
-		}
-		return val
-	case "or2":
-		val0 := RekursivEval(children[0], I)
-		val1 := RekursivEval(children[1], I)
-		return utils.Max2(val0, val1)
-	case "or":
-		var val = 0
-		for _, subtree := range children {
-			var val_ = RekursivEval(subtree, I)
-			val = utils.Max2(val, val_)
-		}
-		return val
-	case "implies":
-		val0 := RekursivEval(children[0], I)
-		val1 := RekursivEval(children[1], I)
-		if val0 <= val1 {
-			return 1
-		}
-		return 0
-	default:
-		log.Fatal("Could not evaluate expression!")
-		return 0
-	}
-}
-
-func RekursivAtoms(tree syntaxbaum.SyntaxBaum) []string {
-	// Herausforderung: schreibe diese Funktion!
-	return []string{}
-}
-
-func RekursivDepth(tree syntaxbaum.SyntaxBaum) int {
-	// Herausforderung: schreibe diese Funktion!
-	return 0
-}
-
-func RekursivLength(tree syntaxbaum.SyntaxBaum) int {
-	// Herausforderung: schreibe diese Funktion!
-	return 0
-}
-
-func RekursivParentheses(tree syntaxbaum.SyntaxBaum) int {
-	// Herausforderung: schreibe diese Funktion!
-	return 0
-}
--- a/codego/aussagenlogik/rekursion/rekursion_test.go
+++ b/codego/aussagenlogik/rekursion/rekursion_test.go
@@ -1,287 +0,0 @@
-package rekursion_test
-
-/* ---------------------------------------------------------------- *
- * UNIT TESTING
- * ---------------------------------------------------------------- */
-
-import (
-	"logik/aussagenlogik/rekursion"
-	"logik/aussagenlogik/schema"
-	"logik/aussagenlogik/syntaxbaum"
-	"logik/core/utils"
-	"testing"
-
-	"github.com/stretchr/testify/assert"
-)
-
-/* ---------------------------------------------------------------- *
- * TESTCASE eval(·, ·)
- * ---------------------------------------------------------------- */
-
-func TestRekursivEvalLiteral(test *testing.T) {
-	var assert = assert.New(test)
-	var tree syntaxbaum.SyntaxBaum
-	var I []string
-	var val int
-	tree, _ = schema.ParseExpr("A0")
-	I = []string{"A0"}
-	val = rekursion.RekursivEval(tree, I)
-	assert.Equal(val, 1)
-	tree, _ = schema.ParseExpr("A0")
-	I = []string{}
-	val = rekursion.RekursivEval(tree, I)
-	assert.Equal(val, 0)
-	tree, _ = schema.ParseExpr("! A0")
-	I = []string{"A0"}
-	val = rekursion.RekursivEval(tree, I)
-	assert.Equal(val, 0)
-	tree, _ = schema.ParseExpr("! A0")
-	I = []string{}
-	val = rekursion.RekursivEval(tree, I)
-	assert.Equal(val, 1)
-}
-
-func TestRekursivEvalComplex1(test *testing.T) {
-	var assert = assert.New(test)
-	var tree syntaxbaum.SyntaxBaum
-	var I []string
-	var val int
-	tree, _ = schema.ParseExpr("( ! A0 || (( A0 && A3 ) || A2 ))")
-	I = []string{"A0", "A2"}
-	val = rekursion.RekursivEval(tree, I)
-	assert.Equal(val, 1)
-	I = []string{"A0", "A3"}
-	val = rekursion.RekursivEval(tree, I)
-	assert.Equal(val, 1)
-	I = []string{"A0"}
-	val = rekursion.RekursivEval(tree, I)
-	assert.Equal(val, 0)
-	I = []string{"A4", "A8"}
-	val = rekursion.RekursivEval(tree, I)
-	assert.Equal(val, 1)
-}
-
-func TestRekursivEvalComplex2(test *testing.T) {
-	var assert = assert.New(test)
-	var tree syntaxbaum.SyntaxBaum
-	var I []string
-	var val int
-	tree, _ = schema.ParseExpr("( ! A0 || (( A0 && A3 ) || ! A2 ))")
-	I = []string{"A0", "A2"}
-	val = rekursion.RekursivEval(tree, I)
-	assert.Equal(val, 0)
-	I = []string{"A0", "A3"}
-	val = rekursion.RekursivEval(tree, I)
-	assert.Equal(val, 1)
-}
-
-/* ---------------------------------------------------------------- *
- * TESTCASE Atoms(·)
- * ---------------------------------------------------------------- */
-
-func TestRekursivAtomsNoduplicates(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	var assert = assert.New(test)
-	var tree syntaxbaum.SyntaxBaum
-	var val []string
-	tree, _ = schema.ParseExpr("( A4 && ( A4 || A4 ))")
-	val = rekursion.RekursivAtoms(tree)
-	var n int = len(utils.FilterStrings(&val, func(x string) bool { return x == "A4" }))
-	assert.Equal(n, 1, "Atome dürfen nicht mehrfach vorkommen!")
-}
-
-func TestRekursivAtomsNononatoms(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	test.Skip("Syntax for generic expressions in ANTLR4 g4 needs to be implemented.")
-	var assert = assert.New(test)
-	var tree syntaxbaum.SyntaxBaum
-	var val []string
-	tree, _ = schema.ParseExpr("( {F} || A3 )")
-	val = rekursion.RekursivAtoms(tree)
-	utils.SortStrings(&val)
-	assert.NotContains(val, "F", "Nichtatomare Formeln dürfen nicht vorkommen!")
-}
-
-func TestRekursivAtomsCalc1(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	var assert = assert.New(test)
-	var tree syntaxbaum.SyntaxBaum
-	var val []string
-	tree, _ = schema.ParseExpr("A0")
-	val = rekursion.RekursivAtoms(tree)
-	utils.SortStrings(&val)
-	assert.Equal(val, []string{"A0"})
-}
-
-func TestRekursivAtomsCalc2(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	var assert = assert.New(test)
-	var tree syntaxbaum.SyntaxBaum
-	var val []string
-	tree, _ = schema.ParseExpr("((( ! A8 && A3 ) || A4 ) && A0 )")
-	val = rekursion.RekursivAtoms(tree)
-	utils.SortStrings(&val)
-	assert.Equal(val, []string{"A0", "A3", "A4", "A8"})
-}
-
-/* ---------------------------------------------------------------- *
- * TESTCASE depth(·, ·)
- * ---------------------------------------------------------------- */
-
-func TestRekursivDepthCalc1(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	var assert = assert.New(test)
-	var tree syntaxbaum.SyntaxBaum
-	var val int
-	tree, _ = schema.ParseExpr("A0")
-	val = rekursion.RekursivDepth(tree)
-	assert.Equal(val, 0)
-}
-
-func TestRekursivDepthCalc2(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	var assert = assert.New(test)
-	var tree syntaxbaum.SyntaxBaum
-	var val int
-	tree, _ = schema.ParseExpr("!! A8")
-	val = rekursion.RekursivDepth(tree)
-	assert.Equal(val, 2)
-}
-
-func TestRekursivDepthCalc3(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	var assert = assert.New(test)
-	var tree syntaxbaum.SyntaxBaum
-	var val int
-	tree, _ = schema.ParseExpr("( ! A0 && A3 )")
-	val = rekursion.RekursivDepth(tree)
-	assert.Equal(val, 2)
-}
-
-func TestRekursivDepthCalc4(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	var assert = assert.New(test)
-	var tree syntaxbaum.SyntaxBaum
-	var val int
-	tree, _ = schema.ParseExpr("((( ! A0 && A3 ) || A4 ) && A8 )")
-	val = rekursion.RekursivDepth(tree)
-	assert.Equal(val, 4)
-}
-
-func TestRekursivDepthCalc5(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	var assert = assert.New(test)
-	var tree syntaxbaum.SyntaxBaum
-	var val int
-	tree, _ = schema.ParseExpr("! ((( ! A0 && A3 ) || A4 ) && A8 )")
-	val = rekursion.RekursivDepth(tree)
-	assert.Equal(val, 5)
-}
-
-/* ---------------------------------------------------------------- *
- * TESTCASE length(·)
- * ---------------------------------------------------------------- */
-
-func TestRekursivLengthCalc1(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	var assert = assert.New(test)
-	var tree syntaxbaum.SyntaxBaum
-	var val int
-	tree, _ = schema.ParseExpr("A0")
-	val = rekursion.RekursivLength(tree)
-	assert.Equal(val, 1)
-}
-
-func TestRekursivLengthCalc2(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	var assert = assert.New(test)
-	var tree syntaxbaum.SyntaxBaum
-	var val int
-	tree, _ = schema.ParseExpr("!! A8")
-	val = rekursion.RekursivLength(tree)
-	assert.Equal(val, 3)
-}
-
-func TestRekursivLengthCalc3(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	var assert = assert.New(test)
-	var tree syntaxbaum.SyntaxBaum
-	var val int
-	tree, _ = schema.ParseExpr("( ! A0 && A3 )")
-	val = rekursion.RekursivLength(tree)
-	assert.Equal(val, 4)
-}
-
-func TestRekursivLengthCalc4(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	var assert = assert.New(test)
-	var tree syntaxbaum.SyntaxBaum
-	var val int
-	tree, _ = schema.ParseExpr("((( ! A0 && A3 ) || A4 ) && A8 )")
-	val = rekursion.RekursivLength(tree)
-	assert.Equal(val, 8)
-}
-
-func TestRekursivLengthCalc5(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	var assert = assert.New(test)
-	var tree syntaxbaum.SyntaxBaum
-	var val int
-	tree, _ = schema.ParseExpr("! ((( ! A0 && A3 ) || A4 ) && A8 )")
-	val = rekursion.RekursivLength(tree)
-	assert.Equal(val, 9)
-}
-
-/* ---------------------------------------------------------------- *
- * TESTCASE #Parentheses(·)
- * ---------------------------------------------------------------- */
-
-func TestRekursivParenthesesCalc1(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	var assert = assert.New(test)
-	var tree syntaxbaum.SyntaxBaum
-	var val int
-	tree, _ = schema.ParseExpr("A0")
-	val = rekursion.RekursivParentheses(tree)
-	assert.Equal(val, 0)
-}
-
-func TestRekursivParenthesesCalc2(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	var assert = assert.New(test)
-	var tree syntaxbaum.SyntaxBaum
-	var val int
-	tree, _ = schema.ParseExpr("!! A8")
-	val = rekursion.RekursivParentheses(tree)
-	assert.Equal(val, 0)
-}
-
-func TestRekursivParenthesesCalc3(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	var assert = assert.New(test)
-	var tree syntaxbaum.SyntaxBaum
-	var val int
-	tree, _ = schema.ParseExpr("( ! A0 && A3 )")
-	val = rekursion.RekursivParentheses(tree)
-	assert.Equal(val, 2)
-}
-
-func TestRekursivParenthesesCalc4(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	var assert = assert.New(test)
-	var tree syntaxbaum.SyntaxBaum
-	var val int
-	tree, _ = schema.ParseExpr("((( ! A0 && A3 ) || A4 ) && A8 )")
-	val = rekursion.RekursivParentheses(tree)
-	assert.Equal(val, 6)
-}
-
-func TestRekursivParenthesesCalc5(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	var assert = assert.New(test)
-	var tree syntaxbaum.SyntaxBaum
-	var val int
-	tree, _ = schema.ParseExpr("! ((( ! A0 && A3 ) || A4 ) && A8 )")
-	val = rekursion.RekursivParentheses(tree)
-	assert.Equal(val, 6)
-}
--- a/codego/aussagenlogik/schema/schema.go
+++ b/codego/aussagenlogik/schema/schema.go
@@ -1,10 +1,9 @@
 package schema

 import (
-	"errors"
-	"logik/aussagenlogik/syntaxbaum"
+	"logik/aussagenlogik/formulae"
 	parser "logik/grammars/aussagenlogik"
-	"strings"
+	"regexp"

 	"github.com/antlr/antlr4/runtime/Go/antlr"
 )
@@ -13,13 +12,13 @@ import (
 * EXPORTS
 * ---------------------------------------------------------------- */

-func ParseExpr(u string) (syntaxbaum.SyntaxBaum, error) {
+func ParseExpr(u string) formulae.Formula {
 	var lexer = createLexer(u)
 	var tokenStream = lexerToTokenStream(lexer)
 	var prs = parser.NewaussagenlogikParser(tokenStream)
 	var t = prs.Start()
-	tree, err := createSyntaxBaum(t, prs)
-	return tree, err
+	tree := createFormula(t, prs)
+	return tree
 }

 /* ---------------------------------------------------------------- *
@@ -39,9 +38,9 @@ func createLexer(u string) antlr.Lexer {
 	return parser.NewaussagenlogikLexer(stream)
 }

-func createSyntaxBaum(tree antlr.Tree, parser antlr.Parser) (syntaxbaum.SyntaxBaum, error) {
+func createFormula(tree antlr.Tree, parser antlr.Parser) formulae.Formula {
 	var ant = antlrTree{tree: tree, parser: &parser}
-	return ant.toSyntaxBaum()
+	return ant.toFormula()
 }

 /* ---------------------------------------------------------------- *
@@ -67,29 +66,18 @@ func (ant antlrTree) getLabel() string {
 }

 func (ant antlrTree) getTextContent() string {
-	var expr string = ant.getLabel()
-	for _, subant := range ant.getChildren() {
+	var expr string = ""
+	var subants = ant.getChildren()
+	if len(subants) == 0 {
+		return ant.getLabel()
+	}
+	for _, subant := range subants {
 		expr += subant.getTextContent()
 	}
 	return expr
 }

-func (ant antlrTree) getTextContentLeaves() string {
-	var expr string = ""
-	var subants = ant.getChildren()
-	if len(subants) == 0 {
-		expr = ant.getLabel()
-	} else {
-		for _, subant := range subants {
-			expr += subant.getTextContent()
-		}
-	}
-	return expr
-}
-
-func (ant antlrTree) toSyntaxBaum() (syntaxbaum.SyntaxBaum, error) {
-	var tree syntaxbaum.SyntaxBaum
-	var err error
+func (ant antlrTree) toFormula() formulae.Formula {
 	var label string = ant.getLabel()
 	var subants = ant.getChildren()
 	var nChildren = len(subants)
@@ -97,79 +85,83 @@ func (ant antlrTree) toSyntaxBaum() (syntaxbaum.SyntaxBaum, error) {
 	switch label {
 	case "start":
 		if nChildren == 1 {
-			return subants[0].toSyntaxBaum()
+			return subants[0].toFormula()
 		}
 	case "open":
 		if nChildren == 1 {
-			return subants[0].toSyntaxBaum()
+			return subants[0].toFormula()
 		}
 	case "closed":
 		switch nChildren {
 		case 1:
-			return subants[0].toSyntaxBaum()
+			return subants[0].toFormula()
+		// expr = ( expr )
 		case 3:
-			return subants[1].toSyntaxBaum()
+			return subants[1].toFormula()
 		}
 	case "atomic":
 		if nChildren == 1 {
-			subant := subants[0]
-			tree = syntaxbaum.SyntaxBaum{}
-			tree.Expr = subant.getTextContentLeaves()
-			tree.Kind = subant.getLabel()
-			tree.Children = [](*syntaxbaum.SyntaxBaum){}
-			tree.Valence = 0
-			return tree, nil
+			return subants[0].toFormula()
 		}
+	case "taut":
+		return formulae.Tautology
+	case "contradiction":
+		return formulae.Contradiction
+	case "atom":
+		name := ant.getTextContent()
+		return formulae.Atom(name)
+	case "generic":
+		re := regexp.MustCompile(`^{|}$`)
+		name := string(re.ReplaceAll([]byte(ant.getTextContent()), []byte("")))
+		return formulae.Generic(name)
 	case "not":
-		if nChildren == 2 { // Children: [NotSymbol, Teilformel]
-			subtree, err := subants[1].toSyntaxBaum()
-			tree = syntaxbaum.SyntaxBaum{}
-			tree.Expr = subants[0].getTextContent() + " " + subtree.Expr
-			tree.Kind = label
-			tree.Children = [](*syntaxbaum.SyntaxBaum){&subtree}
-			tree.Valence = 1
-			return tree, err
+		// NOTE: expr = ! expr
+		if nChildren == 2 {
+			return formulae.Negation(subants[1].toFormula())
 		}
-	case "and2", "and", "or2", "or", "implies":
+	case "and2":
+		// NOTE: expr = expr && expr
+		if nChildren == 3 {
+			return formulae.Conjunction2(subants[0].toFormula(), subants[2].toFormula())
+		}
+	case "or2":
+		// NOTE: expr = expr || expr
+		if nChildren == 3 {
+			return formulae.Disjunction2(subants[0].toFormula(), subants[2].toFormula())
+		}
+	case "implies":
+		// NOTE: expr = expr -> expr
+		if nChildren == 3 {
+			return formulae.Implies(subants[0].toFormula(), subants[2].toFormula())
+		}
+	case "iff":
+		// NOTE: expr = expr <=> expr
+		if nChildren == 3 {
+			return formulae.DoubleImplication(subants[0].toFormula(), subants[2].toFormula())
+		}
+	case "and", "or":
+		// NOTE: expr = expr op expr op ... op expr
 		var n int = int((len(subants) + 1) / 2)
 		if nChildren == 2*n-1 && n >= 2 {
-			var isSymb bool = false
-			var subtrees = make([](*syntaxbaum.SyntaxBaum), n)
+			var subtrees = make([]formulae.Formula, n)
+			var isSymb bool = true
 			var i int = 0
-			var expr string = ""
 			for _, subant := range subants {
 				if isSymb {
-					expr += " " + subant.getTextContent() + " "
-				} else {
-					subtree, err_ := subant.toSyntaxBaum()
-					if err_ != nil {
-						err = err_
-					}
-					subtrees[i] = &subtree
-					expr += " " + subtree.Expr + " "
+					subtrees[i] = subant.toFormula()
 					i++
 				}
+				// NOTE: infix notation: alternatives between expression and symbol
 				isSymb = !isSymb
 			}
-			expr = strings.Trim(expr, " ")
-			var lbrace string = "("
-			var rbrace string = ")"
-			// var lbrace string = "( "
-			// var rbrace string = " )"
-			// if strings.HasPrefix(expr, "(") {
-			// 	lbrace = "("
-			// }
-			// if strings.HasSuffix(expr, ")") {
-			// 	rbrace = ")"
-			// }
-			tree = syntaxbaum.SyntaxBaum{}
-			tree.Expr = lbrace + expr + rbrace
-			tree.Kind = label
-			tree.Children = subtrees
-			tree.Valence = n
-			return tree, err
+			switch label {
+			case "and":
+				return formulae.Conjunction(subtrees)
+			case "or":
+				return formulae.Disjunction(subtrees)
+			}
 		}
 	}

-	return tree, errors.New("Could not parse expression")
+	panic("Could not parse expression")
 }
--- a/codego/aussagenlogik/schema/schema_test.go
+++ b/codego/aussagenlogik/schema/schema_test.go
@@ -5,6 +5,7 @@ package schema_test
 * ---------------------------------------------------------------- */

 import (
+	"logik/aussagenlogik/formulae"
 	"logik/aussagenlogik/schema"
 	"testing"

@@ -17,6 +18,30 @@ import (

 func TestParseExpr(test *testing.T) {
 	var assert = assert.New(test)
-	assert.Equal(0, 0)
-	schema.ParseExpr("A0")
+	var tree formulae.Formula
+
+	tree = schema.ParseExpr("A8712")
+	assert.Equal("A8712", tree.GetExpr())
+	assert.Equal("atom", tree.GetKind())
+	assert.Equal(0, len(tree.GetSubFormulae()))
+
+	tree = schema.ParseExpr("A12")
+	assert.Equal("A12", tree.GetExpr())
+	assert.Equal("atom", tree.GetKind())
+	assert.Equal(0, len(tree.GetSubFormulae()))
+
+	tree = schema.ParseExpr("  ! A5  ")
+	assert.Equal("!A5", tree.GetExpr())
+	assert.Equal("not", tree.GetKind())
+	assert.Equal(1, len(tree.GetSubFormulae()))
+
+	tree = schema.ParseExpr("A0 -> A1")
+	assert.Equal("(A0 -> A1)", tree.GetExpr())
+	assert.Equal("implies", tree.GetKind())
+	assert.Equal(2, len(tree.GetSubFormulae()))
+
+	tree = schema.ParseExpr("(  A0 && ! !  A1) || A2")
+	assert.Equal("((A0 && !!A1) || A2)", tree.GetExpr())
+	assert.Equal("or2", tree.GetKind())
+	assert.Equal(2, len(tree.GetSubFormulae()))
 }
--- a/codego/aussagenlogik/syntaxbaum/syntaxbaum.go
+++ b/codego/aussagenlogik/syntaxbaum/syntaxbaum.go
@@ -1,136 +0,0 @@
-package syntaxbaum
-
-import (
-	"errors"
-	"fmt"
-	"strings"
-)
-
-type SyntaxBaum struct {
-	Kind     string
-	Expr     string
-	Valence  int
-	Children [](*SyntaxBaum)
-}
-
-/* ---------------------------------------------------------------- *
- * METHODS
- * ---------------------------------------------------------------- */
-
-func (tree SyntaxBaum) GetChildren() []SyntaxBaum {
-	var n int = tree.Valence
-	var children = make([]SyntaxBaum, n)
-	for i, subtreePtr := range tree.Children {
-		children[i] = *subtreePtr
-	}
-	return children
-}
-
-func (tree SyntaxBaum) GetChild(indexOpt ...int) (SyntaxBaum, error) {
-	var index int = 0
-	if len(indexOpt) > 0 {
-		index = indexOpt[0]
-	}
-	var subtree SyntaxBaum
-	var err error
-	if 0 <= index && index < tree.Valence {
-		subtree = *(tree.Children[index])
-	} else {
-		err = errors.New(fmt.Sprintf("Instance has no child of index %d !", index))
-	}
-	return subtree, err
-}
-
-func (tree SyntaxBaum) Pretty(preindentOpt ...string) string {
-	var preindent string = ""
-	if len(preindentOpt) > 0 {
-		preindent = preindentOpt[0]
-	}
-	return tree.pretty(preindent, "  ", "", 0)
-}
-
-func (tree SyntaxBaum) pretty(preindent string, tab string, prepend string, depth int) string {
-	var indent string = preindent + strings.Repeat(tab, depth)
-	switch tree.Valence {
-	case 0:
-		switch kind := tree.Kind; kind {
-		case "atom", "generic":
-			return indent + prepend + kind + " " + tree.Expr
-		default:
-			return indent + prepend + kind
-		}
-	default:
-		var lines string = indent + prepend + tree.Kind
-		prepend = "|__ "
-		for _, subtree := range tree.Children {
-			lines += "\n" + subtree.pretty(preindent, tab, prepend, depth+1)
-		}
-		return lines
-	}
-}
-
-// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-// METHODS: Recognitong of Formula-Types
-// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-func (tree SyntaxBaum) isAtom() bool {
-	return tree.Kind == "atom"
-}
-
-func (tree SyntaxBaum) isLiteral() bool {
-	if tree.isAtom() {
-		return true
-	} else if tree.isNegation() {
-		subtree, err := tree.GetChild()
-		if err == nil {
-			return subtree.isAtom()
-		}
-	}
-	return false
-}
-
-func (tree SyntaxBaum) isBeliebig() bool {
-	return tree.Kind == "generic"
-}
-
-func (tree SyntaxBaum) isTrueSymbol() bool {
-	return tree.Kind == "taut"
-}
-
-func (tree SyntaxBaum) isFalseSymbol() bool {
-	return tree.Kind == "contradiction"
-}
-
-func (tree SyntaxBaum) isNegation() bool {
-	return tree.Kind == "not"
-}
-
-func (tree SyntaxBaum) isConjunction() bool {
-	return tree.Kind == "and2"
-}
-
-func (tree SyntaxBaum) isLongConjunction() bool {
-	switch tree.Kind {
-	case "and", "and2":
-		return true
-	default:
-		return false
-	}
-}
-
-func (tree SyntaxBaum) isDisjunction() bool {
-	return tree.Kind == "or2"
-}
-
-func (tree SyntaxBaum) isLongDisjunction() bool {
-	switch tree.Kind {
-	case "or", "or2":
-		return true
-	default:
-		return false
-	}
-}
-
-func (tree SyntaxBaum) isImplication() bool {
-	return tree.Kind == "implies"
-}
--- a/codego/core/utils/utils.go
+++ b/codego/core/utils/utils.go
@@ -1,23 +1,38 @@
 package utils

 import (
+	"encoding/json"
 	"sort"
 	"strings"
 )

 /* ---------------------------------------------------------------- *
- * EXPORTS
+ * METHODS: json
 * ---------------------------------------------------------------- */

-func StrListContains(list []string, x string) bool {
-	for _, obj := range list {
-		if obj == x {
-			return true
-		}
+func JsonToArrayOfStrings(s string, value *[]string) {
+	var err error
+	err = json.Unmarshal([]byte(s), &value)
+	if err != nil {
+		panic(err)
 	}
-	return false
 }

+/* ---------------------------------------------------------------- *
+ * METHODS: conversion
+ * ---------------------------------------------------------------- */
+
+func BoolToInt(cond bool) int {
+	if cond {
+		return 1
+	}
+	return 0
+}
+
+/* ---------------------------------------------------------------- *
+ * METHODS: for integer lists
+ * ---------------------------------------------------------------- */
+
 func Min2(x int, y int) int {
 	if x <= y {
 		return x
@@ -32,6 +47,61 @@ func Max2(x int, y int) int {
 	return y
 }

+func MinList(x []int) int {
+	if len(x) == 0 {
+		panic("Cannot compute the maximum of an empty array.")
+	}
+	var val int = x[0]
+	for i, val_ := range x {
+		if i > 0 {
+			val = Min2(val, val_)
+		}
+	}
+	return val
+}
+
+func MaxList(x []int) int {
+	if len(x) == 0 {
+		panic("Cannot compute the maximum of an empty array.")
+	}
+	var val int = x[0]
+	for i, val_ := range x {
+		if i > 0 {
+			val = Max2(val, val_)
+		}
+	}
+	return val
+}
+
+func SumList(x []int) int {
+	var val int = 0
+	for _, val_ := range x {
+		val += val_
+	}
+	return val
+}
+
+/* ---------------------------------------------------------------- *
+ * METHODS: for string lists
+ * ---------------------------------------------------------------- */
+
+func CopyStringList(list []string) []string {
+	var listCopy = make([]string, len(list))
+	for i, value := range list {
+		listCopy[i] = value
+	}
+	return listCopy
+}
+
+func StrListContains(list []string, x string) bool {
+	for _, obj := range list {
+		if obj == x {
+			return true
+		}
+	}
+	return false
+}
+
 func SortStrings(list *[]string) {
 	sort.Slice(*list, func(i int, j int) bool {
 		u := strings.ToLower((*list)[i])
@@ -68,7 +138,8 @@ func UnionStrings2(list1 []string, list2 []string) []string {
 	return list
 }

-func UnionStringsTo(listTo *[]string, listFrom []string) {
+// assumes that listTo contains no duplicates
+func UnionStringsInPlace(listTo *[]string, listFrom []string) {
 	var mark = make(map[string]bool)
 	for _, item := range listFrom {
 		mark[item] = true
@@ -82,3 +153,23 @@ func UnionStringsTo(listTo *[]string, listFrom []string) {
 		}
 	}
 }
+
+func UnionStringsList(lists [][]string) []string {
+	var list = []string{}
+	for _, list_ := range lists {
+		UnionStringsInPlace(&list, list_)
+	}
+	return list
+}
+
+/* ---------------------------------------------------------------- *
+ * METHODS: for maps
+ * ---------------------------------------------------------------- */
+
+func CopyMapStringBool(m map[string]bool) map[string]bool {
+	var mCopy = map[string]bool{}
+	for key, value := range m {
+		mCopy[key] = value
+	}
+	return mCopy
+}
--- a/codego/core/utils/utils_test.go
+++ b/codego/core/utils/utils_test.go
@@ -12,6 +12,60 @@ import (
 	"github.com/stretchr/testify/assert"
 )

+/* ---------------------------------------------------------------- *
+ * TESTCASE JsonToArrayOfStrings
+ * ---------------------------------------------------------------- */
+
+func TestJsonToArrayOfStrings(test *testing.T) {
+	var assert = assert.New(test)
+	var result []string
+	utils.JsonToArrayOfStrings("[]", &result)
+	assert.ElementsMatch([]string{}, result)
+	utils.JsonToArrayOfStrings("[ \"ganymed\" ]", &result)
+	assert.ElementsMatch([]string{"ganymed"}, result)
+	utils.JsonToArrayOfStrings("[ \"ganymed\", \"io\" ]", &result)
+	assert.ElementsMatch([]string{"ganymed", "io"}, result)
+	assert.Panics(func() { utils.JsonToArrayOfStrings("[ 178 ]", &result) }, "Should panic if converting not a JSON-encoded array of strings!")
+	assert.Panics(func() { utils.JsonToArrayOfStrings("true", &result) }, "Should panic if converting not a JSON-encoded array of strings!")
+	assert.Panics(func() { utils.JsonToArrayOfStrings("", &result) }, "Should panic if converting not a JSON-encoded array of strings!")
+	assert.Panics(func() { utils.JsonToArrayOfStrings("nil", &result) }, "Should panic if converting not a JSON-encoded array of strings!")
+	assert.Panics(func() { utils.JsonToArrayOfStrings("\"somestring\"", &result) }, "Should panic if converting not a JSON-encoded array of strings!")
+	assert.Panics(func() { utils.JsonToArrayOfStrings("'somestring'", &result) }, "Should panic if converting not a JSON-encoded array of strings!")
+}
+
+/* ---------------------------------------------------------------- *
+ * TESTCASE Min2, Max2, MinList, MaxList, SumList
+ * ---------------------------------------------------------------- */
+
+func TestMin(test *testing.T) {
+	var assert = assert.New(test)
+	assert.Equal(3, utils.Min2(3, 8))
+	assert.Equal(8, utils.Min2(100, 8))
+	assert.Equal(50, utils.MinList([]int{50}))
+	assert.Equal(1, utils.MinList([]int{50, 1}))
+	assert.Equal(2, utils.MinList([]int{50, 34, 10, 2, 8, 89}))
+	assert.Panics(func() { utils.MinList([]int{}) }, "Min of list should panic on empty list!")
+}
+
+func TestMax(test *testing.T) {
+	var assert = assert.New(test)
+	assert.Equal(8, utils.Max2(3, 8))
+	assert.Equal(100, utils.Max2(100, 8))
+	assert.Equal(50, utils.MaxList([]int{50}))
+	assert.Equal(50, utils.MaxList([]int{50, 1}))
+	assert.Equal(89, utils.MaxList([]int{50, 34, 10, 2, 8, 89}))
+	assert.Panics(func() { utils.MaxList([]int{}) }, "Max of list should panic on empty list!")
+}
+
+func TestSumList(test *testing.T) {
+	var assert = assert.New(test)
+	assert.Equal(0, utils.SumList([]int{}), "Sum of empty list should be 0.")
+	assert.Equal(2198, utils.SumList([]int{2198}))
+	assert.Equal(15, utils.SumList([]int{0, 1, 2, 3, 4, 5}))
+	assert.Equal(1038, utils.SumList([]int{1000, 1, 37}))
+	assert.Equal(237, utils.SumList([]int{1000, -800, 37}))
+}
+
 /* ---------------------------------------------------------------- *
 * TESTCASE SortStrings
 * ---------------------------------------------------------------- */
@@ -19,8 +73,9 @@ import (
 func TestSortStrings(test *testing.T) {
 	var assert = assert.New(test)
 	var list = []string{"katze", "Hund", "baby", "Pluto", "Saturn", "Mond"}
+	// NOTE: here use .Equal and not .ElementsMatch, since order important.
 	utils.SortStrings(&list)
-	assert.Equal(list, []string{"baby", "Hund", "katze", "Mond", "Pluto", "Saturn"})
+	assert.Equal([]string{"baby", "Hund", "katze", "Mond", "Pluto", "Saturn"}, list)
 }

 /* ---------------------------------------------------------------- *
@@ -31,11 +86,11 @@ func TestFilterStrings(test *testing.T) {
 	var assert = assert.New(test)
 	var list = []string{"abram", "aaron", "aardvark", "aarhus", "alaska", "eel", "aal"}
 	var list2 = utils.FilterStrings(&list, func(x string) bool { return strings.HasPrefix(x, "aa") })
-	assert.Equal(list2, []string{"aaron", "aardvark", "aarhus", "aal"})
+	assert.ElementsMatch([]string{"aaron", "aardvark", "aarhus", "aal"}, list2)
 }

 /* ---------------------------------------------------------------- *
- * TESTCASE UnionStrings2, UnionStringsTo
+ * TESTCASE UnionStrings2, UnionStringsInPlace, UnionStringsList
 * ---------------------------------------------------------------- */

 func TestUnionStrings2(test *testing.T) {
@@ -43,15 +98,22 @@ func TestUnionStrings2(test *testing.T) {
 	var list1 = []string{"red", "blue", "blue", "green", "blue", "grey", "black", "green"}
 	var list2 = []string{"yellow", "orange", "lila", "red"}
 	var list = utils.UnionStrings2(list1, list2)
-	utils.SortStrings(&list)
-	assert.Equal(list, []string{"black", "blue", "green", "grey", "lila", "orange", "red", "yellow"})
+	assert.ElementsMatch([]string{"black", "blue", "green", "grey", "lila", "orange", "red", "yellow"}, list)
 }

-func UnionStringsTo(test *testing.T) {
+func TestUnionStringsInPlace(test *testing.T) {
 	var assert = assert.New(test)
-	var list1 = []string{"red", "blue", "blue", "green"}
-	var list2 = []string{"yellow", "red", "black"}
-	utils.UnionStringsTo(&list1, list2)
-	utils.SortStrings(&list1)
-	assert.Equal(list1, []string{"black", "blue", "green", "red", "yellow"})
+	var list1 = []string{"red", "blue", "green"}
+	var list2 = []string{"yellow", "red", "blue", "red", "black"}
+	utils.UnionStringsInPlace(&list1, list2)
+	assert.ElementsMatch([]string{"black", "blue", "green", "red", "yellow"}, list1)
+}
+
+func TestUnionStringsList(test *testing.T) {
+	var assert = assert.New(test)
+	var list []string
+	var lists [][]string
+	lists = [][]string{{"red", "blue", "blue", "green"}, {"yellow", "red", "black"}}
+	list = utils.UnionStringsList(lists)
+	assert.ElementsMatch([]string{"black", "blue", "green", "red", "yellow"}, list)
 }
--- a/codego/go.mod
+++ b/codego/go.mod
@@ -3,11 +3,12 @@ module logik
 go 1.16

 require (
-	github.com/antlr/antlr4/runtime/Go/antlr v0.0.0-20210506161523-0a1c3e3ce1ca
+	github.com/antlr/antlr4/runtime/Go/antlr v0.0.0-20210510155620-3601dcad5d17
 	github.com/joho/godotenv v1.3.0
 	github.com/lithammer/dedent v1.1.0
 	// siehe https://pkg.go.dev/github.com/stretchr/testify/assert
 	// und https://github.com/stretchr/testify
 	github.com/stretchr/testify v1.7.0
-	golang.org/x/tools v0.1.0
+	golang.org/x/crypto v0.0.0-20200622213623-75b288015ac9 // indirect
+	golang.org/x/tools v0.1.1
 )
--- a/codego/go.sum
+++ b/codego/go.sum
@@ -1,5 +1,5 @@
-github.com/antlr/antlr4/runtime/Go/antlr v0.0.0-20210506161523-0a1c3e3ce1ca h1:cZZsTEHO/8dZcxfjctHHbnEDLKdvyjUjWLNchKdgO94=
-github.com/antlr/antlr4/runtime/Go/antlr v0.0.0-20210506161523-0a1c3e3ce1ca/go.mod h1:F7bn7fEU90QkQ3tnmaTx3LTKLEDqnwWODIYppRQ5hnY=
+github.com/antlr/antlr4/runtime/Go/antlr v0.0.0-20210510155620-3601dcad5d17 h1:fLGaJgAYjJwsFGRMsKZ4POcylLOXlLDmUAEuOLllvyU=
+github.com/antlr/antlr4/runtime/Go/antlr v0.0.0-20210510155620-3601dcad5d17/go.mod h1:F7bn7fEU90QkQ3tnmaTx3LTKLEDqnwWODIYppRQ5hnY=
 github.com/davecgh/go-spew v1.1.0 h1:ZDRjVQ15GmhC3fiQ8ni8+OwkZQO4DARzQgrnXU1Liz8=
 github.com/davecgh/go-spew v1.1.0/go.mod h1:J7Y8YcW2NihsgmVo/mv3lAwl/skON4iLHjSsI+c5H38=
 github.com/joho/godotenv v1.3.0 h1:Zjp+RcGpHhGlrMbJzXTrZZPrWj+1vfm90La1wgB6Bhc=
@@ -12,26 +12,28 @@ github.com/stretchr/objx v0.1.0 h1:4G4v2dO3VZwixGIRoQ5Lfboy6nUhCyYzaqnIAPPhYs4=
 github.com/stretchr/objx v0.1.0/go.mod h1:HFkY916IF+rwdDfMAkV7OtwuqBVzrE8GR6GFx+wExME=
 github.com/stretchr/testify v1.7.0 h1:nwc3DEeHmmLAfoZucVR881uASk0Mfjw8xYJ99tb5CcY=
 github.com/stretchr/testify v1.7.0/go.mod h1:6Fq8oRcR53rry900zMqJjRRixrwX3KX962/h/Wwjteg=
-github.com/yuin/goldmark v1.2.1/go.mod h1:3hX8gzYuyVAZsxl0MRgGTJEmQBFcNTphYh9decYSb74=
+github.com/yuin/goldmark v1.3.5/go.mod h1:mwnBkeHKe2W/ZEtQ+71ViKU8L12m81fl3OWwC1Zlc8k=
 golang.org/x/crypto v0.0.0-20190308221718-c2843e01d9a2/go.mod h1:djNgcEr1/C05ACkg1iLfiJU5Ep61QUkGW8qpdssI0+w=
 golang.org/x/crypto v0.0.0-20191011191535-87dc89f01550/go.mod h1:yigFU9vqHzYiE8UmvKecakEJjdnWj3jj499lnFckfCI=
 golang.org/x/crypto v0.0.0-20200622213623-75b288015ac9/go.mod h1:LzIPMQfyMNhhGPhUkYOs5KpL4U8rLKemX1yGLhDgUto=
-golang.org/x/mod v0.3.0/go.mod h1:s0Qsj1ACt9ePp/hMypM3fl4fZqREWJwdYDEqhRiZZUA=
+golang.org/x/mod v0.4.2/go.mod h1:s0Qsj1ACt9ePp/hMypM3fl4fZqREWJwdYDEqhRiZZUA=
 golang.org/x/net v0.0.0-20190404232315-eb5bcb51f2a3/go.mod h1:t9HGtf8HONx5eT2rtn7q6eTqICYqUVnKs3thJo3Qplg=
 golang.org/x/net v0.0.0-20190620200207-3b0461eec859/go.mod h1:z5CRVTTTmAJ677TzLLGU+0bjPO0LkuOLi4/5GtJWs/s=
-golang.org/x/net v0.0.0-20201021035429-f5854403a974/go.mod h1:sp8m0HH+o8qH0wwXwYZr8TS3Oi6o0r6Gce1SSxlDquU=
+golang.org/x/net v0.0.0-20210405180319-a5a99cb37ef4/go.mod h1:p54w0d4576C0XHj96bSt6lcn1PtDYWL6XObtHCRCNQM=
 golang.org/x/sync v0.0.0-20190423024810-112230192c58/go.mod h1:RxMgew5VJxzue5/jJTE5uejpjVlOe/izrB70Jof72aM=
-golang.org/x/sync v0.0.0-20201020160332-67f06af15bc9/go.mod h1:RxMgew5VJxzue5/jJTE5uejpjVlOe/izrB70Jof72aM=
+golang.org/x/sync v0.0.0-20210220032951-036812b2e83c/go.mod h1:RxMgew5VJxzue5/jJTE5uejpjVlOe/izrB70Jof72aM=
 golang.org/x/sys v0.0.0-20190215142949-d0b11bdaac8a/go.mod h1:STP8DvDyc/dI5b8T5hshtkjS+E42TnysNCUPdjciGhY=
 golang.org/x/sys v0.0.0-20190412213103-97732733099d/go.mod h1:h1NjWce9XRLGQEsW7wpKNCjG9DtNlClVuFLEZdDNbEs=
-golang.org/x/sys v0.0.0-20200930185726-fdedc70b468f/go.mod h1:h1NjWce9XRLGQEsW7wpKNCjG9DtNlClVuFLEZdDNbEs=
-golang.org/x/sys v0.0.0-20210119212857-b64e53b001e4/go.mod h1:h1NjWce9XRLGQEsW7wpKNCjG9DtNlClVuFLEZdDNbEs=
+golang.org/x/sys v0.0.0-20201119102817-f84b799fce68/go.mod h1:h1NjWce9XRLGQEsW7wpKNCjG9DtNlClVuFLEZdDNbEs=
+golang.org/x/sys v0.0.0-20210330210617-4fbd30eecc44/go.mod h1:h1NjWce9XRLGQEsW7wpKNCjG9DtNlClVuFLEZdDNbEs=
+golang.org/x/sys v0.0.0-20210510120138-977fb7262007/go.mod h1:oPkhp1MJrh7nUepCBck5+mAzfO9JrbApNNgaTdGDITg=
+golang.org/x/term v0.0.0-20201126162022-7de9c90e9dd1/go.mod h1:bj7SfCRtBDWHUb9snDiAeCFNEtKQo2Wmx5Cou7ajbmo=
 golang.org/x/text v0.3.0/go.mod h1:NqM8EUOU14njkJ3fqMW+pc6Ldnwhi/IjpwHt7yyuwOQ=
 golang.org/x/text v0.3.3/go.mod h1:5Zoc/QRtKVWzQhOtBMvqHzDpF6irO9z98xDceosuGiQ=
 golang.org/x/tools v0.0.0-20180917221912-90fa682c2a6e/go.mod h1:n7NCudcB/nEzxVGmLbDWY5pfWTLqBcC2KZ6jyYvM4mQ=
 golang.org/x/tools v0.0.0-20191119224855-298f0cb1881e/go.mod h1:b+2E5dAYhXwXZwtnZ6UAqBI28+e2cm9otk0dWdXHAEo=
-golang.org/x/tools v0.1.0 h1:po9/4sTYwZU9lPhi1tOrb4hCv3qrhiQ77LZfGa2OjwY=
-golang.org/x/tools v0.1.0/go.mod h1:xkSsbof2nBLbhDlRMhhhyNLN/zl3eTqcnHD5viDpcZ0=
+golang.org/x/tools v0.1.1 h1:wGiQel/hW0NnEkJUk8lbzkX2gFJU6PFxf1v5OlCfuOs=
+golang.org/x/tools v0.1.1/go.mod h1:o0xws9oXOQQZyjljx8fwUC0k7L1pTE6eaCbjGeHmOkk=
 golang.org/x/xerrors v0.0.0-20190717185122-a985d3407aa7/go.mod h1:I/5z698sn9Ka8TeJc9MKroUUfqBBauWjQqLJ2OPfmY0=
 golang.org/x/xerrors v0.0.0-20191011141410-1b5146add898/go.mod h1:I/5z698sn9Ka8TeJc9MKroUUfqBBauWjQqLJ2OPfmY0=
 golang.org/x/xerrors v0.0.0-20200804184101-5ec99f83aff1/go.mod h1:I/5z698sn9Ka8TeJc9MKroUUfqBBauWjQqLJ2OPfmY0=
--- a/codego/grammars/aussagenlogik.g4
+++ b/codego/grammars/aussagenlogik.g4
@@ -1,33 +1,37 @@
 grammar aussagenlogik;

 // Standardtokens:
-NUMBER: [0-9]+;
+NUMBER: [0-9];
+ZERO: ~[a-zA-Z0-9][0]; // negatives Look-Behind nötig, um konfliktierendes Lexing zu vermeiden
+ONE: ~[a-zA-Z0-9][1];  // ""
 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_IMPL: ('->'|'=>');
+SYMB_IFF:  ([<][-]+[>]|[<][=]+[>]|'iff');
+SYMB_IMPL: (~[<][-]+[>]|~[<][=]+[>]);

 // Rules
 start: open <EOF> | closed <EOF>;

 closed: atomic | not | LBRACE open RBRACE;
-open: and2 | and | or2 | or | implies;
+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}, {F1}, usw.
-// // generic: LCURLYBRACE (.*?) RCURLYBRACE;
-// FIXME: dieses Schema führt zu Konflikten
+atomic: taut | contradiction | atom | generic;
+taut:  (ONE|'true');
+contradiction: (ZERO|'false');
+atom: 'A' NUMBER+;
+// 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;
@@ -39,3 +43,5 @@ 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;
--- a/codego/main.go
+++ b/codego/main.go
@@ -1,12 +1,12 @@
 package main

 import (
-	"encoding/json"
 	"fmt"
-	"logik/aussagenlogik/rekursion"
+	"logik/aussagenlogik/formulae"
+	"logik/aussagenlogik/recursion"
 	"logik/aussagenlogik/schema"
-	"logik/aussagenlogik/syntaxbaum"
 	env "logik/core/environment"
+	"logik/core/utils"
 	"strings"

 	"github.com/lithammer/dedent"
@@ -21,6 +21,7 @@ type dataType struct {

 type resultsType struct {
 	eval         int
+	nnf          formulae.Formula
 	atoms        []string
 	depth        int
 	length       int
@@ -31,23 +32,10 @@ var data dataType

 func main() {
 	// Extrahiere Daten
-	err := getData()
-	if err != nil {
-		return
-	}
+	getData()
 	// Ausdruck -> Syntaxbaum
-	tree, err := schema.ParseExpr(data.expr)
-	if err != nil {
-		return
-	}
-	// Methoden ausführen:
-	results := resultsType{
-		eval:         rekursion.RekursivEval(tree, data.interpretation),
-		atoms:        rekursion.RekursivAtoms(tree),
-		depth:        rekursion.RekursivDepth(tree),
-		length:       rekursion.RekursivLength(tree),
-		nParentheses: rekursion.RekursivParentheses(tree),
-	}
+	tree := schema.ParseExpr(data.expr)
+	results := getResults(tree)
 	// Resultate anzeigen:
 	displayResults(tree, results)
 }
@@ -56,15 +44,25 @@ func main() {
 // SONSTIGE METHODEN
 // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

-func getData() error {
+func getData() {
 	env.ENV_FILE_NAME = DATA_ENV
 	data.expr = env.ReadEnvKey("expr")
 	s := env.ReadEnvKey("interpretation")
-	err := json.Unmarshal([]byte(s), &data.interpretation)
-	return err
+	utils.JsonToArrayOfStrings(s, &data.interpretation)
 }

-func displayResults(tree syntaxbaum.SyntaxBaum, results resultsType) {
+func getResults(tree formulae.Formula) resultsType {
+	return resultsType{
+		eval:         recursion.Eval(tree, data.interpretation),
+		nnf:          recursion.NNF(tree),
+		atoms:        recursion.Atoms(tree),
+		depth:        recursion.FmlDepth(tree),
+		length:       recursion.FmlLength(tree),
+		nParentheses: recursion.NrParentheses(tree),
+	}
+}
+
+func displayResults(tree formulae.Formula, results resultsType) {
 	fmt.Println(fmt.Sprintf(
 		dedent.Dedent(`
 		Syntaxbaum von
@@ -74,18 +72,20 @@ func displayResults(tree syntaxbaum.SyntaxBaum, results resultsType) {

 		Für I = {%[3]s} und F wie oben gilt
 		eval(F, I)      = %[4]d;
-		atoms(F)        = {%[5]s};  <- *
-		depth(F)        = %[6]d;  <- *
-		length(F)       = %[7]d;  <- *
-		#parentheses(F) = %[8]d;  <- *
+		F^NNF           = %[5]s;
+		atoms(F)        = {%[6]s};  <- *
+		depth(F)        = %[7]d;  <- *
+		length(F)       = %[8]d;  <- *
+		#parentheses(F) = %[9]d;  <- *

 		* noch nicht implementiert!
 		Challenge: schreibe diese Methoden! (siehe README.md)
 		`),
-		tree.Expr,
+		tree.GetExpr(),
 		tree.Pretty("    "),
 		strings.Join(data.interpretation, ", "),
 		results.eval,
+		results.nnf.GetExpr(),
 		// string(results.atoms),
 		strings.Join(results.atoms, ", "),
 		results.depth,
--- a/codego/scripts/build.sh
+++ b/codego/scripts/build.sh
@@ -16,8 +16,7 @@ function call_go() {
 }

 function check_requirements() {
-    [ -f "go.sum" ] && rm "go.sum";
-    call_go get "$( cat requirements )";
+    call_go get "$( cat scripts/requirements )";
 }

 function get_antlr() {
@@ -37,6 +36,7 @@ function precompile_grammars() {
    local name;
    ! [ -f "grammars/antlr.jar" ] && get_antlr; # <- lädt antl.jar herunter, wenn fehlt
    pushd grammars >> $NULL;
+        rm -rf .antlr; # <- wird automatisch erzeugt, aber wir brauche dies nicht
        while read fname; do
            ( [ "$fname" == "" ] || ! [ -f "$fname" ] ) && continue;
            name="$( echo "$fname" | sed -E "s/^(.*)\.g4$/\1/g" )";
@@ -47,14 +47,15 @@ function precompile_grammars() {
 }

 function compile_programme() {
-    [ -f "main" ] && rm "main";
+    [ -f "dist/main" ] && rm "dist/main";
    echo -e "\033[92;1mGO\033[0m kompiliert \033[1mmain.go\033[0m";
-    call_go build "main.go";
+    call_go build -o dist/main "main.go";
+    ! [ -f "dist/main" ] && exit 1;
 }

 function run_programme() {
    echo -e "\033[92;1mGO\033[0m kompiliertes Programm wird ausgeführt";
-    ./main;
+    ./dist/main;
 }

 ################################
--- a/codego/scripts/requirements
+++ b/codego/scripts/requirements
@@ -0,0 +1,5 @@
+github.com/joho/godotenv@v1.3.0
+github.com/lithammer/dedent
+github.com/antlr/antlr4/runtime/Go/antlr
+github.com/stretchr/testify
+golang.org/x/tools
--- a/codego/scripts/test.sh
+++ b/codego/scripts/test.sh
@@ -8,18 +8,22 @@
 # HILFSMETHODEN
 ################################

+export TEST_VERBOSE=false # <- true: unittest mit verbose output
+export TEST_TIMEOUT="10s"
+
 function call_go() {
    go $@;
 }

 function check_requirements() {
-    [ -f "go.sum" ] && rm "go.sum";
-    call_go get "$( cat requirements )";
+    call_go get "$( cat scripts/requirements )";
 }

 function run_unittests(){
    echo -e "\033[1mUNITTESTS\033[0m\n";
-    call_go test -v -timeout 60s -count 1 -run "^Test[A-Z].*" "logik" "./...";
+    local verbose_opt="";
+    ( $TEST_VERBOSE ) && verbose_opt="-v"
+    call_go test $verbose_opt -timeout $TEST_TIMEOUT -count 1 -run "^Test[A-Z].*" "logik" "./...";
 }

 ################################
--- a/notes/.gitignore
+++ b/notes/.gitignore
@@ -1,4 +0,0 @@
-*
-!/.gitignore
-
-!/*.pdf
--- a/notes/glossar.md
+++ b/notes/glossar.md
@@ -0,0 +1,69 @@
+<style>
+    table tbody tr td {
+        vertical-align: top;
+    }
+    table tbody tr td:nth-child(1) {
+        font-size: 10pt;
+    }
+    table tbody tr td:nth-child(2), table tbody tr td:nth-child(3) {
+        font-size: 8pt;
+    }
+</style>
+
+# Glossar #
+
+| Symbol | Referenz (im Skript) | Kurze Beschreibung |
+| :----- | :------------------- | :----------------- |
+| `¬` | §8 Definition, VL2, Seite 8 | Negationsjunktor („nicht“) |
+| `⋀` | §8 Definition, VL2, Seite 8 | Konjunktionsjunktor („und“) |
+| `⋁` | §8 Definition, VL2, Seite 8 | Disunktionsjunktor („oder“) |
+| `⟶` | VL2, Seite 47 | **Abkürzung** für Implikation |
+| `⟷` | VL2, Seite 47 | **Abkürzung** für Doppeltimplikation |
+| `⊨` | §9 Definition, VL2, Seite 34 | Erfüllbarkeitsbeziehung: `I ⊨ F` gdw. `I` erf. `F` |
+| `=` | — | `F = G` gdw. `F` und `G` _dieselbe_ Formel sind |
+| `≡` | §13 Definition, VL3, Seite 11 | `F ≡ G` gdw. `F`, `G` **semantisch** äquivalent |
+| `{...}_⋀` | §39 Definition, VL5, Seite 108 | Mengendarstellung von Disjunktionsglied |
+| ~~-`𝒜`-~~ | — | (**Eintrag ignorieren**: kommt in VL nicht vor!) |
+| AL | (VL2–VL6) | Aussagenlogik |
+| `Aᵢ` | §8 Definition, VL2, Seite 8 | das _i_-te Atom in der AL-Sprache |
+| `Atome(·)` | §5 Definition, V2, Seite 14 | `Atome(F) =` Menge aller Atome in `F` |
+| bereinigt | §76 Definition, VL10, Seite 21 | äqv. Formel, Variablensubstitution, so dass jede Var nur gebunden od. frei vorkommt |
+| `𝔠` | §88+§89 Definition, VL11, Seiten 9+14 | (Fraktur c) die Herbrand-Konstante („out of bounds“) |
+| DNF | §22 Definition, VL3, Seite 55 | disjunktive Normalform für AL und PL |
+| erfüllbar | §10 Definition, VL2, Seite 68 | Die „klassischen“ Probleme |
+| `eval(·,·)` | §16 Algorithmus, VL3, Seite 30 | Evaluation: `eval(F,I)=1` gdw. `I ⊨ F` |
+| `ℱ` | §8 Definition, VL2, Seite 8 | Die „AL-Sprache“, Menge aller AL-Formeln |
+| `Fun(t)` | §63 Definition, VL9, Seite 18 | alle Variablen, Konstanten, Fktsymbole in Term `t` |
+| `FV(F)` | §57 Definition, VL8, Seite 27 | Menge freier Variablen in `F` (für Terme siehe `var(t)`) |
+| `g`, `g´`, `g´´`, ... | | Skolemisierung: ∃-Eliminierung mittels Funktionen, die Abhängigkeiten ausdrücken |
+| `GV(F)` | §75 Definition, VL10, Seite 17 | Menge gebundener Variablen in `F`|
+| `H,H(F)` | §88 Definition, VL11, Seite 9 | Herbrand-Symbole, Herbrand-Universum |
+| Herbrand-Interpretation | §89 Definition, VL11, Seite 14 | Interpretation für ein Herbrand-Modell. Alle H-M haben die gleiche Interpretationen von Termen. Nur Relationen können anders interpretiert werden. |
+| KNF | §22 Definition (AL), VL3, Seite 55; §85 Definition (PL), VL10, Seite 89 | konjunktive Normalform für AL und PL |
+| `ℒ` | §8 Definition, VL2, Seite 8 | Die Menge der Literale |
+| PL | (ab VL7) | Prädikatenlogik |
+| NNF | §18 Definition (AL), VL3, Seite 39; §73 Definition (PL), VL10, Seite 8 | Negationsnormalform - Negation nur bei Literalen |
+| PNF | §78 Definition, VL10, Seite 37 | Pränexnormalform - Kette von Quantoren um einen Q-freien Teil |
+| `ℛ,ℛ⁽ᵏ⁾`| §52 Definition, VL7, Seite 72 | Menge der (`k`-stelligen) Relationssymbole, `k≥0`. |
+| `res(·)` | §41–43 Definition, VL6, Seiten 37–43 | `res(F) =` Menge aller Resolventen aus Disjunktionsgliedern aus `F` |
+| `Res(·)` | §43 Definition, VL6, Seite 43 | `Res(F) = F ∪ res(F)` |
+| `Res⁽ⁿ⁾(·)` | §43 Definition, VL6, Seite 43 | `Res(Res(···Res(F)···))`, _n_ Mal |
+| `Res*(·)` | §43 Definition, VL6, Seite 43 | Resolutionshülle |
+| `𝒮,𝒮⁽ᵏ⁾`| §52 Definition, VL7, Seite 72 | Menge der (`k`-stelligen) Funktionssymbole, `k≥0`. **Beachte:** für `k=0` sind dies die Konstanten! |
+| Skolemform | §81, VL10, Seite 62 | äqv. Formel, in der alle Existenzquantoren eliminiert wurden |
+| strukturelle Ind | §6 Theorem, VL2, Seite 24 | allgemeine Induktion über die Teilformelbeziehung |
+| strukturelle Rek | §4 Theorem, VL2, Seite 12 | rekursive Konstruktionschemata über die Teilformelbeziehung |
+| `Sym(F)` | §64 Definition, VL9, Seite 20 | alle „relevanten“ Symbole in `F`: alle **freien** Vars, alle Konstanten, Fktsymbole, Relnsymbole |
+| `𝒯` | §53 Definition, VL7, Seite 74 | Menge der Terme in PL |
+| tautologisch | §10 Definition, VL2, Seite 68 | Die „klassischen“ Probleme |
+| `TF(·)` | §35 Definition, VL5, Seite 56 | `TF(F) =` Menge aller Teilformeln in `F` (inkl. `F` selbst) |
+| `tᵥ` | §37 Definition, VL5, Seite 64 | Abbildung, die Teilformeln auf Literale abbildet |
+| `tseiᵥ` | §37 Definition, VL5, Seite 64 | Tseitin-Transformation |
+| unerfüllbar | §10 Definition, VL2, Seite 68 | Die „klassischen“ Probleme |
+| `𝒱` | §52 Definition, VL7, Seite 72 | Menge der Variablen in PL |
+| `var(t)` | §55 Definition, VL8, Seite 20 | Menge der Variablen in `t` (für Fml siehe `FV(F)`) |
+| widerlegbar | §10 Definition, VL2, Seite 68 | Die „klassischen“ Probleme |
+
+... (wird fortgesetzt)
+
+**ACHTUNG:** Seitennr können abweichen.
--- a/notes/woche10.pdf
+++ b/notes/woche10.pdf
--- a/notes/woche12.pdf
+++ b/notes/woche12.pdf
--- a/notes/woche14.pdf
+++ b/notes/woche14.pdf
--- a/notes/woche4.pdf
+++ b/notes/woche4.pdf
--- a/notes/woche5.pdf
+++ b/notes/woche5.pdf
--- a/notes/woche8.pdf
+++ b/notes/woche8.pdf
--- a/protocol/README.md
+++ b/protocol/README.md
@@ -2,9 +2,30 @@

 Inhaltsverzeichnis

- [Vorlesungswoche 1](./woche1.md)
- [Vorlesungswoche 2](./woche2.md) Erste Übung: Organisatorisches
- [Vorlesungswoche 3](./woche3.md) Seminaraufgaben aus Blatt 1
- [Vorlesungswoche 4](./woche4.md) ~~Hausaufgaben aus Blatt ??~~ Spezielle Themen
- [Vorlesungswoche 5](./woche5.md) Seminaraufgaben aus Blatt 2
- [Vorlesungswoche 6](./woche6.md) Hausaufgaben aus Blatt 1
+- [Vorlesungswoche 1](./woche1.md) (_keine Übung_)
+- [Vorlesungswoche 2](./woche2.md) Erste Übung: Organisatorisches.
+- [Vorlesungswoche 3](./woche3.md) Semaufg Blatt 1; [BBB Aufzeichnung](https://t1p.de/tjiu).
+- [Vorlesungswoche 4](./woche4.md) Spezielle Themen; [Zoom Aufzeichnung](https://t1p.de/91vz).
+- [Vorlesungswoche 5](./woche5.md) Semaufg Blatt 2; [Zoom Aufzeichnung](https://t1p.de/ny7n).
+- [Vorlesungswoche 6](./woche6.md) HA Blatt 1; [Zoom Aufzeichnung](https://t1p.de/m431).
+- [Vorlesungswoche 7](./woche7.md) (_keine Übung: ...Pfingsten..._)
+- [Vorlesungswoche 8](./woche8.md) Semaufg Blatt 3; [Zoom Aufzeichnung](https://t1p.de/fmok).
+- [Vorlesungswoche 9](./woche9.md) HA Blatt 2; [Zoom Aufzeichnung](https://t1p.de/8vmh).
+- [Vorlesungswoche 10](./woche10.md) Semaufg Blatt 4; [Zoom Aufzeichnung](https://t1p.de/fpv5).
+- [Vorlesungswoche 11](./woche11.md) HA Blatt 3; [Zoom Aufzeichnung](https://t1p.de/626y).
+- [Vorlesungswoche 12](./woche12.md) Semaufg Blatt 5; [Zoom Aufzeichnung](https://t1p.de/n4bt).
+  - (Zusatz) Seminaraufgabe 5.5 [Zoom Aufzeichnung](https://t1p.de/bnlj).
+- [Vorlesungswoche 13](./woche13.md) HA Blatt 4; [Zoom Aufzeichnung](https://t1p.de/76qo).
+- [Vorlesungswoche 14](./woche14.md) Semaufg Blatt 6; [Zoom Aufzeichnung](https://t1p.de/slya).
+- [Vorlesungswoche 15](./woche15.md) HA Blatt 5; [Zoom Aufzeichnung](https://t1p.de/3xsm).
+
+**Notizen**
+
+- Für den BBB-Raum bzw. die Zoom-Aufzeichnungen braucht man einen **Code** (siehe Moodle).
+- Klausurdatum wird noch angekündigt.
+  Je nachdem können wir ggf. 1–2 Stunden für Vorklausurfragen organisieren.
+- In [**Vorlesungswoche 16**](./woche16.md) wird eine zusätzliche Übung angeboten:
+  <br/>
+  allgemeine Fragestellung von Studierenden.
+  - Zoom-Raum mit dem üblichen Code.
+  - Dies wird _nicht_ aufgezeichnet werden!
--- a/protocol/woche10.md
+++ b/protocol/woche10.md
@@ -0,0 +1,23 @@
+# Vorlesungswoche 10 (14.–20. Juni) #
+
+Handnotizen findet man unter [notes/woche10.pdf](./../notes/woche10.pdf).
+
+## Agenda ##
+
+- [x] 2–5 min Organisatorisches
+- [x] Serie 4, Seminaraufgaben besprechen
+    - [x] SemA 4.1
+    - [x] SemA 4.2
+    - [x] SemA 4.3
+    - [x] SemA 4.4
+    - [x] SemA 4.5
+    - Anmerkungen zu HA
+- [x] restliche Zeit für allg. Fragen
+
+## Nächste Woche ##
+
+- HA aus Blatt 3.
+
+### TODOs (Studierende) ###
+
+- am ÜB 4 weiter arbeiten.
--- a/protocol/woche11.md
+++ b/protocol/woche11.md
@@ -0,0 +1,20 @@
+# Vorlesungswoche 11 (21.–27. Juni) #
+
+## Agenda ##
+
+- [x] 2–5 min Organisatorisches
+- [x] Serie 3, Hausaufgaben besprechen
+    - [x] allgemeines Feedback
+    - [x] HA 3.1
+    - [x] HA 3.2
+    - [x] HA 3.3
+- [x] restliche Zeit für allg. Fragen
+    - Frage über VPN Zugang bis nächste Woche zu klären.
+
+## Nächste Woche ##
+
+- Seminaraufgaben aus Blatt 5.
+
+### TODOs (Studierende) ###
+
+- ÜB 4 bis **Do 24.06.** um 22:00 abgeben!
--- a/protocol/woche12.md
+++ b/protocol/woche12.md
@@ -0,0 +1,43 @@
+# Vorlesungswoche 12 (28. Juni – 4. Juli) #
+
+## Agenda ##
+
+- [x] 2–5 min Organisatorisches
+- [x] Serie 5, Seminaraufgaben besprechen
+    - [x] SemA 5.1
+    - [x] SemA 5.2
+    - [x] SemA 5.3
+    - [x] SemA 5.4
+    - ~~[ ] (Zusatz) SemA 5.5~~ ---> siehe Aufzeichnung
+- [x] restliche Zeit für allg. Fragen
+    - Alternativer Beweis von (d) durch Argument:
+
+        ```
+        »Sonst wären F und F^skol sem. äquivalent,
+        aber das ist nicht i. A. der Fall.«
+        ```
+
+        Da wir aber uns aber auf einer Instanz beschränken,
+        passt dieser Ansatz nicht.
+        Wir müssen im Einzelfall prüfen.
+        Vgl. Unterschied zw.
+
+        ```
+        1. Es ist nicht so, dass (F ≡ F^skol) für alle F
+        ```
+        und
+
+        ```
+        2. Für alle F, es ist nicht so dass (F ≡ F^skol).
+        ```
+
+        Wir haben nur 1 und damit kann es durchaus sein,
+        dass für einzelne Fälle F, F^skol schon sem. äqv. sind.
+
+## Nächste Woche ##
+
+- HA aus Blatt 4.
+
+### TODOs (Studierende) ###
+
+- am ÜB 5 weiter arbeiten.
--- a/protocol/woche13.md
+++ b/protocol/woche13.md
@@ -0,0 +1,21 @@
+# Vorlesungswoche 13 (5.–11. Juli) #
+
+## Agenda ##
+
+- [x] 2–5 min Organisatorisches
+- [x] Serie 4, Hausaufgaben besprechen
+    - [x] allgemeines Feedback
+    - [x] HA 4.1
+    - [x] HA 4.2
+    - [x] HA 4.3
+    - [x] HA 4.4
+    - [x] HA 4.5
+- [x] restliche Zeit für allg. Fragen
+
+## Nächste Woche ##
+
+- Seminaraufgaben aus Blatt 6.
+
+### TODOs (Studierende) ###
+
+- ÜB 5 bis **Do 08.07.** um 22:00 abgeben!
--- a/protocol/woche14.md
+++ b/protocol/woche14.md
@@ -0,0 +1,23 @@
+# Vorlesungswoche 14 (12.–18. Juli) #
+
+## Agenda ##
+
+- [x] 2–5 min Organisatorisches
+    - **Beachte:** HA zu Serie 6 werden leider nicht besprochen!
+    - Notenstand in Moodle, Schwellwert 59 Pkt
+    - Zusatzübung
+- [x] Serie 6, Seminaraufgaben besprechen
+    - [x] SemA 6.1
+    - [x] SemA 6.2
+    - [x] SemA 6.3
+    - [x] SemA 6.4
+    - ~~[ ] (Zusatz) SemA 6.5~~ ---> siehe Aufzeichnung in Moodle
+- [x] restliche Zeit für allg. Fragen
+
+## Nächste Woche ##
+
+- HA aus Blatt 5.
+
+### TODOs (Studierende) ###
+
+- am ÜB 6 weiter arbeiten.
--- a/protocol/woche15.md
+++ b/protocol/woche15.md
@@ -0,0 +1,23 @@
+# Vorlesungswoche 15 (19.–25. Juli) #
+
+## Agenda ##
+
+- [x] 2–5 min Organisatorisches
+    - [x] Anfragen, ob Vorklausurübung erwünscht wird.
+- [x] Serie 5, Hausaufgaben besprechen
+    - ~~[ ] allgemeines Feedback~~
+    - [x] HA 5.1
+    - [x] HA 5.2
+    - [x] HA 5.3
+    - [x] HA 5.4
+    - [x] HA 5.5
+- ~~[ ] restliche Zeit für allg. Fragen~~
+
+## Nächste Woche ##
+
+- Studierende bringen **eigene Fragen** mit und wir diskutieren diese.
+
+### TODOs (Studierende) ###
+
+- ÜB 6 bis **Do 22.07.** um 22:00 abgeben!
+- Klausurvorbereitung!
--- a/protocol/woche16.md
+++ b/protocol/woche16.md
@@ -0,0 +1,15 @@
+# Woche 16 (26. Juli – 1. Aug) #
+
+Diese Woche wird nicht aufgezeichnet.
+
+## Agenda ##
+
+[x] allgemeine ganzen Stoff betreffende Fragen von Studierenden
+
+## Nächste Woche ##
+
+- Klausur.
+
+### TODOs (Studierende) ###
+
+- Klausurvorbereitung!
--- a/protocol/woche3.md
+++ b/protocol/woche3.md
@@ -1,5 +1,7 @@
 # Vorlesungswoche 3 (26. April – 2. Mai) #

+## Agenda ##
+
 - [x] Organisatorisches (max. 5 min)
    - Erinnerung über Abgabe: Matrikelnr., 1 PDF.
 - [x] Serie 1, Seminaraufgaben
--- a/protocol/woche4.md
+++ b/protocol/woche4.md
@@ -1,4 +1,8 @@
-# Vorlesungswoche 4 (3. April – 9. Mai) #
+# Vorlesungswoche 4 (3. Mai – 9. Mai) #
+
+Handnotizen findet man unter [notes/woche4.pdf](./../notes/woche4.pdf).
+
+## Agenda ##

 - [x] Organisatorisches (max. 5 min)
    - Hochladen = Abgeben
@@ -43,7 +47,6 @@
        -> „gelöst“ durch wohlfundiert/Wohlordnung
        -> R keine Menge

-
 ## Nächste Woche ##

 - Seminaraufgaben für Serie 2:
--- a/protocol/woche5.md
+++ b/protocol/woche5.md
@@ -0,0 +1,24 @@
+# Vorlesungswoche 5 (10.–16. Mai) #
+
+Handnotizen findet man unter [notes/woche5.pdf](./../notes/woche5.pdf).
+
+## Agenda ##
+
+- [x] 2–5 min Organisatorisches (max. 5 min)
+- [x] Serie 2, Seminaraufgaben
+    - [x] 7,5 min SA 2.1 Modelle
+    - [x] 7,5 min SA 2.2 Wahrheitstafel ~> DNF/KNF
+        - DNF nur kurz
+        - KNF
+    - [x] 5 min SA 2.3 Erkennung von Hornfml
+    - [x] 10 min SA 2.4 Markierungsalg
+    - [x] 10 min SA 2.5 Strukturelle Ind
+
+## Nächste Woche ##
+
+- Besprechung HA ÜB 1
+
+### TODOs (Studierende) ###
+
+- Folien zu Wochen 3–5 weiterlesen
+- weiter am ÜB 2 arbeiten
--- a/protocol/woche6.md
+++ b/protocol/woche6.md
@@ -0,0 +1,20 @@
+# Vorlesungswoche 6 (17.–23. Mai) #
+
+## Agenda ##
+
+- [x] 2–5 min Organisatorisches
+- [x] Serie 1, Hausaufgaben besprechen (inkl. Feedbacknotizen von SHK)
+    - [x] HA 1.1
+    - [x] HA 1.2
+    - [x] HA 1.3
+    - [x] HA 1.4
+- [x] restliche Zeit für allg. Fragen
+    - Fragen zu strukturelle Induktion
+
+## Nächste Woche ##
+
+- nach Anfrage kann ggf. etwas aufgezeichnet werden
+
+### TODOs (Studierende) ###
+
+- ÜB 2 bis **Do 20.05.** um 22:00 abgeben!
--- a/protocol/woche7.md
+++ b/protocol/woche7.md
@@ -0,0 +1,3 @@
+# Vorlesungswoche 7 (24.–30. Mai) #
+
+(keine VL od. ÜG diese Woche)
--- a/protocol/woche8.md
+++ b/protocol/woche8.md
@@ -0,0 +1,23 @@
+# Vorlesungswoche 8 (31. Mai – 6. Juni) #
+
+Handnotizen findet man unter [notes/woche8.pdf](./../notes/woche8.pdf).
+
+## Agenda ##
+
+- [x] 2–5 min Organisatorisches
+    - Feedback zu HA 1
+    - Symbolverzeichnis findet man in [notes/glossar.md](./../notes/glossar.md).
+- [x] Serie 3, Seminaraufgaben besprechen
+    - [x] SemA 3.1
+    - [x] SemA 3.2
+    - [x] SemA 3.3
+- [ ] restliche Zeit für allg. Fragen
+
+## Nächste Woche ##
+
+- HA aus Blatt 2.
+
+### TODOs (Studierende) ###
+
+– VL Wochen 5+6 wieder durchlesen, VL Woche 7 für Vorlesung durchlesen.
+- am ÜB 3 weiter arbeiten.
--- a/protocol/woche9.md
+++ b/protocol/woche9.md
@@ -0,0 +1,24 @@
+# Vorlesungswoche 9 (7.–13. Juni) #
+
+## Agenda ##
+
+- [x] 2–5 min Organisatorisches
+- [x] Serie 2, Hausaufgaben besprechen
+    - [x] allgemeines Feedback
+    - [x] SemA 2.1
+    - [x] SemA 2.2
+    - [x] SemA 2.3
+    - [x] SemA 2.4
+    - [x] SemA 2.5
+- [x] restliche Zeit für allg. Fragen
+
+## Nächste Woche ##
+
+- Seminaraufgaben aus Blatt 4.
+- Allg.: bitte überlegen, was vor der Klausur erwünscht wäre, bspw. interaktive Sprechstunden/Fragerunde,
+    oder ob ihr (selbstverständlich Pandemie-Maßnahmen beachtend) unter euch euch treffen wollt,
+    durch den Stoff + die Übungen gemeinsam geht.
+
+### TODOs (Studierende) ###
+
+- ÜB 3 bis **Do 10.06.** um 22:00 abgeben!
Author	SHA1	Message	Date
raj_mathe	60d5231717	master > master: protokoll woche 16	2021-07-28 12:25:29 +02:00
raj_mathe	fa1c091565	master > master: protokoll + READMEs überarbeitet	2021-07-26 16:53:03 +02:00
raj_mathe	fd3229410c	master > master: protokoll woche 15	2021-07-21 13:01:10 +02:00
raj_mathe	f86c908d45	master > master: protokoll woche15	2021-07-21 10:58:07 +02:00
raj_mathe	1b1b781b84	master > master: handnotizen woche14	2021-07-14 13:00:21 +02:00
raj_mathe	2b44a0c54c	master > master: protokoll woche14	2021-07-14 13:00:17 +02:00
raj_mathe	f278500d27	master > master: protocol woche14	2021-07-13 20:06:18 +02:00
raj_mathe	dc6f46777d	master > master: protokoll woche 13	2021-07-07 17:40:51 +02:00
raj_mathe	97a06db946	master > master: protokolle aktualisiert	2021-07-06 15:15:41 +02:00
raj_mathe	7433401bf0	master > master: README.md	2021-07-06 15:15:26 +02:00
raj_mathe	950942d07d	master > master: aufzeichnungslink + kleine Fixes	2021-06-30 16:24:54 +02:00
raj_mathe	405808a47d	master > master: notes woche12	2021-06-30 13:08:35 +02:00
raj_mathe	00c4d85bd9	master > master: protocoll woche12	2021-06-30 13:08:28 +02:00
raj_mathe	07b0931e97	master > master: protocol woche12	2021-06-29 17:06:22 +02:00
raj_mathe	caa24ac777	master > master: protokoll woche11	2021-06-23 15:53:46 +02:00
raj_mathe	f5d978bd7c	master > master: woche11	2021-06-21 11:22:52 +02:00
raj_mathe	9c1941c9d8	master > master: README.md	2021-06-20 18:40:42 +02:00
raj_mathe	2921cc354a	master > master: handnotizen woche10	2021-06-20 18:40:36 +02:00
raj_mathe	466eabeece	master > master: handnotizen woche8	2021-06-20 18:40:32 +02:00
raj_mathe	48529c79e3	master > master: .gitignore	2021-06-20 18:36:16 +02:00
raj_mathe	5f6820fcec	master > master: protokoll	2021-06-20 18:35:52 +02:00
raj_mathe	23a8ba3a49	master > master: Glossar	2021-06-20 18:35:40 +02:00
raj_mathe	7cc2039050	master > master: .gitignore	2021-06-20 18:35:29 +02:00
raj_mathe	3d49ab9b7a	master > master: protokoll woche 6	2021-05-18 11:36:40 +02:00
raj_mathe	f292d7e5dc	master > master: codego - utils + unit tests, A1[0-9]+ mit testen	2021-05-18 11:32:32 +02:00
raj_mathe	2ab9b63a08	master > master: codego - Formulae package	2021-05-18 11:31:29 +02:00
raj_mathe	4be6896a0f	master > master: codego - Grammatik	2021-05-18 11:31:01 +02:00
raj_mathe	c48f703744	master > master: codego - test.sh	2021-05-18 11:30:27 +02:00
raj_mathe	0b9378cea1	master > master: notes - Woche5 (bloß kosmetische Änderungen)	2021-05-15 12:12:46 +02:00
raj_mathe	d877f3905c	master > master: codego - test nicht mehr wegen generics überspringen	2021-05-15 10:59:20 +02:00
raj_mathe	38c4614e3e	master > master: codego - minor fix	2021-05-15 10:58:56 +02:00
raj_mathe	888728d039	master > master: codego - generics schema	2021-05-15 10:58:23 +02:00
raj_mathe	0856bfc0b0	master > master: codego - generics	2021-05-15 10:58:17 +02:00
raj_mathe	b315e666b8	master > master: codego - test.sh (entfernte rm go.sum)	2021-05-15 00:06:01 +02:00
raj_mathe	3b1c190543	master > master: codego - nnf für implies, iff	2021-05-15 00:05:42 +02:00
raj_mathe	6d774a6a4c	master > master: codego - unittests	2021-05-15 00:05:26 +02:00
raj_mathe	79bfcf57bb	master > master: codego - iff	2021-05-15 00:05:03 +02:00
raj_mathe	9b225b0551	master > master: codego - minor cleanup	2021-05-14 19:23:53 +02:00
raj_mathe	39be87d52f	master > master: codego - cleanup	2021-05-14 18:35:06 +02:00
raj_mathe	89c8e63f4b	master > master: codego - aufteilen von methoden in /formulae	2021-05-14 17:41:01 +02:00
raj_mathe	73b7817dcd	master > master: codego - auslagern, erzeugungsmethode verbessert, SyntaxBaum -> Formula	2021-05-14 16:58:27 +02:00
raj_mathe	d490406892	master > master: codego - README.md	2021-05-14 16:57:50 +02:00
raj_mathe	004204c9e9	master > master: codego - .gitignore	2021-05-14 16:57:38 +02:00
raj_mathe	3de689d6fc	master > master: codego - build.sh vereinfacht	2021-05-14 16:57:25 +02:00
raj_mathe	6641946bad	master > master: codego Tippfehler	2021-05-12 22:37:00 +02:00
raj_mathe	2c9b4762a4	master > master: codego panic statt err in utils + unit tests	2021-05-12 22:35:10 +02:00
raj_mathe	a20cfba970	master > master: codego unit tests (actual, expected) Reihenfolge	2021-05-12 18:54:41 +02:00
raj_mathe	45821fc85d	master > master: codego go.sum aktualisiert	2021-05-12 18:47:14 +02:00
raj_mathe	1e37fd2ea9	master > master: codego unit tests aktualisiert	2021-05-12 18:46:51 +02:00
raj_mathe	c10f194ce4	master > master: codego rekursives Aufrufen mit Channels ausgelagert	2021-05-12 18:46:37 +02:00
raj_mathe	8778d31676	master > master: codego main aufgeräumt	2021-05-12 18:45:58 +02:00
raj_mathe	8dcf781b96	master > master: codego Anwendung von Go's "channels" für Rekursion	2021-05-12 18:45:43 +02:00
raj_mathe	5e89d57dad	master > master: codego Aufräumung von SyntaxBaum Methoden	2021-05-12 18:45:18 +02:00
raj_mathe	100701d610	master > master: codego fügte funktionen utils hinzu	2021-05-12 18:44:53 +02:00
raj_mathe	44b0ee41bf	master > master: go package updates	2021-05-12 14:11:04 +02:00
raj_mathe	8e6bd1def7	master > master: codego build script	2021-05-12 14:10:19 +02:00
raj_mathe	7272454835	master > master: Notes Woche 4	2021-05-12 14:04:54 +02:00
raj_mathe	3e8709f90d	master > master: Notes Woche 5	2021-05-12 14:04:49 +02:00
raj_mathe	1bce3a20af	master > master: Protokoll Woche 5	2021-05-12 14:04:39 +02:00
raj_mathe	34422b420b	master > master: protokoll Woche 5	2021-05-12 11:00:05 +02:00
raj_mathe	cbeca60c33	master > master: umbenennung von grammatik	2021-05-10 15:55:00 +02:00
raj_mathe	30ed4667e1	master > master: requirements verschoben	2021-05-10 15:49:24 +02:00
raj_mathe	2dcafc4eb5	master > master: code -> README.md	2021-05-10 15:46:46 +02:00
raj_mathe	61ec2d7df3	master > master: allgemeine Aufräumung	2021-05-10 15:42:42 +02:00
RD	a0dee82659	master > master: notes für Woche4 überarbeitet leichte Korrektur auf Seite 6	2021-05-09 21:01:29 +02:00
raj_mathe	813a984257	master > master: unittests nicht mehr per Default verbose	2021-05-09 20:41:54 +02:00
raj_mathe	cd21b1f035	master > master: codego methoden statt properties verwenden	2021-05-09 20:41:24 +02:00