master > master: protokoll woche 16

leichte Korrektur auf Seite 6

.gitignore

@@ -4,7 +4,10 @@
 
 !/docs
 !/notes
+!/notes/*.pdf
+!/notes/*.md
 !/protocol
 !/protocol/*.md
 
 !/code
+!/codego

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.

code/.gitignore

@@ -1,12 +1,21 @@
 *
 !/.gitignore
 
-!/README.md
-!/run.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

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 run.sh test.sh
+    chmod +x scripts/*.sh
-    ## oder
-    chmod +x *.sh
     ```
-- In `run.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
-./run.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.

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

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.syntaxbaum import SyntaxBaum;
-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;
 
 # ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 # 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):
+    # Fall ¬F
-        name = fml.expr;
+    elif fml.isNegation():
-        return 1 if (name in I) else 0;
+        val0 = rekursivEval(subfml[0], I);
-    elif isTrueSymbol(fml):
-        return 1;
-    elif isFalseSymbol(fml):
-        return 0;
-    elif isNegation(fml):
-        val0 = rekursiv_eval(subfml[0], I);
         return 1 - val0;
-    elif isConjunction(fml):
+    # Fall F1 ⋀ F2
-        val0 = rekursiv_eval(subfml[0], I);
+    elif fml.isConjunction2():
-        val1 = rekursiv_eval(subfml[1], I);
+        val0 = rekursivEval(subfml[0], I);
+        val1 = rekursivEval(subfml[1], I);
         return min(val0, val1);
-    elif isLongConjunction(fml):
+    # Fall F1 ⋁ F2
-        values = [rekursiv_eval(t, I) for t in subfml];
+    elif fml.isDisjunction2():
-        return min(values);
+        val0 = rekursivEval(subfml[0], I);
-    elif isDisjunction(fml):
+        val1 = rekursivEval(subfml[1], I);
-        val0 = rekursiv_eval(subfml[0], I);
-        val1 = rekursiv_eval(subfml[1], I);
         return max(val0, val1);
-    elif isLongDisjunction(fml):
+    ########
-        values = [rekursiv_eval(t, I) for t in subfml];
+    # WEITERE FÄLLE NICHT IN VORLESUNG
-        return max(values);
+    ########
-    elif isImplication(fml):
+    # Sonderfall: generische Formel als Variable
-        val0 = rekursiv_eval(subfml[0], I);
+    if fml.isGeneric():
-        val1 = rekursiv_eval(subfml[1], I);
+        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

code/aussagenlogik/schema.py

@@ -6,12 +6,7 @@
 # ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 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 lark import Tree;
-from typing import List;
-from typing import Union;
 
 from aussagenlogik.syntaxbaum import SyntaxBaum;
 
@@ -19,10 +14,10 @@ from aussagenlogik.syntaxbaum import SyntaxBaum;
 # GLOBALE KONSTANTEN
 # ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-## lexer
+# lexer durch LARK erzeugen
-with open('aussagenlogik/grammar.lark', 'r') as fp:
+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
@@ -30,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 == ['disj', 'disj_lang'];
-
-def isImplication(fml: SyntaxBaum) -> bool:
-    return fml.kind == 'impl';

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.children = [];
-            self.expr = fml.children[0];
+        self.valence = 0;
-            self.children = [];
+        expr_parts = []
-            self.tree = Tree(self.kind, fml.children);
+        for child in fml.children:
-        else:
+            if isinstance(child, str):
-            self.children = [ SyntaxBaum(child) for child in fml.children if isinstance(child, Tree) and child.data != 'symb' ];
+                expr_parts.append(child);
-            self.tree = Tree(self.kind, [child.tree for child in self.children]);
+            ## subfml is instance larkTree:
-            signature_parts = [];
+            elif child.data == 'symb':
-            i = 0;
+                symb = str(child.children[0]);
-            for subfml in fml.children:
+                expr_parts.append(symb);
-                if isinstance(subfml, str):
+            else:
-                    signature_parts.append(subfml);
+                subtree = SyntaxBaum(child);
-                elif subfml.data == 'symb':
+                self.children.append(subtree);
-                    symb = str(subfml.children[0]);
+                self.valence += 1;
-                    signature_parts.append(symb);
+                expr_parts.append(subtree.expr);
-                else:
+        self.expr = ' '.join(expr_parts);
-                    signature_parts.append('{{{}}}'.format(i));
+        if self.valence > 1:
-                    i += 1;
+            self.expr = '(' + self.expr + ')';
-            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;
         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';

code/data.env

@@ -1,9 +1,9 @@
-# expr = "A0"
+# expr = 'A0'
-# expr = "! A0"
+# expr = '! A0'
-# expr = "( A0 && A1 )"
+# expr = '( A0 && A1 )'
-# expr = "( A0 || A1 )"
+# expr = '( A0 || A1 )'
-# expr = "( A0 -> A1 )"
+# expr = '( A0 -> A1 )'
-expr = "( A0 -> ((A0 && A3 && A4) || ! A2) )"
+expr = '( A0 -> ((A0 && A3 && A4) || ! A2) )'
-# expr = "( A0 -> ((A0 && A3) || A2) )"
+# expr = '( A0 -> ((A0 && A3) || A2) )'
-# expr = "(( {G} || !{G} ) -> A5)"
+# expr = '(( {G} || !{G} ) -> A5)'
-interpretation = "[ 'A0', 'A2' ]"
+interpretation = '[ "A0", "A2" ]'

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**.

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

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 rekursivEval;
-from aussagenlogik.rekursion import rekursiv_atoms;
+from aussagenlogik.rekursion import rekursivAtoms;
-from aussagenlogik.rekursion import rekursiv_depth;
+from aussagenlogik.rekursion import rekursivDepth;
-from aussagenlogik.rekursion import rekursiv_length;
+from aussagenlogik.rekursion import rekursivLength;
-from aussagenlogik.rekursion import rekursiv_parentheses;
+from aussagenlogik.rekursion import rekursivParentheses;
 
 # ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 # GLOBALE KONSTANTEN
@@ -37,20 +37,19 @@ 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),
+        eval         = rekursivEval(tree, I),
-        atoms = rekursiv_atoms(fml),
+        atoms        = rekursivAtoms(tree),
-        d     = rekursiv_depth(fml),
+        depth        = rekursivDepth(tree),
-        l     = rekursiv_length(fml),
+        length       = rekursivLength(tree),
-        p     = rekursiv_parentheses(fml),
+        nParentheses = rekursivParentheses(tree),
     );
     ## Resultate anzeigen:
-    display_results(expr, fml, I, results);
+    display_results(tree, I, results);
     return;
 
-
 # ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 # SONSTIGE METHODEN
 # ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -61,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:
+        F := \033[92;1m{expr}\033[0m:
-        '''.format(F=fml)
+        '''.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[2mdepth(F)        = \033[94;1m{depth}\033[0m; \033[91;1m<- *\033[0m
-        \033[2mlength(F)       = \033[94;1m{l}\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{p}\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

code/scripts/build.sh

@@ -1,7 +1,7 @@
 #!/usr/bin/env bash
 
 ################################################################################################
-# NOTE: `chmod +x run.sh` vorher ausführen, um dieses Skript benutzen zu können.
+# NOTE: `chmod +x build.sh` vorher ausführen, um dieses Skript benutzen zu können.
 ################################################################################################
 
 ################################
@@ -12,8 +12,8 @@ function call_python() {
     [ "$OSTYPE" == "msys" ] && py -3 $@ || python3 $@;
 }
 
-function run_check_requirements() {
+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() {
@@ -25,7 +25,7 @@ function run_code() {
 ################################
 
 # Kann auskommentiert werden, wenn nötige Module schon installiert:
-run_check_requirements;
+check_requirements;
 
 # Code ausführen:
-run_code
+run_code;

code/scripts/test.sh

@@ -12,13 +12,13 @@ function call_python() {
     [ "$OSTYPE" == "msys" ] && py -3 $@ || python3 $@;
 }
 
-function run_check_requirements() {
+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;
@@ -32,7 +32,7 @@ function run_unittests(){
 ################################
 
 # Kann auskommentiert werden, wenn nötige Module schon installiert:
-run_check_requirements;
+check_requirements;
 
 # Code testen (unittests):
 run_unittests;

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 rekursivEval;
-from aussagenlogik.rekursion import rekursiv_depth;
+from aussagenlogik.rekursion import rekursivAtoms;
-from aussagenlogik.rekursion import rekursiv_length;
+from aussagenlogik.rekursion import rekursivDepth;
-from aussagenlogik.rekursion import rekursiv_parentheses;
+from aussagenlogik.rekursion import rekursivLength;
-from aussagenlogik.rekursion import rekursiv_eval;
+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;

codego/.gitignore

@@ -0,0 +1,29 @@
+*
+!/.gitignore
+
+!/data.env
+!/README.md
+
+## 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/recursion
+!/aussagenlogik/schema
+!/aussagenlogik/formulae
+!/core
+!/core/environment
+!/core/utils
+!/**/*.go
+!/go.mod
+!/go.sum

codego/README.md

@@ -0,0 +1,96 @@
+# Code in golang #
+
+Die Inhalte dieses Ordners sind absolut **kein Pflichtbestandteil** des Kurses.
+
+Diese dienen nur zur Demonstration / konkreten Verwirklichung von Verfahren, die im Kurs auftauchen. Für Wissbegierige mit auch grundlegenden Programmierkenntnissen bietet sich dies als Möglichkeit an, um sich selbst zu überzeugen, dass strukturelle Rekursion funktioniert.
+
+Der Gebrauch dieser Skripte unterliegt der Eigenverantwortung von Studierenden.
+
+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)
+- 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.
+
+## Voreinstellungen ##
+
+- In einer bash-console zu diesem Ordner navigieren und folgenden Befehl ausführen:
+    ```bash
+    chmod +x scripts/*.sh
+    ```
+- 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.
+
+## Daten ##
+
+In `data.env` kann man Daten (aktuell: auszuwertenden Ausdruck + Interpretation/Modell) eintragen. Man beachte dabei die Syntax.
+
+## Gebrauchshinweise ##
+
+In einer bash-console zu diesem Ordner navigieren und
+```bash
+source scripts/build.sh
+## oder
+go build main.go && ./main
+```
+ausführen.
+
+Das bash Skript macht folgende Schritte
+
+```bash
+# installiert go-module (kann nach 1. Mal rauskommentiert werden):
+check_requirements;
+# lädt ggf. antlr.jar herunter (wenn fehlt), mit dem die Grammatiken erzeugt werden (kann nach 1. Mal rauskommentiert werden):
+precompile_grammars;
+# kompiliert Go-Projekt (nach jeder Code-Änderung erneut nötig), sonst rauskommentieren:
+compile_programme;
+# führt kompiliertes Programm auf Daten in data.env aus:
+run_programme;
+```
+
+## Offene Challenges ##
+
+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 ###
+
+Probiere es mit Stift-und-Zettel und anhand von Beispielen die Werte händisch zu berechnen. Vergleiche dies mit den durch den Code rekursiv berechneten Werten. Stimmt alles überein?
+
+### 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`.
+
+- In der Console (wenn noch nicht geschehen) folgenden Befehl einmalig ausführen:
+    ```bash
+    chmod +x scripts/test.sh
+    ```
+- 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.
+
+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.

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)
+}

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" }

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},
+	}
+}

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
+}

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()
+	}
+}

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())
+}

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)
+}

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)
+}

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)
+}

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
+}

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())
+}

codego/aussagenlogik/schema/schema.go

@@ -0,0 +1,167 @@
+package schema
+
+import (
+	"logik/aussagenlogik/formulae"
+	parser "logik/grammars/aussagenlogik"
+	"regexp"
+
+	"github.com/antlr/antlr4/runtime/Go/antlr"
+)
+
+/* ---------------------------------------------------------------- *
+ * EXPORTS
+ * ---------------------------------------------------------------- */
+
+func ParseExpr(u string) formulae.Formula {
+	var lexer = createLexer(u)
+	var tokenStream = lexerToTokenStream(lexer)
+	var prs = parser.NewaussagenlogikParser(tokenStream)
+	var t = prs.Start()
+	tree := createFormula(t, prs)
+	return tree
+}
+
+/* ---------------------------------------------------------------- *
+ * PRIVATE
+ * ---------------------------------------------------------------- */
+
+func exprToStream(u string) *antlr.InputStream {
+	return antlr.NewInputStream(u)
+}
+
+func lexerToTokenStream(lexer antlr.Lexer) antlr.TokenStream {
+	return antlr.NewCommonTokenStream(lexer, antlr.TokenDefaultChannel)
+}
+
+func createLexer(u string) antlr.Lexer {
+	stream := exprToStream(u)
+	return parser.NewaussagenlogikLexer(stream)
+}
+
+func createFormula(tree antlr.Tree, parser antlr.Parser) formulae.Formula {
+	var ant = antlrTree{tree: tree, parser: &parser}
+	return ant.toFormula()
+}
+
+/* ---------------------------------------------------------------- *
+ * Struct: antlrTree + Methods
+ * ---------------------------------------------------------------- */
+
+type antlrTree struct {
+	tree   antlr.Tree
+	parser *antlr.Parser
+}
+
+func (ant antlrTree) getChildren() []antlrTree {
+	var nodes = ant.tree.GetChildren()
+	var subants = make([]antlrTree, len(nodes))
+	for i, node := range nodes {
+		subants[i] = antlrTree{tree: node, parser: ant.parser}
+	}
+	return subants
+}
+
+func (ant antlrTree) getLabel() string {
+	return antlr.TreesGetNodeText(ant.tree, []string{}, *ant.parser)
+}
+
+func (ant antlrTree) getTextContent() string {
+	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) toFormula() formulae.Formula {
+	var label string = ant.getLabel()
+	var subants = ant.getChildren()
+	var nChildren = len(subants)
+
+	switch label {
+	case "start":
+		if nChildren == 1 {
+			return subants[0].toFormula()
+		}
+	case "open":
+		if nChildren == 1 {
+			return subants[0].toFormula()
+		}
+	case "closed":
+		switch nChildren {
+		case 1:
+			return subants[0].toFormula()
+		// expr = ( expr )
+		case 3:
+			return subants[1].toFormula()
+		}
+	case "atomic":
+		if nChildren == 1 {
+			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":
+		// NOTE: expr = ! expr
+		if nChildren == 2 {
+			return formulae.Negation(subants[1].toFormula())
+		}
+	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 subtrees = make([]formulae.Formula, n)
+			var isSymb bool = true
+			var i int = 0
+			for _, subant := range subants {
+				if isSymb {
+					subtrees[i] = subant.toFormula()
+					i++
+				}
+				// NOTE: infix notation: alternatives between expression and symbol
+				isSymb = !isSymb
+			}
+			switch label {
+			case "and":
+				return formulae.Conjunction(subtrees)
+			case "or":
+				return formulae.Disjunction(subtrees)
+			}
+		}
+	}
+
+	panic("Could not parse expression")
+}

codego/aussagenlogik/schema/schema_test.go

@@ -0,0 +1,47 @@
+package schema_test
+
+/* ---------------------------------------------------------------- *
+ * UNIT TESTING
+ * ---------------------------------------------------------------- */
+
+import (
+	"logik/aussagenlogik/formulae"
+	"logik/aussagenlogik/schema"
+	"testing"
+
+	"github.com/stretchr/testify/assert"
+)
+
+/* ---------------------------------------------------------------- *
+ * TESTCASE ParseExpr
+ * ---------------------------------------------------------------- */
+
+func TestParseExpr(test *testing.T) {
+	var assert = assert.New(test)
+	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()))
+}

codego/core/environment/environment.go

@@ -0,0 +1,71 @@
+package environment
+
+import (
+	"errors"
+	"fmt"
+	"log"
+	"os"
+
+	"github.com/joho/godotenv"
+)
+
+var ENV_FILE_NAME string
+
+/* ---------------------------------------------------------------- *
+ * EXPORTS
+ * ---------------------------------------------------------------- */
+
+func ReadEnvKey(key string, optional ...string) string {
+	value, err := readEnvKey(key, optional...)
+	if err != nil {
+		log.Fatal(err)
+	}
+	return value
+}
+
+func ReadEnvKeyAllowMissing(key string, optional ...string) string {
+	value, _ := readEnvKey(key, optional...)
+	return value
+}
+
+func ReadEnvKeyDefault(key string, valueDefault string, optional ...string) string {
+	value, _ := readEnvKey(key, optional...)
+	if value == "" {
+		return valueDefault
+	}
+	return value
+}
+
+/* ---------------------------------------------------------------- *
+ * PRIVATE
+ * ---------------------------------------------------------------- */
+
+func loadEnvFile(path string) error {
+	if path == "" {
+		log.Fatal("Path name to environment file is not allowed to be empty!")
+	}
+	return godotenv.Load(path)
+}
+
+func getEnvKey(key string) string {
+	return os.Getenv(key)
+}
+
+func readEnvKey(key string, optional ...string) (string, error) {
+	var path string = ENV_FILE_NAME
+	var err error
+	var value string
+	if len(optional) > 0 {
+		path = optional[0]
+	}
+	err = loadEnvFile(path)
+	if err != nil {
+		log.Fatalf("Could not read environment file, \033[1m%s\033[0m!\n", path)
+	}
+	err = nil
+	value = getEnvKey(key)
+	if value == "" {
+		err = errors.New(fmt.Sprintf("Environment key \033[1m%s\033[0m missing or empty in environment file \033[1m%s\033[0m!", key, path))
+	}
+	return value, err
+}

codego/core/utils/utils.go

@@ -0,0 +1,175 @@
+package utils
+
+import (
+	"encoding/json"
+	"sort"
+	"strings"
+)
+
+/* ---------------------------------------------------------------- *
+ * METHODS: json
+ * ---------------------------------------------------------------- */
+
+func JsonToArrayOfStrings(s string, value *[]string) {
+	var err error
+	err = json.Unmarshal([]byte(s), &value)
+	if err != nil {
+		panic(err)
+	}
+}
+
+/* ---------------------------------------------------------------- *
+ * 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
+	}
+	return y
+}
+
+func Max2(x int, y int) int {
+	if x >= y {
+		return x
+	}
+	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])
+		v := strings.ToLower((*list)[j])
+		cmp := strings.Compare(u, v)
+		return (cmp < 0)
+	})
+}
+
+func FilterStrings(list *[]string, f func(string) bool) []string {
+	var listFiltered = []string{}
+	for _, val := range *list {
+		if f(val) {
+			listFiltered = append(listFiltered, val)
+		}
+	}
+	return listFiltered
+}
+
+func UnionStrings2(list1 []string, list2 []string) []string {
+	var mark = make(map[string]bool)
+	for _, item := range list1 {
+		mark[item] = true
+	}
+	for _, item := range list2 {
+		mark[item] = true
+	}
+	var list = make([]string, len(mark))
+	var i int = 0
+	for item, _ := range mark {
+		list[i] = item
+		i++
+	}
+	return list
+}
+
+// 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
+	}
+	for _, item := range *listTo {
+		mark[item] = false // signals suppression of duplicate addition
+	}
+	for item, isNew := range mark {
+		if isNew {
+			*listTo = append(*listTo, item)
+		}
+	}
+}
+
+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
+}

codego/core/utils/utils_test.go

@@ -0,0 +1,119 @@
+package utils_test
+
+/* ---------------------------------------------------------------- *
+ * UNIT TESTING
+ * ---------------------------------------------------------------- */
+
+import (
+	"logik/core/utils"
+	"strings"
+	"testing"
+
+	"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
+ * ---------------------------------------------------------------- */
+
+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([]string{"baby", "Hund", "katze", "Mond", "Pluto", "Saturn"}, list)
+}
+
+/* ---------------------------------------------------------------- *
+ * TESTCASE SortStrings
+ * ---------------------------------------------------------------- */
+
+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.ElementsMatch([]string{"aaron", "aardvark", "aarhus", "aal"}, list2)
+}
+
+/* ---------------------------------------------------------------- *
+ * TESTCASE UnionStrings2, UnionStringsInPlace, UnionStringsList
+ * ---------------------------------------------------------------- */
+
+func TestUnionStrings2(test *testing.T) {
+	var assert = assert.New(test)
+	var list1 = []string{"red", "blue", "blue", "green", "blue", "grey", "black", "green"}
+	var list2 = []string{"yellow", "orange", "lila", "red"}
+	var list = utils.UnionStrings2(list1, list2)
+	assert.ElementsMatch([]string{"black", "blue", "green", "grey", "lila", "orange", "red", "yellow"}, list)
+}
+
+func TestUnionStringsInPlace(test *testing.T) {
+	var assert = assert.New(test)
+	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)
+}

codego/data.env

@@ -0,0 +1,12 @@
+# expr = 'A0'
+# expr = '! A0'
+# expr = 'A9341'
+# expr = '!!! A84'
+# expr = '( A0 || A1 )'
+# expr = '( A0 -> A1 )'
+# expr = '( A0 && ! (0 || A8 || 1) ) -> A5'
+expr = '( A0 -> ((A0 && A3 && A4) || ! A2) )'
+# expr = '( A0 -> ((A0 && A3 && A4) || A2) )'
+# expr = '( A0 -> ((A0 && A3) || A2) )'
+# expr = '(( {G} || !{G} ) -> A5)'
+interpretation = [ "A0", "A2" ]

codego/go.mod

@@ -0,0 +1,14 @@
+module logik
+
+go 1.16
+
+require (
+	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/crypto v0.0.0-20200622213623-75b288015ac9 // indirect
+	golang.org/x/tools v0.1.1
+)

codego/go.sum

@@ -0,0 +1,42 @@
+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=
+github.com/joho/godotenv v1.3.0/go.mod h1:7hK45KPybAkOC6peb+G5yklZfMxEjkZhHbwpqxOKXbg=
+github.com/lithammer/dedent v1.1.0 h1:VNzHMVCBNG1j0fh3OrsFRkVUwStdDArbgBWoPAffktY=
+github.com/lithammer/dedent v1.1.0/go.mod h1:jrXYCQtgg0nJiN+StA2KgR7w6CiQNv9Fd/Z9BP0jIOc=
+github.com/pmezard/go-difflib v1.0.0 h1:4DBwDE0NGyQoBHbLQYPwSUPoCMWR5BEzIk/f1lZbAQM=
+github.com/pmezard/go-difflib v1.0.0/go.mod h1:iKH77koFhYxTK1pcRnkKkqfTogsbg7gZNVY4sRDYZ/4=
+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.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.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-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-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-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.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=
+gopkg.in/check.v1 v0.0.0-20161208181325-20d25e280405/go.mod h1:Co6ibVJAznAaIkqp8huTwlJQCZ016jof/cbN4VW5Yz0=
+gopkg.in/yaml.v3 v3.0.0-20200313102051-9f266ea9e77c h1:dUUwHk2QECo/6vqA44rthZ8ie2QXMNeKRTHCNY2nXvo=
+gopkg.in/yaml.v3 v3.0.0-20200313102051-9f266ea9e77c/go.mod h1:K4uyk7z7BCEPqu6E+C64Yfv1cQ7kz7rIZviUmN+EgEM=

codego/grammars/README.md

@@ -0,0 +1,5 @@
+# ANTLR4 #
+
+Gebrauchsanleitung <https://blog.gopheracademy.com/advent-2017/parsing-with-antlr4-and-go>
+
+_Hinweis:_ In dieser Repo wurden die in der o.s. Webseite erwähnten Schritte bereits in den bash Skripten berücksichtigt.

codego/grammars/aussagenlogik.g4

@@ -0,0 +1,47 @@
+grammar aussagenlogik;
+
+// Standardtokens:
+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_IFF:  ([<][-]+[>]|[<][=]+[>]|'iff');
+SYMB_IMPL: (~[<][-]+[>]|~[<][=]+[>]);
+
+// Rules
+start: open <EOF> | closed <EOF>;
+
+closed: atomic | not | LBRACE open RBRACE;
+open: and2 | and | or2 | or | implies | iff;
+
+// Schemata für atomische Ausdrücke
+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;
+// Schemata für Konjunktion: F1 ⋀ F2 bzw. F1 ⋀ F2 ⋀ ... ⋀ Fn
+and2:      closed   symb=SYMB_AND  closed;
+and:     ( closed ( symb=SYMB_AND  closed )+ );
+// Schemata für Disjunktion: F1 ⋁ F2 bzw. F1 ⋁ F2 ⋁ ... ⋁ Fn
+or2:       closed   symb=SYMB_OR   closed;
+or:      ( closed ( symb=SYMB_OR   closed )+ );
+// Schema für Implikation: F1 ⟶ F2
+implies:   closed   symb=SYMB_IMPL closed;
+// Schema für Implikation: F1 ⟷ F2
+iff:       closed   symb=SYMB_IFF  closed;

codego/main.go

@@ -0,0 +1,95 @@
+package main
+
+import (
+	"fmt"
+	"logik/aussagenlogik/formulae"
+	"logik/aussagenlogik/recursion"
+	"logik/aussagenlogik/schema"
+	env "logik/core/environment"
+	"logik/core/utils"
+	"strings"
+
+	"github.com/lithammer/dedent"
+)
+
+var DATA_ENV string = "data.env"
+
+type dataType struct {
+	expr           string
+	interpretation []string
+}
+
+type resultsType struct {
+	eval         int
+	nnf          formulae.Formula
+	atoms        []string
+	depth        int
+	length       int
+	nParentheses int
+}
+
+var data dataType
+
+func main() {
+	// Extrahiere Daten
+	getData()
+	// Ausdruck -> Syntaxbaum
+	tree := schema.ParseExpr(data.expr)
+	results := getResults(tree)
+	// Resultate anzeigen:
+	displayResults(tree, results)
+}
+
+// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+// SONSTIGE METHODEN
+// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+func getData() {
+	env.ENV_FILE_NAME = DATA_ENV
+	data.expr = env.ReadEnvKey("expr")
+	s := env.ReadEnvKey("interpretation")
+	utils.JsonToArrayOfStrings(s, &data.interpretation)
+}
+
+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
+		F := %[1]s:
+
+		%[2]s
+
+		Für I = {%[3]s} und F wie oben gilt
+		eval(F, I)      = %[4]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.GetExpr(),
+		tree.Pretty("    "),
+		strings.Join(data.interpretation, ", "),
+		results.eval,
+		results.nnf.GetExpr(),
+		// string(results.atoms),
+		strings.Join(results.atoms, ", "),
+		results.depth,
+		results.length,
+		results.nParentheses,
+	))
+}

codego/scripts/build.sh

@@ -0,0 +1,71 @@
+#!/usr/bin/env bash
+
+################################################################################################
+# NOTE: `chmod +x build.sh` vorher ausführen, um dieses Skript benutzen zu können.
+################################################################################################
+
+################################
+# HILFSMETHODEN
+################################
+
+export NULL="/dev/null"
+export ANTLR_VESION="4.7";
+
+function call_go() {
+    go $@;
+}
+
+function check_requirements() {
+    call_go get "$( cat scripts/requirements )";
+}
+
+function get_antlr() {
+    local url="http://www.antlr.org/download/antlr-${ANTLR_VESION}-complete.jar";
+    ( wget $url ) >> $NULL 2> $NULL || (echo -e "[\033[91;1mERROR\033[0m] konnte \033[1;2mwget $url\033[0m nicht ausführen." && exit 1);
+    while read fname; do
+        if ! [ "$fname" == "" ] && [ -f "$fname" ]; then
+            echo -e "\033[92;1mANTLR\033[1m-${ANTLR_VESION}\033[0m wurde heruntergeladen und in \033[1mcodego/grammars\033[0m kopiert.";
+            mv "$fname" "grammars/antlr.jar";
+            break;
+        fi
+    done <<< "$( ls antlr*.jar )"
+}
+
+function precompile_grammars() {
+    local fname;
+    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" )";
+            echo -e "\033[92;1mANTLR\033[0m präkompiliert Grammatik \033[1m${fname}\033[0m";
+            java -jar antlr.jar -Dlanguage=Go "$fname" -o "$name";
+        done <<< "$( ls *.g4 2> $NULL )"
+    popd >> $NULL;
+}
+
+function compile_programme() {
+    [ -f "dist/main" ] && rm "dist/main";
+    echo -e "\033[92;1mGO\033[0m kompiliert \033[1mmain.go\033[0m";
+    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";
+    ./dist/main;
+}
+
+################################
+# HAUPTVORGÄNGE
+################################
+
+# Kann auskommentiert werden, wenn nötige Module schon installiert:
+check_requirements;
+
+# Code als Programm kompilieren und ausführen:
+precompile_grammars;
+compile_programme;
+run_programme;

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

codego/scripts/test.sh

@@ -0,0 +1,37 @@
+#!/usr/bin/env bash
+
+################################################################################################
+# NOTE: `chmod +x test.sh` vorher ausführen, um dieses Skript benutzen zu können.
+################################################################################################
+
+################################
+# HILFSMETHODEN
+################################
+
+export TEST_VERBOSE=false # <- true: unittest mit verbose output
+export TEST_TIMEOUT="10s"
+
+function call_go() {
+    go $@;
+}
+
+function check_requirements() {
+    call_go get "$( cat scripts/requirements )";
+}
+
+function run_unittests(){
+    echo -e "\033[1mUNITTESTS\033[0m\n";
+    local verbose_opt="";
+    ( $TEST_VERBOSE ) && verbose_opt="-v"
+    call_go test $verbose_opt -timeout $TEST_TIMEOUT -count 1 -run "^Test[A-Z].*" "logik" "./...";
+}
+
+################################
+# HAUPTVORGÄNGE
+################################
+
+# Kann auskommentiert werden, wenn nötige Module schon installiert:
+check_requirements;
+
+# Code testen (unittests):
+run_unittests;

notes/.gitignore

@@ -1,4 +0,0 @@
-*
-!/.gitignore
-
-!/*.pdf

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.

protocol/README.md

@@ -2,9 +2,30 @@
 
 Inhaltsverzeichnis
 
-- [Vorlesungswoche 1](./woche1.md)
+- [Vorlesungswoche 1](./woche1.md) (_keine Übung_)
-- [Vorlesungswoche 2](./woche2.md) Erste Übung: Organisatorisches
+- [Vorlesungswoche 2](./woche2.md) Erste Übung: Organisatorisches.
-- [Vorlesungswoche 3](./woche3.md) Seminaraufgaben aus Blatt 1
+- [Vorlesungswoche 3](./woche3.md) Semaufg Blatt 1; [BBB Aufzeichnung](https://t1p.de/tjiu).
-- [Vorlesungswoche 4](./woche4.md) ~~Hausaufgaben aus Blatt ??~~ Spezielle Themen
+- [Vorlesungswoche 4](./woche4.md) Spezielle Themen; [Zoom Aufzeichnung](https://t1p.de/91vz).
-- [Vorlesungswoche 5](./woche5.md) Seminaraufgaben aus Blatt 2
+- [Vorlesungswoche 5](./woche5.md) Semaufg Blatt 2; [Zoom Aufzeichnung](https://t1p.de/ny7n).
-- [Vorlesungswoche 6](./woche6.md) Hausaufgaben aus Blatt 1
+- [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!

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.

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!

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.

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!

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.

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!

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!

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

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:

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

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!

protocol/woche7.md

@@ -0,0 +1,3 @@
+# Vorlesungswoche 7 (24.–30. Mai) #
+
+(keine VL od. ÜG diese Woche)

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.

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!