diff --git a/codego/aussagenlogik/formulae/formulae.go b/codego/aussagenlogik/formulae/formulae.go
deleted file mode 100644
index e4a9f2e..0000000
--- a/codego/aussagenlogik/formulae/formulae.go
+++ /dev/null
@@ -1,283 +0,0 @@
-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_basic.go b/codego/aussagenlogik/formulae/formulae_basic.go
new file mode 100644
index 0000000..3085c8a
--- /dev/null
+++ b/codego/aussagenlogik/formulae/formulae_basic.go
@@ -0,0 +1,119 @@
+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: 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_construction.go b/codego/aussagenlogik/formulae/formulae_construction.go
new file mode 100644
index 0000000..1074d32
--- /dev/null
+++ b/codego/aussagenlogik/formulae/formulae_construction.go
@@ -0,0 +1,117 @@
+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(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},
+	}
+}
diff --git a/codego/aussagenlogik/formulae/formulae_types.go b/codego/aussagenlogik/formulae/formulae_pairs.go
similarity index 100%
rename from codego/aussagenlogik/formulae/formulae_types.go
rename to codego/aussagenlogik/formulae/formulae_pairs.go