diff --git a/codego/aussagenlogik/formulae/formulae.go b/codego/aussagenlogik/formulae/formulae.go
new file mode 100644
index 0000000..e4a9f2e
--- /dev/null
+++ b/codego/aussagenlogik/formulae/formulae.go
@@ -0,0 +1,283 @@
+package formulae
+
+import (
+	"fmt"
+	"strings"
+)
+
+/* ---------------------------------------------------------------- *
+ * TYPE Formula
+ * ---------------------------------------------------------------- */
+
+type Formula struct {
+	kind        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) SetSubformulae(children [](*Formula)) {
+	fml.subformulae = children
+	fml.valence = len(children)
+}
+
+func (fml Formula) GetSubFormulae() []Formula {
+	var n int = fml.valence
+	var children = make([]Formula, n)
+	for i, subfml := range fml.subformulae {
+		children[i] = *subfml
+	}
+	return children
+}
+
+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
+	}
+}
+
+func (fml Formula) Deepcopy() Formula {
+	var children = make([](*Formula), len(fml.subformulae))
+	for i, child := range fml.subformulae {
+		childCopy := child.Deepcopy()
+		children[i] = &childCopy
+	}
+	return Formula{
+		expr:        fml.expr,
+		kind:        fml.kind,
+		valence:     fml.valence,
+		subformulae: children,
+	}
+}
+
+/* ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *
+ * METHODS: Basic constructions
+ * ---------------------------------------------------------------- */
+
+var Tautology = Formula{
+	kind:        "taut",
+	expr:        "1",
+	valence:     0,
+	subformulae: [](*Formula){},
+}
+
+var Contradiction = Formula{
+	kind:        "contradiction",
+	expr:        "0",
+	valence:     0,
+	subformulae: [](*Formula){},
+}
+
+func Atom(expr string) Formula {
+	return Formula{
+		kind:        "atom",
+		expr:        expr,
+		valence:     0,
+		subformulae: [](*Formula){},
+	}
+}
+
+func NegatedAtom(expr string) Formula {
+	return Negation(Atom(expr))
+}
+
+func Generic(expr string) Formula {
+	return Formula{
+		kind:        "generic",
+		expr:        expr,
+		valence:     0,
+		subformulae: [](*Formula){},
+	}
+}
+
+func Negation(fml Formula) Formula {
+	return Formula{
+		kind:        "not",
+		expr:        "!" + " " + fml.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 {
+	var expr string = ""
+	var children = make([](*Formula), len(fmls))
+	for i, fml := range fmls {
+		if i > 0 {
+			expr += " && "
+		}
+		expr += fml.expr
+		children[i] = &fml
+	}
+	return Formula{
+		kind:        "and",
+		expr:        "(" + expr + ")",
+		valence:     len(children),
+		subformulae: children,
+	}
+}
+
+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 {
+	var expr string = ""
+	var children = make([](*Formula), len(fmls))
+	for i, fml := range fmls {
+		if i > 0 {
+			expr += " || "
+		}
+		expr += fml.expr
+		children[i] = &fml
+	}
+	return Formula{
+		kind:        "or",
+		expr:        "(" + expr + ")",
+		valence:     len(children),
+		subformulae: children,
+	}
+}
+
+func Implies(fml1 Formula, fml2 Formula) Formula {
+	return Formula{
+		kind:        "implies",
+		expr:        "(" + fml1.expr + " -> " + fml2.expr + ")",
+		valence:     2,
+		subformulae: [](*Formula){&fml1, &fml2},
+	}
+}
+
+/* ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *
+ * 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"
+}
diff --git a/codego/aussagenlogik/formulae/formulae_generate.go b/codego/aussagenlogik/formulae/formulae_generate.go
new file mode 100644
index 0000000..63183c1
--- /dev/null
+++ b/codego/aussagenlogik/formulae/formulae_generate.go
@@ -0,0 +1,165 @@
+package formulae
+
+// NOTE: GoLang hat noch keine generics. Erst 2022.
+
+/* ---------------------------------------------------------------- *
+ * Generate int-value FN from scheme
+ * ---------------------------------------------------------------- */
+
+func CreateFromSchemeIntValued(scheme func(fml Formula, prevValues []int) int) func(fml Formula) int {
+	var fn func(fml Formula) int
+	var subFn = func(ch chan int, subfml Formula) { ch <- fn(subfml) }
+	fn = func(fml Formula) int {
+		var subfmls = fml.GetSubFormulae()
+		var n = len(subfmls)
+		var subChan = make([](chan int), n)
+		var prevValues = make([]int, len(subfmls))
+		// start parallel computations on subformulas
+		for i, subfml := range subfmls {
+			subChan[i] = make(chan int) // create Channel, since currently nil
+			go subFn(subChan[i], subfml)
+		}
+		// successively read values
+		for i := 0; i < n; i++ {
+			prevValues[i] = <-subChan[i]
+		}
+		// apply schema to get value for formula
+		return scheme(fml, prevValues)
+	}
+	return fn
+}
+
+/* ---------------------------------------------------------------- *
+ * Generate string-value FN from scheme
+ * ---------------------------------------------------------------- */
+
+func CreateFromSchemeStringValued(scheme func(fml Formula, prevValues []string) string) func(fml Formula) string {
+	var fn func(fml Formula) string
+	var subFn = func(ch chan string, subfml Formula) { ch <- fn(subfml) }
+	fn = func(fml Formula) string {
+		var subfmls = fml.GetSubFormulae()
+		var n = len(subfmls)
+		var subChan = make([](chan string), n)
+		var prevValues = make([]string, len(subfmls))
+		// start parallel computations on subformulas
+		for i, subfml := range subfmls {
+			subChan[i] = make(chan string) // create Channel, since currently nil
+			go subFn(subChan[i], subfml)
+		}
+		// successively read values
+		for i := 0; i < n; i++ {
+			prevValues[i] = <-subChan[i]
+		}
+		// apply schema to get value for formula
+		return scheme(fml, prevValues)
+	}
+	return fn
+}
+
+/* ---------------------------------------------------------------- *
+ * Generate *[]string-value Fn from scheme
+ * ---------------------------------------------------------------- */
+
+func CreateFromSchemeStringsValued(scheme func(fml Formula, prevValues [][]string) []string) func(fml Formula) []string {
+	var fn func(fml Formula) []string
+	var subFn = func(ch chan []string, subfml Formula) { ch <- fn(subfml) }
+	fn = func(fml Formula) []string {
+		var subfmls = fml.GetSubFormulae()
+		var n = len(subfmls)
+		var subChan = make([](chan []string), n)
+		var prevValues = make([][]string, len(subfmls))
+		// start parallel computations on subformulas
+		for i, subfml := range subfmls {
+			subChan[i] = make(chan []string) // create Channel, since currently nil
+			go subFn(subChan[i], subfml)
+		}
+		// successively read values
+		for i := 0; i < n; i++ {
+			prevValues[i] = <-subChan[i]
+		}
+		// apply schema to get value for formula
+		return scheme(fml, prevValues)
+	}
+	return fn
+}
+
+/* ---------------------------------------------------------------- *
+ * Generate Formula-value Fn from scheme
+ * ---------------------------------------------------------------- */
+
+func CreateFromSchemeFmlValued(scheme func(fml Formula, prevValues []Formula) Formula) func(fml Formula) Formula {
+	var fn func(fml Formula) Formula
+	var subFn = func(ch chan Formula, subfml Formula) { ch <- fn(subfml) }
+	fn = func(fml Formula) Formula {
+		var subfmls = fml.GetSubFormulae()
+		var n = len(subfmls)
+		var subChan = make([](chan Formula), n)
+		var prevValues = make([]Formula, len(subfmls))
+		// start parallel computations on subformulas
+		for i, subfml := range subfmls {
+			subChan[i] = make(chan Formula) // create Channel, since currently nil
+			go subFn(subChan[i], subfml)
+		}
+		// successively read values
+		for i := 0; i < n; i++ {
+			prevValues[i] = <-subChan[i]
+		}
+		// apply schema to get value for formula
+		return scheme(fml, prevValues)
+	}
+	return fn
+}
+
+/* ---------------------------------------------------------------- *
+ * Generate *[]Formula-value Fn from scheme
+ * ---------------------------------------------------------------- */
+
+func CreateFromSchemeFmlsValued(scheme func(fml Formula, prevValues [](*[]Formula)) *[]Formula) func(fml Formula) *[]Formula {
+	var fn func(fml Formula) *[]Formula
+	var subFn = func(ch chan *[]Formula, subfml Formula) { ch <- fn(subfml) }
+	fn = func(fml Formula) *[]Formula {
+		var subfmls = fml.GetSubFormulae()
+		var n = len(subfmls)
+		var subChan = make([](chan *[]Formula), n)
+		var prevValues = make([](*[]Formula), len(subfmls))
+		// start parallel computations on subformulas
+		for i, subfml := range subfmls {
+			subChan[i] = make(chan *[]Formula) // create Channel, since currently nil
+			go subFn(subChan[i], subfml)
+		}
+		// successively read values
+		for i := 0; i < n; i++ {
+			prevValues[i] = <-subChan[i]
+		}
+		// apply schema to get value for formula
+		return scheme(fml, prevValues)
+	}
+	return fn
+}
+
+/* ---------------------------------------------------------------- *
+ * Generate {pos: Formula, ne: Formula}-value Fn from scheme
+ * ---------------------------------------------------------------- */
+
+func CreateFromSchemeFmlPairValued(scheme func(fml Formula, prevValues []FormulaPair) FormulaPair) func(fml Formula) FormulaPair {
+	var fn func(fml Formula) FormulaPair
+	var subFn = func(ch chan FormulaPair, subfml Formula) { ch <- fn(subfml) }
+	fn = func(fml Formula) FormulaPair {
+		var subfmls = fml.GetSubFormulae()
+		var n = len(subfmls)
+		var subChan = make([](chan FormulaPair), n)
+		var prevValues = make([]FormulaPair, len(subfmls))
+		// start parallel computations on subformulas
+		for i, subfml := range subfmls {
+			subChan[i] = make(chan FormulaPair) // create Channel, since currently nil
+			go subFn(subChan[i], subfml)
+		}
+		// successively read values
+		for i := 0; i < n; i++ {
+			prevValues[i] = <-subChan[i]
+		}
+		// apply schema to get value for formula
+		return scheme(fml, prevValues)
+	}
+	return fn
+}
diff --git a/codego/aussagenlogik/formulae/formulae_types.go b/codego/aussagenlogik/formulae/formulae_types.go
new file mode 100644
index 0000000..2a493f4
--- /dev/null
+++ b/codego/aussagenlogik/formulae/formulae_types.go
@@ -0,0 +1,34 @@
+package formulae
+
+/* ---------------------------------------------------------------- *
+ * 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
+}
diff --git a/codego/aussagenlogik/recursion/recursion_atoms.go b/codego/aussagenlogik/recursion/recursion_atoms.go
new file mode 100644
index 0000000..acdd395
--- /dev/null
+++ b/codego/aussagenlogik/recursion/recursion_atoms.go
@@ -0,0 +1,20 @@
+package recursion
+
+import (
+	"logik/aussagenlogik/formulae"
+)
+
+/* ---------------------------------------------------------------- *
+ * METHOD: Atoms
+ * ---------------------------------------------------------------- */
+
+func Atoms(tree formulae.Formula) []string {
+	// Definiere Schema:
+	var schema = func(tree formulae.Formula, prevValues [][]string) []string {
+		// Herausforderung: schreibe diese Funktion!
+		return []string{}
+	}
+	// Erzeuge Funktion aus Schema und berechne Wert:
+	fn := formulae.CreateFromSchemeStringsValued(schema)
+	return fn(tree)
+}
diff --git a/codego/aussagenlogik/recursion/recursion_count.go b/codego/aussagenlogik/recursion/recursion_count.go
new file mode 100644
index 0000000..200f40f
--- /dev/null
+++ b/codego/aussagenlogik/recursion/recursion_count.go
@@ -0,0 +1,49 @@
+package recursion
+
+import (
+	"logik/aussagenlogik/formulae"
+)
+
+/* ---------------------------------------------------------------- *
+ * METHOD: Formula Depth
+ * ---------------------------------------------------------------- */
+
+func FmlDepth(tree formulae.Formula) int {
+	// Definiere Schema:
+	var schema = func(tree formulae.Formula, prevValues []int) int {
+		// Herausforderung: schreibe diese Funktion!
+		return 0
+	}
+	// Erzeuge Funktion aus Schema und berechne Wert:
+	fn := formulae.CreateFromSchemeIntValued(schema)
+	return fn(tree)
+}
+
+/* ---------------------------------------------------------------- *
+ * METHOD: Formula Length
+ * ---------------------------------------------------------------- */
+
+func FmlLength(tree formulae.Formula) int {
+	// Definiere Schema:
+	var schema = func(tree formulae.Formula, prevValues []int) int {
+		// Herausforderung: schreibe diese Funktion!
+		return 0
+	}
+	// Erzeuge Funktion aus Schema und berechne Wert:
+	fn := formulae.CreateFromSchemeIntValued(schema)
+	return fn(tree)
+}
+
+/* ---------------------------------------------------------------- *
+ * METHOD: Number of Parentheses
+ * ---------------------------------------------------------------- */
+func NrParentheses(tree formulae.Formula) int {
+	// Definiere Schema:
+	var schema = func(tree formulae.Formula, prevValues []int) int {
+		// Herausforderung: schreibe diese Funktion!
+		return 0
+	}
+	// Erzeuge Funktion aus Schema und berechne Wert:
+	fn := formulae.CreateFromSchemeIntValued(schema)
+	return fn(tree)
+}
diff --git a/codego/aussagenlogik/recursion/recursion_eval.go b/codego/aussagenlogik/recursion/recursion_eval.go
new file mode 100644
index 0000000..8e5ce15
--- /dev/null
+++ b/codego/aussagenlogik/recursion/recursion_eval.go
@@ -0,0 +1,42 @@
+package recursion
+
+import (
+	"logik/aussagenlogik/formulae"
+	"logik/core/utils"
+)
+
+/* ---------------------------------------------------------------- *
+ * METHOD: Evaluation of fomulae in models
+ * ---------------------------------------------------------------- */
+
+func Eval(tree formulae.Formula, I []string) int {
+	// Definiere (parameterisiertes) Schema:
+	var schema = func(_I []string) func(formulae.Formula, []int) int {
+		return func(tree formulae.Formula, prevValues []int) int {
+			if tree.IsAtom() || tree.IsGeneric() {
+				return utils.BoolToInt(utils.StrListContains(_I, tree.GetExpr()))
+			} else if tree.IsTautologySymbol() {
+				return 1
+			} else if tree.IsContradictionSymbol() {
+				return 0
+			} else if tree.IsNegation() {
+				return 1 - prevValues[0]
+			} else if tree.IsConjunction2() {
+				return utils.Min2(prevValues[0], prevValues[1])
+			} else if tree.IsConjunction() {
+				return utils.MinList(prevValues)
+			} else if tree.IsDisjunction2() {
+				return utils.Max2(prevValues[0], prevValues[1])
+			} else if tree.IsDisjunction() {
+				return utils.MaxList(prevValues)
+			} else if tree.IsImplication() {
+				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(tree)
+}
diff --git a/codego/aussagenlogik/recursion/recursion_nnf.go b/codego/aussagenlogik/recursion/recursion_nnf.go
new file mode 100644
index 0000000..73e1ec0
--- /dev/null
+++ b/codego/aussagenlogik/recursion/recursion_nnf.go
@@ -0,0 +1,77 @@
+package recursion
+
+import (
+	"logik/aussagenlogik/formulae"
+)
+
+/* ---------------------------------------------------------------- *
+ * METHOD: compute NNF
+ * ---------------------------------------------------------------- */
+
+// NOTE: diese bedarf einer Art Doppeltrekursion
+func NNF(tree formulae.Formula) formulae.Formula {
+	// Definiere Schema:
+	var schema = func(tree 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 tree.IsPositiveLiteral() {
+			return formulae.FormulaPair{
+				Pos: tree.Deepcopy(),
+				Neg: formulae.Negation(tree),
+			}
+		} else if tree.IsNegativeLiteral() {
+			return formulae.FormulaPair{
+				Pos: tree.Deepcopy(),
+				Neg: prevPos[0],
+			}
+		} else if tree.IsTautologySymbol() {
+			return formulae.FormulaPair{
+				Pos: formulae.Tautology,
+				Neg: formulae.Contradiction,
+			}
+		} else if tree.IsContradictionSymbol() {
+			return formulae.FormulaPair{
+				Pos: formulae.Contradiction,
+				Neg: formulae.Tautology,
+			}
+		} else if tree.IsNegation() {
+			return formulae.FormulaPair{
+				Pos: prevNeg[0],
+				Neg: prevPos[0],
+			}
+		} else if tree.IsConjunction2() {
+			return formulae.FormulaPair{
+				Pos: formulae.Conjunction2(prevPos[0], prevPos[1]),
+				Neg: formulae.Disjunction2(prevNeg[0], prevNeg[1]),
+			}
+		} else if tree.IsConjunction() {
+			return formulae.FormulaPair{
+				Pos: formulae.Conjunction(prevPos),
+				Neg: formulae.Disjunction(prevNeg),
+			}
+		} else if tree.IsDisjunction2() {
+			return formulae.FormulaPair{
+				Pos: formulae.Disjunction2(prevPos[0], prevPos[1]),
+				Neg: formulae.Conjunction2(prevNeg[0], prevNeg[1]),
+			}
+		} else if tree.IsDisjunction() {
+			return formulae.FormulaPair{
+				Pos: formulae.Disjunction(prevPos),
+				Neg: formulae.Conjunction(prevNeg),
+			}
+		} else if tree.IsImplication() {
+			return formulae.FormulaPair{
+				Pos: formulae.Implies(prevPos[0], prevPos[1]),
+				Neg: formulae.Conjunction2(prevPos[0], prevNeg[1]),
+			}
+		} else {
+			panic("Could not evaluate expression!")
+		}
+	}
+	// Erzeuge Funktion aus Schema und berechne Wert:
+	fn := formulae.CreateFromSchemeFmlPairValued(schema)
+	return fn(tree).Pos
+}
diff --git a/codego/aussagenlogik/recursion/recursion_test.go b/codego/aussagenlogik/recursion/recursion_test.go
new file mode 100644
index 0000000..fb43757
--- /dev/null
+++ b/codego/aussagenlogik/recursion/recursion_test.go
@@ -0,0 +1,359 @@
+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 TestEvalComplex1(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)
+}
+
+func TestEvalComplex2(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(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")
+	test.Skip("Syntax for generic expressions in ANTLR4 g4 needs to be implemented.")
+	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)
+	utils.SortStrings(&val)
+	assert.Equal([]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)
+	utils.SortStrings(&val)
+	assert.Equal([]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())
+}
diff --git a/codego/aussagenlogik/rekursion/rekursion.go b/codego/aussagenlogik/rekursion/rekursion.go
deleted file mode 100644
index a06735d..0000000
--- a/codego/aussagenlogik/rekursion/rekursion.go
+++ /dev/null
@@ -1,70 +0,0 @@
-package rekursion
-
-import (
-	"logik/aussagenlogik/syntaxbaum"
-	"logik/core/utils"
-)
-
-/* ---------------------------------------------------------------- *
- * EXPORTS
- * ---------------------------------------------------------------- */
-
-type RekursiveChannelInt struct {
-	channel chan int
-}
-
-func RekursivEval(ch chan int, tree syntaxbaum.SyntaxBaum, I []string) {
-	// Werte für Teilformeln rekursiv berechnen
-	fn := func(_ch chan int, _tree syntaxbaum.SyntaxBaum) { RekursivEval(_ch, _tree, I) }
-	var values = RekursiveCallInt(fn, tree.GetChildren())
-	// Aus Werten für Teilformeln Wert für Formeln berechnen
-	if tree.IsAtom() || tree.IsGeneric() {
-		ch <- utils.BoolToInt(utils.StrListContains(I, tree.GetExpr()))
-	} else if tree.IsTautologySymbol() {
-		ch <- 1
-	} else if tree.IsContradictionSymbol() {
-		ch <- 0
-	} else if tree.IsNegation() {
-		ch <- 1 - values[0]
-	} else if tree.IsConjunction2() {
-		ch <- utils.Min2(values[0], values[1])
-	} else if tree.IsConjunction() {
-		ch <- utils.MinList(values)
-	} else if tree.IsDisjunction2() {
-		ch <- utils.Max2(values[0], values[1])
-	} else if tree.IsDisjunction() {
-		ch <- utils.MaxList(values)
-	} else if tree.IsImplication() {
-		ch <- utils.BoolToInt(values[0] <= values[1])
-	} else {
-		panic("Could not evaluate expression!")
-	}
-}
-
-func RekursivAtoms(ch chan []string, tree syntaxbaum.SyntaxBaum) {
-	// // Werte für Teilformeln rekursiv berechnen
-	// var values = RekursiveCallStringList(RekursivAtoms, tree.GetChildren())
-	// Herausforderung: schreibe diese Funktion!
-	ch <- []string{}
-}
-
-func RekursivDepth(ch chan int, tree syntaxbaum.SyntaxBaum) {
-	// // Werte für Teilformeln rekursiv berechnen
-	// var values = RekursiveCallInt(RekursivDepth, tree.GetChildren())
-	// Herausforderung: schreibe diese Funktion!
-	ch <- 0
-}
-
-func RekursivLength(ch chan int, tree syntaxbaum.SyntaxBaum) {
-	// // Werte für Teilformeln rekursiv berechnen
-	// var values = RekursiveCallInt(RekursivLength, tree.GetChildren())
-	// Herausforderung: schreibe diese Funktion!
-	ch <- 0
-}
-
-func RekursivParentheses(ch chan int, tree syntaxbaum.SyntaxBaum) {
-	// // Werte für Teilformeln rekursiv berechnen
-	// var values = RekursiveCallInt(RekursivParentheses, tree.GetChildren())
-	// Herausforderung: schreibe diese Funktion!
-	ch <- 0
-}
diff --git a/codego/aussagenlogik/rekursion/rekursion_aux.go b/codego/aussagenlogik/rekursion/rekursion_aux.go
deleted file mode 100644
index c9f806d..0000000
--- a/codego/aussagenlogik/rekursion/rekursion_aux.go
+++ /dev/null
@@ -1,51 +0,0 @@
-package rekursion
-
-import (
-	"logik/aussagenlogik/syntaxbaum"
-)
-
-/* ---------------------------------------------------------------- *
- * EXPORTS
- * ---------------------------------------------------------------- */
-
-func RekursiveCallInt(fn func(ch chan int, tree syntaxbaum.SyntaxBaum), children []syntaxbaum.SyntaxBaum) []int {
-	subChannel := make(chan int)
-	values := make([]int, len(children))
-	// start parallel computations on subformulae
-	for _, subtree := range children {
-		go fn(subChannel, subtree)
-	}
-	// successively read values
-	for i := 0; i < len(children); i++ {
-		values[i] = <-subChannel
-	}
-	return values
-}
-
-func RekursiveCallString(fn func(ch chan string, tree syntaxbaum.SyntaxBaum), children []syntaxbaum.SyntaxBaum) []string {
-	subChannel := make(chan string)
-	values := make([]string, len(children))
-	// start parallel computations
-	for _, subtree := range children {
-		go fn(subChannel, subtree)
-	}
-	// successively read values
-	for i := 0; i < len(children); i++ {
-		values[i] = <-subChannel
-	}
-	return values
-}
-
-func RekursiveCallStringList(fn func(ch chan []string, tree syntaxbaum.SyntaxBaum), children []syntaxbaum.SyntaxBaum) [][]string {
-	subChannel := make(chan []string)
-	values := make([][]string, len(children))
-	// start parallel computations
-	for _, subtree := range children {
-		go fn(subChannel, subtree)
-	}
-	// successively read values
-	for i := 0; i < len(children); i++ {
-		values[i] = <-subChannel
-	}
-	return values
-}
diff --git a/codego/aussagenlogik/rekursion/rekursion_test.go b/codego/aussagenlogik/rekursion/rekursion_test.go
deleted file mode 100644
index 991c33d..0000000
--- a/codego/aussagenlogik/rekursion/rekursion_test.go
+++ /dev/null
@@ -1,295 +0,0 @@
-package rekursion_test
-
-/* ---------------------------------------------------------------- *
- * UNIT TESTING
- * ---------------------------------------------------------------- */
-
-import (
-	"logik/aussagenlogik/rekursion"
-	"logik/aussagenlogik/schema"
-	"logik/aussagenlogik/syntaxbaum"
-	"logik/core/utils"
-	"testing"
-
-	"github.com/stretchr/testify/assert"
-)
-
-/* ---------------------------------------------------------------- *
- * TESTCASE eval(·, ·)
- * ---------------------------------------------------------------- */
-
-func TestRekursivEvalLiteral(test *testing.T) {
-	var assert = assert.New(test)
-	var ch = make(chan int)
-	var tree syntaxbaum.SyntaxBaum
-	var I []string
-	tree = schema.ParseExpr("A0")
-	I = []string{"A0"}
-	go rekursion.RekursivEval(ch, tree, I)
-	assert.Equal(1, <-ch)
-	tree = schema.ParseExpr("A0")
-	I = []string{}
-	go rekursion.RekursivEval(ch, tree, I)
-	assert.Equal(0, <-ch)
-	tree = schema.ParseExpr("! A0")
-	I = []string{"A0"}
-	go rekursion.RekursivEval(ch, tree, I)
-	assert.Equal(0, <-ch)
-	tree = schema.ParseExpr("! A0")
-	I = []string{}
-	go rekursion.RekursivEval(ch, tree, I)
-	assert.Equal(1, <-ch)
-}
-
-func TestRekursivEvalComplex1(test *testing.T) {
-	var assert = assert.New(test)
-	var ch = make(chan int)
-	var tree syntaxbaum.SyntaxBaum
-	var I []string
-	tree = schema.ParseExpr("( ! A0 || (( A0 && A3 ) || A2 ))")
-	I = []string{"A0", "A2"}
-	go rekursion.RekursivEval(ch, tree, I)
-	assert.Equal(1, <-ch)
-	I = []string{"A0", "A3"}
-	go rekursion.RekursivEval(ch, tree, I)
-	assert.Equal(1, <-ch)
-	I = []string{"A0"}
-	go rekursion.RekursivEval(ch, tree, I)
-	assert.Equal(0, <-ch)
-	I = []string{"A4", "A8"}
-	go rekursion.RekursivEval(ch, tree, I)
-	assert.Equal(1, <-ch)
-}
-
-func TestRekursivEvalComplex2(test *testing.T) {
-	var assert = assert.New(test)
-	var ch = make(chan int)
-	var tree syntaxbaum.SyntaxBaum
-	var I []string
-	tree = schema.ParseExpr("( ! A0 || (( A0 && A3 ) || ! A2 ))")
-	I = []string{"A0", "A2"}
-	go rekursion.RekursivEval(ch, tree, I)
-	assert.Equal(0, <-ch)
-	I = []string{"A0", "A3"}
-	go rekursion.RekursivEval(ch, tree, I)
-	assert.Equal(1, <-ch)
-}
-
-/* ---------------------------------------------------------------- *
- * TESTCASE Atoms(·)
- * ---------------------------------------------------------------- */
-
-func TestRekursivAtomsNoduplicates(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	var assert = assert.New(test)
-	var ch = make(chan []string)
-	var tree syntaxbaum.SyntaxBaum
-	var val []string
-	tree = schema.ParseExpr("( A4 && ( A4 || A4 ))")
-	go rekursion.RekursivAtoms(ch, tree)
-	val = <-ch
-	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 TestRekursivAtomsNononatoms(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	test.Skip("Syntax for generic expressions in ANTLR4 g4 needs to be implemented.")
-	var assert = assert.New(test)
-	var ch = make(chan []string)
-	var tree syntaxbaum.SyntaxBaum
-	var val []string
-	tree = schema.ParseExpr("( {F} || A3 )")
-	go rekursion.RekursivAtoms(ch, tree)
-	val = <-ch
-	utils.SortStrings(&val)
-	assert.NotContains(val, "F", "Nichtatomare Formeln dürfen nicht vorkommen!")
-}
-
-func TestRekursivAtomsCalc1(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	var assert = assert.New(test)
-	var ch = make(chan []string)
-	var tree syntaxbaum.SyntaxBaum
-	var val []string
-	tree = schema.ParseExpr("A0")
-	go rekursion.RekursivAtoms(ch, tree)
-	val = <-ch
-	utils.SortStrings(&val)
-	assert.Equal([]string{"A0"}, val)
-}
-
-func TestRekursivAtomsCalc2(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	var assert = assert.New(test)
-	var ch = make(chan []string)
-	var tree syntaxbaum.SyntaxBaum
-	var val []string
-	tree = schema.ParseExpr("((( ! A8 && A3 ) || A4 ) && A0 )")
-	go rekursion.RekursivAtoms(ch, tree)
-	val = <-ch
-	utils.SortStrings(&val)
-	assert.Equal([]string{"A0", "A3", "A4", "A8"}, val)
-}
-
-/* ---------------------------------------------------------------- *
- * TESTCASE depth(·, ·)
- * ---------------------------------------------------------------- */
-
-func TestRekursivDepthCalc1(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	var assert = assert.New(test)
-	var ch = make(chan int)
-	var tree syntaxbaum.SyntaxBaum
-	tree = schema.ParseExpr("A0")
-	go rekursion.RekursivDepth(ch, tree)
-	assert.Equal(0, <-ch)
-}
-
-func TestRekursivDepthCalc2(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	var assert = assert.New(test)
-	var ch = make(chan int)
-	var tree syntaxbaum.SyntaxBaum
-	tree = schema.ParseExpr("!! A8")
-	go rekursion.RekursivDepth(ch, tree)
-	assert.Equal(2, <-ch)
-}
-
-func TestRekursivDepthCalc3(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	var assert = assert.New(test)
-	var ch = make(chan int)
-	var tree syntaxbaum.SyntaxBaum
-	tree = schema.ParseExpr("( ! A0 && A3 )")
-	go rekursion.RekursivDepth(ch, tree)
-	assert.Equal(2, <-ch)
-}
-
-func TestRekursivDepthCalc4(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	var assert = assert.New(test)
-	var ch = make(chan int)
-	var tree syntaxbaum.SyntaxBaum
-	tree = schema.ParseExpr("((( ! A0 && A3 ) || A4 ) && A8 )")
-	go rekursion.RekursivDepth(ch, tree)
-	assert.Equal(4, <-ch)
-}
-
-func TestRekursivDepthCalc5(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	var assert = assert.New(test)
-	var ch = make(chan int)
-	var tree syntaxbaum.SyntaxBaum
-	tree = schema.ParseExpr("! ((( ! A0 && A3 ) || A4 ) && A8 )")
-	go rekursion.RekursivDepth(ch, tree)
-	assert.Equal(5, <-ch)
-}
-
-/* ---------------------------------------------------------------- *
- * TESTCASE length(·)
- * ---------------------------------------------------------------- */
-
-func TestRekursivLengthCalc1(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	var assert = assert.New(test)
-	var ch = make(chan int)
-	var tree syntaxbaum.SyntaxBaum
-	tree = schema.ParseExpr("A0")
-	go rekursion.RekursivLength(ch, tree)
-	assert.Equal(1, <-ch)
-}
-
-func TestRekursivLengthCalc2(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	var assert = assert.New(test)
-	var ch = make(chan int)
-	var tree syntaxbaum.SyntaxBaum
-	tree = schema.ParseExpr("!! A8")
-	go rekursion.RekursivLength(ch, tree)
-	assert.Equal(3, <-ch)
-}
-
-func TestRekursivLengthCalc3(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	var assert = assert.New(test)
-	var ch = make(chan int)
-	var tree syntaxbaum.SyntaxBaum
-	tree = schema.ParseExpr("( ! A0 && A3 )")
-	go rekursion.RekursivLength(ch, tree)
-	assert.Equal(4, <-ch)
-}
-
-func TestRekursivLengthCalc4(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	var assert = assert.New(test)
-	var ch = make(chan int)
-	var tree syntaxbaum.SyntaxBaum
-	tree = schema.ParseExpr("((( ! A0 && A3 ) || A4 ) && A8 )")
-	go rekursion.RekursivLength(ch, tree)
-	assert.Equal(8, <-ch)
-}
-
-func TestRekursivLengthCalc5(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	var assert = assert.New(test)
-	var ch = make(chan int)
-	var tree syntaxbaum.SyntaxBaum
-	tree = schema.ParseExpr("! ((( ! A0 && A3 ) || A4 ) && A8 )")
-	go rekursion.RekursivLength(ch, tree)
-	assert.Equal(9, <-ch)
-}
-
-/* ---------------------------------------------------------------- *
- * TESTCASE #Parentheses(·)
- * ---------------------------------------------------------------- */
-
-func TestRekursivParenthesesCalc1(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	var assert = assert.New(test)
-	var ch = make(chan int)
-	var tree syntaxbaum.SyntaxBaum
-	tree = schema.ParseExpr("A0")
-	go rekursion.RekursivParentheses(ch, tree)
-	assert.Equal(0, <-ch)
-}
-
-func TestRekursivParenthesesCalc2(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	var assert = assert.New(test)
-	var ch = make(chan int)
-	var tree syntaxbaum.SyntaxBaum
-	tree = schema.ParseExpr("!! A8")
-	go rekursion.RekursivParentheses(ch, tree)
-	assert.Equal(0, <-ch)
-}
-
-func TestRekursivParenthesesCalc3(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	var assert = assert.New(test)
-	var ch = make(chan int)
-	var tree syntaxbaum.SyntaxBaum
-	tree = schema.ParseExpr("( ! A0 && A3 )")
-	go rekursion.RekursivParentheses(ch, tree)
-	assert.Equal(2, <-ch)
-}
-
-func TestRekursivParenthesesCalc4(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	var assert = assert.New(test)
-	var ch = make(chan int)
-	var tree syntaxbaum.SyntaxBaum
-	tree = schema.ParseExpr("((( ! A0 && A3 ) || A4 ) && A8 )")
-	go rekursion.RekursivParentheses(ch, tree)
-	assert.Equal(6, <-ch)
-}
-
-func TestRekursivParenthesesCalc5(test *testing.T) {
-	test.Skip("Methode noch nicht implementiert")
-	var assert = assert.New(test)
-	var ch = make(chan int)
-	var tree syntaxbaum.SyntaxBaum
-	tree = schema.ParseExpr("! ((( ! A0 && A3 ) || A4 ) && A8 )")
-	go rekursion.RekursivParentheses(ch, tree)
-	assert.Equal(6, <-ch)
-}
diff --git a/codego/aussagenlogik/schema/schema.go b/codego/aussagenlogik/schema/schema.go
index cadf525..782b620 100644
--- a/codego/aussagenlogik/schema/schema.go
+++ b/codego/aussagenlogik/schema/schema.go
@@ -1,9 +1,8 @@
 package schema
 
 import (
-	"logik/aussagenlogik/syntaxbaum"
+	"logik/aussagenlogik/formulae"
 	parser "logik/grammars/aussagenlogik"
-	"strings"
 
 	"github.com/antlr/antlr4/runtime/Go/antlr"
 )
@@ -12,12 +11,12 @@ import (
  * EXPORTS
  * ---------------------------------------------------------------- */
 
-func ParseExpr(u string) syntaxbaum.SyntaxBaum {
+func ParseExpr(u string) formulae.Formula {
 	var lexer = createLexer(u)
 	var tokenStream = lexerToTokenStream(lexer)
 	var prs = parser.NewaussagenlogikParser(tokenStream)
 	var t = prs.Start()
-	tree := createSyntaxBaum(t, prs)
+	tree := createFormula(t, prs)
 	return tree
 }
 
@@ -38,9 +37,9 @@ func createLexer(u string) antlr.Lexer {
 	return parser.NewaussagenlogikLexer(stream)
 }
 
-func createSyntaxBaum(tree antlr.Tree, parser antlr.Parser) syntaxbaum.SyntaxBaum {
+func createFormula(tree antlr.Tree, parser antlr.Parser) formulae.Formula {
 	var ant = antlrTree{tree: tree, parser: &parser}
-	return ant.toSyntaxBaum()
+	return ant.toFormula()
 }
 
 /* ---------------------------------------------------------------- *
@@ -86,8 +85,7 @@ func (ant antlrTree) getTextContentLeaves() string {
 	return expr
 }
 
-func (ant antlrTree) toSyntaxBaum() syntaxbaum.SyntaxBaum {
-	var tree syntaxbaum.SyntaxBaum
+func (ant antlrTree) toFormula() formulae.Formula {
 	var label string = ant.getLabel()
 	var subants = ant.getChildren()
 	var nChildren = len(subants)
@@ -95,65 +93,73 @@ func (ant antlrTree) toSyntaxBaum() syntaxbaum.SyntaxBaum {
 	switch label {
 	case "start":
 		if nChildren == 1 {
-			return subants[0].toSyntaxBaum()
+			return subants[0].toFormula()
 		}
 	case "open":
 		if nChildren == 1 {
-			return subants[0].toSyntaxBaum()
+			return subants[0].toFormula()
 		}
 	case "closed":
 		switch nChildren {
 		case 1:
-			return subants[0].toSyntaxBaum()
+			return subants[0].toFormula()
+		// expr = ( expr )
 		case 3:
-			return subants[1].toSyntaxBaum()
+			return subants[1].toFormula()
 		}
 	case "atomic":
 		if nChildren == 1 {
-			subant := subants[0]
-			tree = syntaxbaum.SyntaxBaum{}
-			tree.SetKind(subant.getLabel())
-			tree.SetExpr(subant.getTextContentLeaves())
-			tree.SetChildren([](*syntaxbaum.SyntaxBaum){})
-			return tree
+			return subants[0].toFormula()
 		}
+	case "taut":
+		return formulae.Tautology
+	case "contradiction":
+		return formulae.Contradiction
+	case "atom":
+		return formulae.Atom(ant.getTextContentLeaves())
+	case "generic":
+		return formulae.Generic(ant.getTextContentLeaves())
 	case "not":
+		// NOTE: expr = ! expr
 		if nChildren == 2 {
-			// NOTE: Children = [NotSymbol, Teilformel]
-			subtree := subants[1].toSyntaxBaum()
-			tree = syntaxbaum.SyntaxBaum{}
-			tree.SetKind(label)
-			tree.SetExpr(subants[0].getTextContent() + " " + subtree.GetExpr())
-			tree.SetChildren([](*syntaxbaum.SyntaxBaum){&subtree})
-			return tree
+			return formulae.Negation(subants[1].toFormula())
 		}
-	case "and2", "and", "or2", "or", "implies":
+	case "and2":
+		// NOTE: expr = expr && expr
+		if nChildren == 3 {
+			return formulae.Conjunction2(subants[0].toFormula(), subants[2].toFormula())
+		}
+	case "or2":
+		// NOTE: expr = expr || expr
+		if nChildren == 3 {
+			return formulae.Disjunction2(subants[0].toFormula(), subants[2].toFormula())
+		}
+	case "implies":
+		// NOTE: expr = expr -> expr
+		if nChildren == 3 {
+			return formulae.Implies(subants[0].toFormula(), subants[2].toFormula())
+		}
+	case "and", "or":
+		// NOTE: expr = expr op expr op ... op expr
 		var n int = int((len(subants) + 1) / 2)
 		if nChildren == 2*n-1 && n >= 2 {
-			var isSymb bool = false
-			var subtrees = make([](*syntaxbaum.SyntaxBaum), n)
+			var subtrees = make([]formulae.Formula, n)
+			var isSymb bool = true
 			var i int = 0
-			var expr string = ""
 			for _, subant := range subants {
 				if isSymb {
-					expr += " " + subant.getTextContent()
-				} else {
-					subtree := subant.toSyntaxBaum()
-					subtrees[i] = &subtree
-					expr += " " + subtree.GetExpr()
+					subtrees[i] = subant.toFormula()
 					i++
 				}
 				// NOTE: infix notation: alternatives between expression and symbol
 				isSymb = !isSymb
 			}
-			expr = strings.Trim(expr, " ")
-			var lbrace string = "("
-			var rbrace string = ")"
-			tree = syntaxbaum.SyntaxBaum{}
-			tree.SetKind(label)
-			tree.SetExpr(lbrace + expr + rbrace)
-			tree.SetChildren(subtrees)
-			return tree
+			switch label {
+			case "and":
+				return formulae.Conjunction(subtrees)
+			case "or":
+				return formulae.Disjunction(subtrees)
+			}
 		}
 	}
 
diff --git a/codego/aussagenlogik/schema/schema_test.go b/codego/aussagenlogik/schema/schema_test.go
index f7878bd..4fd4110 100644
--- a/codego/aussagenlogik/schema/schema_test.go
+++ b/codego/aussagenlogik/schema/schema_test.go
@@ -5,8 +5,8 @@ package schema_test
  * ---------------------------------------------------------------- */
 
 import (
+	"logik/aussagenlogik/formulae"
 	"logik/aussagenlogik/schema"
-	"logik/aussagenlogik/syntaxbaum"
 	"testing"
 
 	"github.com/stretchr/testify/assert"
@@ -18,25 +18,25 @@ import (
 
 func TestParseExpr(test *testing.T) {
 	var assert = assert.New(test)
-	var tree syntaxbaum.SyntaxBaum
+	var tree formulae.Formula
 
 	tree = schema.ParseExpr("A8712")
 	assert.Equal("A8712", tree.GetExpr())
 	assert.Equal("atom", tree.GetKind())
-	assert.Equal(0, len(tree.GetChildren()))
+	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.GetChildren()))
+	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.GetChildren()))
+	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.GetChildren()))
+	assert.Equal(2, len(tree.GetSubFormulae()))
 }
diff --git a/codego/aussagenlogik/syntaxbaum/syntaxbaum.go b/codego/aussagenlogik/syntaxbaum/syntaxbaum.go
deleted file mode 100644
index 9aa7478..0000000
--- a/codego/aussagenlogik/syntaxbaum/syntaxbaum.go
+++ /dev/null
@@ -1,154 +0,0 @@
-package syntaxbaum
-
-import (
-	"errors"
-	"fmt"
-	"strings"
-)
-
-type SyntaxBaum struct {
-	kind     string
-	expr     string
-	valence  int
-	children [](*SyntaxBaum)
-}
-
-/* ---------------------------------------------------------------- *
- * METHODS
- * ---------------------------------------------------------------- */
-func (tree *SyntaxBaum) SetKind(kind string) {
-	tree.kind = kind
-}
-
-func (tree SyntaxBaum) GetKind() string {
-	return tree.kind
-}
-
-func (tree *SyntaxBaum) SetExpr(expr string) {
-	tree.expr = expr
-}
-
-func (tree SyntaxBaum) GetExpr() string {
-	return tree.expr
-}
-
-func (tree *SyntaxBaum) SetChildren(children [](*SyntaxBaum)) {
-	tree.children = children
-	tree.valence = len(children)
-}
-
-func (tree SyntaxBaum) GetChildren() []SyntaxBaum {
-	var n int = tree.valence
-	var children = make([]SyntaxBaum, n)
-	for i, subtreePtr := range tree.children {
-		children[i] = *subtreePtr
-	}
-	return children
-}
-
-func (tree SyntaxBaum) GetChild(indexOpt ...int) (SyntaxBaum, error) {
-	var index int = 0
-	if len(indexOpt) > 0 {
-		index = indexOpt[0]
-	}
-	var subtree SyntaxBaum
-	var err error
-	if 0 <= index && index < tree.valence {
-		subtree = *(tree.children[index])
-	} else {
-		err = errors.New(fmt.Sprintf("Instance has no child of index %d !", index))
-	}
-	return subtree, err
-}
-
-func (tree SyntaxBaum) Pretty(preindentOpt ...string) string {
-	var preindent string = ""
-	if len(preindentOpt) > 0 {
-		preindent = preindentOpt[0]
-	}
-	return tree.pretty(preindent, "  ", "", 0)
-}
-
-func (tree SyntaxBaum) pretty(preindent string, tab string, prepend string, depth int) string {
-	var indent string = preindent + strings.Repeat(tab, depth)
-	switch tree.valence {
-	case 0:
-		switch kind := tree.kind; kind {
-		case "atom", "generic":
-			return indent + prepend + kind + " " + tree.expr
-		default:
-			return indent + prepend + kind
-		}
-	default:
-		var lines string = indent + prepend + tree.kind
-		prepend = "|__ "
-		for _, subtree := range tree.children {
-			lines += "\n" + subtree.pretty(preindent, tab, prepend, depth+1)
-		}
-		return lines
-	}
-}
-
-// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-// METHODS: Recognitong of Formula-Types
-// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-func (tree SyntaxBaum) IsIrreducible() bool {
-	return tree.valence == 0
-}
-
-func (tree SyntaxBaum) IsAtom() bool {
-	return tree.kind == "atom"
-}
-
-func (tree SyntaxBaum) IsLiteral() bool {
-	if tree.IsAtom() {
-		return true
-	} else if tree.IsNegation() {
-		subtree, err := tree.GetChild()
-		if err == nil {
-			return subtree.IsAtom()
-		}
-	}
-	return false
-}
-
-func (tree SyntaxBaum) IsGeneric() bool {
-	return tree.kind == "generic"
-}
-
-func (tree SyntaxBaum) IsTautologySymbol() bool {
-	return tree.kind == "taut"
-}
-
-func (tree SyntaxBaum) IsContradictionSymbol() bool {
-	return tree.kind == "contradiction"
-}
-
-func (tree SyntaxBaum) IsConnective() bool {
-	return tree.valence > 0
-}
-
-func (tree SyntaxBaum) IsNegation() bool {
-	return tree.kind == "not"
-}
-
-func (tree SyntaxBaum) IsConjunction2() bool {
-	return tree.kind == "and2"
-}
-
-func (tree SyntaxBaum) IsConjunction() bool {
-	return tree.kind == "and" || tree.kind == "and2"
-}
-
-func (tree SyntaxBaum) IsDisjunction2() bool {
-	return tree.kind == "or2"
-}
-
-func (tree SyntaxBaum) IsDisjunction() bool {
-	return tree.kind == "or" || tree.kind == "or2"
-}
-
-func (tree SyntaxBaum) IsImplication() bool {
-	return tree.kind == "implies"
-}
diff --git a/codego/core/utils/utils.go b/codego/core/utils/utils.go
index 0bc8cd5..b9f2206 100644
--- a/codego/core/utils/utils.go
+++ b/codego/core/utils/utils.go
@@ -131,7 +131,7 @@ func UnionStrings2(list1 []string, list2 []string) []string {
 }
 
 // assumes that listTo contains no duplicates
-func UnionStringsTo(listTo *[]string, listFrom []string) {
+func UnionStringsInPlace(listTo *[]string, listFrom []string) {
 	var mark = make(map[string]bool)
 	for _, item := range listFrom {
 		mark[item] = true
@@ -149,7 +149,7 @@ func UnionStringsTo(listTo *[]string, listFrom []string) {
 func UnionStringsList(lists [][]string) []string {
 	var list = []string{}
 	for _, list_ := range lists {
-		UnionStringsTo(&list, list_)
+		UnionStringsInPlace(&list, list_)
 	}
 	return list
 }
diff --git a/codego/core/utils/utils_test.go b/codego/core/utils/utils_test.go
index 6232852..1dfcd97 100644
--- a/codego/core/utils/utils_test.go
+++ b/codego/core/utils/utils_test.go
@@ -89,7 +89,7 @@ func TestFilterStrings(test *testing.T) {
 }
 
 /* ---------------------------------------------------------------- *
- * TESTCASE UnionStrings2, UnionStringsTo, UnionStringsList
+ * TESTCASE UnionStrings2, UnionStringsInPlace, UnionStringsList
  * ---------------------------------------------------------------- */
 
 func TestUnionStrings2(test *testing.T) {
@@ -101,11 +101,11 @@ func TestUnionStrings2(test *testing.T) {
 	assert.Equal([]string{"black", "blue", "green", "grey", "lila", "orange", "red", "yellow"}, list)
 }
 
-func TestUnionStringsTo(test *testing.T) {
+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.UnionStringsTo(&list1, list2)
+	utils.UnionStringsInPlace(&list1, list2)
 	utils.SortStrings(&list1)
 	assert.Equal([]string{"black", "blue", "green", "red", "yellow"}, list1)
 }
diff --git a/codego/main.go b/codego/main.go
index 5b1a015..b09be3b 100644
--- a/codego/main.go
+++ b/codego/main.go
@@ -2,9 +2,9 @@ package main
 
 import (
 	"fmt"
-	"logik/aussagenlogik/rekursion"
+	"logik/aussagenlogik/formulae"
+	"logik/aussagenlogik/recursion"
 	"logik/aussagenlogik/schema"
-	"logik/aussagenlogik/syntaxbaum"
 	env "logik/core/environment"
 	"logik/core/utils"
 	"strings"
@@ -21,6 +21,7 @@ type dataType struct {
 
 type resultsType struct {
 	eval         int
+	nnf          formulae.Formula
 	atoms        []string
 	depth        int
 	length       int
@@ -50,28 +51,18 @@ func getData() {
 	utils.JsonToArrayOfStrings(s, &data.interpretation)
 }
 
-func getResults(tree syntaxbaum.SyntaxBaum) resultsType {
-	ch1 := make(chan int)
-	ch2 := make(chan []string)
-	ch3 := make(chan int)
-	ch4 := make(chan int)
-	ch5 := make(chan int)
-	go rekursion.RekursivEval(ch1, tree, data.interpretation)
-	go rekursion.RekursivAtoms(ch2, tree)
-	go rekursion.RekursivDepth(ch3, tree)
-	go rekursion.RekursivLength(ch4, tree)
-	go rekursion.RekursivParentheses(ch5, tree)
-	// Methoden ausführen:
+func getResults(tree formulae.Formula) resultsType {
 	return resultsType{
-		eval:         <-ch1,
-		atoms:        <-ch2,
-		depth:        <-ch3,
-		length:       <-ch4,
-		nParentheses: <-ch5,
+		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 syntaxbaum.SyntaxBaum, results resultsType) {
+func displayResults(tree formulae.Formula, results resultsType) {
 	fmt.Println(fmt.Sprintf(
 		dedent.Dedent(`
 		Syntaxbaum von
@@ -81,10 +72,11 @@ func displayResults(tree syntaxbaum.SyntaxBaum, results resultsType) {
 
 		Für I = {%[3]s} und F wie oben gilt
 		eval(F, I)      = %[4]d;
-		atoms(F)        = {%[5]s};  <- *
-		depth(F)        = %[6]d;  <- *
-		length(F)       = %[7]d;  <- *
-		#parentheses(F) = %[8]d;  <- *
+		F^NNF           = %[5]s;
+		atoms(F)        = {%[6]s};  <- *
+		depth(F)        = %[7]d;  <- *
+		length(F)       = %[8]d;  <- *
+		#parentheses(F) = %[9]d;  <- *
 
 		* noch nicht implementiert!
 		Challenge: schreibe diese Methoden! (siehe README.md)
@@ -93,6 +85,7 @@ func displayResults(tree syntaxbaum.SyntaxBaum, results resultsType) {
 		tree.Pretty("    "),
 		strings.Join(data.interpretation, ", "),
 		results.eval,
+		results.nnf.GetExpr(),
 		// string(results.atoms),
 		strings.Join(results.atoms, ", "),
 		results.depth,