diff --git a/documents/Programmierparadigmen/Lambda.tex b/documents/Programmierparadigmen/Lambda.tex
index feabfeb..f0e823c 100644
--- a/documents/Programmierparadigmen/Lambda.tex
+++ b/documents/Programmierparadigmen/Lambda.tex
@@ -294,6 +294,75 @@ Insbesondere ist also $f \ g$ ein Fixpunkt von $g$.
     $\qed$
 \end{beweis}
 
+\section{Let-Polymorphismus}\xindex{let-Polymorphismus}\footnote{WS 2013 / 2014, Folie 205ff}%
+Das Programm $P = \text{let } f = \lambda x.\ 2 \text{ in } f\ (f\ \text{\texttt{true}})$
+ist eine polymorphe Hilfsfunktion, da sie beliebige Werte auf 2 Abbildet.
+Auch solche Ausdrücke sollen typisierbar sein.
 
+Die Kodierung 
+\[\text{let} x = t_1 \text{ in } t_2\]
+ist bedeutungsgleich mit
+\[(\lambda x.\ t_2) t_1\]
 
-Für den Turing-Operator gilt 
\ No newline at end of file
+Das Problem ist, dass 
+\[P = \lambda f. \ f (f\ \text{\texttt{true}})\ (\lambda x.\ 2)\]
+so nicht typisierbar ist, da in
+\[\ABS \frac{f: \tau_f \vdash f\ (f\ \text{\texttt{true}}): \dots}{\vdash \lambda f.\ f\ (f\ \text{\texttt{true}}): \dots}\]
+müsste 
+\[\tau_f = \text{bool} \rightarrow \text{int}\]
+und zugleich
+\[\tau_f = \text{int} \rightarrow \text{int}\]
+in den Typkontext eingetragen werden. Dies ist jedoch nicht möglich. Stattdessen
+wird 
+\[\text{let} x = t_1 \text{ in } t_2\]
+als neues Konstrukt im $\lambda$-Kalkül erlaubt.
+
+\begin{definition}[Typschema]\xindex{Typschema}%
+    Ein Typ der Gestalt $\forall \alpha_1.\ \forall \alpha_2.\ \dots\ \forall \alpha_n. \tau$
+    heißt \textbf{Typschema}. Es bindet freie Variablen $\alpha_1, \dots, \alpha_n$
+    in $\tau$.
+\end{definition}
+
+\begin{beispiel}[Typschema]
+    Das Typschema $\forall \alpha.\ \alpha \rightarrow \alpha$ steht für unendlich
+    viele Typen und insbesondere für folgende:
+    \begin{bspenum}
+        \item int $\rightarrow$ int, bool $\rightarrow$ bool, \dots
+        \item (int $\rightarrow$ int) $\rightarrow$ (int $\rightarrow$ int), \dots
+        \item \dots
+    \end{bspenum}
+\end{beispiel}
+
+\begin{definition}[Typschemainstanziierung]\xindex{Typschemainstanziierung}%
+    Sei $\tau_2$ ein Nicht-Schema-Typ. Dann heißt der Typ
+    \[\tau[\alpha \mapsto \tau_2]\]
+    eine \textbf{Instanziierung} vom Typschema $\forall \alpha.\ \tau$
+    und man schreibt:
+    \[(\forall \alpha.\ \tau) \succeq \tau [\alpha \mapsto \tau_2]\]
+\end{definition}
+
+\begin{beispiel}[Typschemainstanziierung]
+    Folgendes sind Beispiele für Typschemainstanziierungen:
+    \begin{bspenum}
+        \item $\forall \alpha.\ \alpha \rightarrow \alpha \succeq \text{int} \rightarrow \text{int}$
+        \item $\forall \alpha.\ \alpha \rightarrow \alpha \succeq (\text{int} \rightarrow \text{int}) \rightarrow (\text{int} \rightarrow \text{int})$
+        \item $\text{int} \succeq \text{int}$
+    \end{bspenum}
+
+    Folgendes sind keine Typschemainstanziierungen:
+    \begin{bspenum}
+        \item $\alpha \rightarrow \alpha \nsucceq \text{int} \rightarrow \text{int}$
+        \item $\alpha \nsucceq \text{bool}$
+        \item $\forall \alpha.\ \alpha \rightarrow \alpha \nsucceq \text{bool}$
+    \end{bspenum}
+\end{beispiel}
+
+Zu Typschemata gibt es angepasste Regeln:
+
+\[\VAR \frac{\Gamma(x)= \tau' \;\;\; \tau' \succeq \tau}{\gamma \vdash x: \tau}\]
+
+und
+
+\[\ABS \frac{\Gamma, x: \tau_1 \vdash t: \tau_2 \;\;\; \tau_1 \text{ kein Typschema}}{\Gamma \vdash  \lambda x. t: \tau_1 \rightarrow \tau_2}\]
+
+\todo[inline]{Folie 208ff}
\ No newline at end of file
diff --git a/documents/Programmierparadigmen/Programmierparadigmen.pdf b/documents/Programmierparadigmen/Programmierparadigmen.pdf
index c484e39..4da5baa 100644
Binary files a/documents/Programmierparadigmen/Programmierparadigmen.pdf and b/documents/Programmierparadigmen/Programmierparadigmen.pdf differ
diff --git a/documents/Programmierparadigmen/Programmiersprachen.tex b/documents/Programmierparadigmen/Programmiersprachen.tex
index 5d319c1..46e7831 100644
--- a/documents/Programmierparadigmen/Programmiersprachen.tex
+++ b/documents/Programmierparadigmen/Programmiersprachen.tex
@@ -136,13 +136,20 @@ Programmiersprachen können anhand der Art ihrer Typisierung unterschieden werde
 \end{beispiel}
 
 \begin{definition}[Polymorphie]\xindex{Polymorphie}%
-    Ein Typ heißt \textbf{polymorph}, wenn er mindestens einen Parameter hat.
+    \begin{defenum}
+        \item Ein Typ heißt polymorph, wenn er mindestens einen Parameter hat.
+        \item Eine Funktion heißt polymorph, wenn ihr Verhalten nicht von dem
+              konkreten Typen der Parameter abhängt.
+    \end{defenum}
 \end{definition}
 
 \begin{beispiel}[Polymorphie]
-    In Java sind beispielsweise Listen polymorph:
+    In Java sind beispielsweise Listen polymorphe Typen:
 
     \inputminted[numbersep=5pt, tabsize=4]{java}{scripts/java/list-example.java}
+
+    Entsprechend sind auf Listen polymorphe Operationen wie \texttt{add} und
+    \texttt{remove} definiert.
 \end{beispiel}
 
 \begin{definition}[Statische und dynamische Typisierung]\xindex{Typisierung!statische}\xindex{Typisierung!dynamische}%
diff --git a/documents/Programmierparadigmen/Prolog.tex b/documents/Programmierparadigmen/Prolog.tex
index e8c0bff..6409544 100644
--- a/documents/Programmierparadigmen/Prolog.tex
+++ b/documents/Programmierparadigmen/Prolog.tex
@@ -16,6 +16,24 @@ Kompiliere ihn mit \texttt{gplc hello-world.pl}. Es wird eine
 ausführbare Datei erzeugt.
 
 \section{Syntax}
+In Prolog gibt es Prädikate, die Werte haben. Prädikate werden immer klein geschrieben.
+So kann das Prädikat \texttt{farbe} mit den Werten \texttt{rot}, \texttt{gruen},
+\texttt{blau}, \texttt{gelb} - welche auch immer klein geschrieben werden - wie 
+folgt definiert werden:
+
+\inputminted[numbersep=5pt, tabsize=4]{prolog}{scripts/prolog/praedikat-farbe.pl}
+
+\begin{itemize}
+    \item Terme werden durch \texttt{,} mit einem logischem \textbf{und} verknüpft.
+    \item Ungleichheit wird durch \texttt{\=} ausgedrückt.
+\end{itemize}
+
+So ist folgendes Prädikat \texttt{nachbar(X, Y)} genau dann wahr, wenn $X$
+und $Y$ Farben sind und $X \neq Y$ gilt:
+
+\inputminted[numbersep=5pt, tabsize=4]{prolog}{scripts/prolog/simple-term.pl}
+
+
 \section{Beispiele}
 \subsection{Humans}
 Erstelle folgende Datei:
diff --git a/documents/Programmierparadigmen/Symbolverzeichnis.tex b/documents/Programmierparadigmen/Symbolverzeichnis.tex
index a037df1..dff1d55 100644
--- a/documents/Programmierparadigmen/Symbolverzeichnis.tex
+++ b/documents/Programmierparadigmen/Symbolverzeichnis.tex
@@ -45,6 +45,7 @@ $\psi \vdash \varphi$        & Syntaktische Herleitbarkeit\newline Die Formel $\
 \setlength\mylengthb{\dimexpr\columnwidth-\mylengtha-2\tabcolsep\relax}
 
 \begin{xtabular}{@{} p{\mylengtha} P{\mylengthb} @{}}
-$\bot$  & Bottom\\
-$\Parr$ & TODO?
+$\bot$   & Bottom\\
+$\Parr$  & TODO?\\
+$\succeq$& Typschemainstanziierung\\
 \end{xtabular}
\ No newline at end of file
diff --git a/documents/Programmierparadigmen/scripts/prolog/dl-faerbbarkeit b/documents/Programmierparadigmen/scripts/prolog/dl-faerbbarkeit
new file mode 100755
index 0000000..ba7edbd
Binary files /dev/null and b/documents/Programmierparadigmen/scripts/prolog/dl-faerbbarkeit differ
diff --git a/documents/Programmierparadigmen/scripts/prolog/dl-faerbbarkeit.pl b/documents/Programmierparadigmen/scripts/prolog/dl-faerbbarkeit.pl
new file mode 100644
index 0000000..da5c687
--- /dev/null
+++ b/documents/Programmierparadigmen/scripts/prolog/dl-faerbbarkeit.pl
@@ -0,0 +1,18 @@
+farbe(blau).
+farbe(gelb).
+farbe(gruen).
+nachbar(X, Y) :- farbe(X), farbe(Y), X \= Y.
+deutschland(SH,MV,HH,HB,NI,ST,BE,BB,SN,NW,HE,TH,RP,SL,BW,BY) :-
+nachbar(SH, NI), nachbar(SH, HH), nachbar(SH, MV),
+nachbar(HH, NI),
+nachbar(MV, NI), nachbar(MV, BB),
+nachbar(NI, HB), nachbar(NI, BB), nachbar(NI, ST), nachbar(NI, TH),
+nachbar(NI, HE), nachbar(NI, NW),
+nachbar(ST, BB), nachbar(ST, SN), nachbar(ST, TH),
+nachbar(BB, BE), nachbar(BB, SN),
+nachbar(NW, HE), nachbar(NW, RP),
+nachbar(SN, TH), nachbar(SN, BY),
+nachbar(RP, SL), nachbar(RP, HE), nachbar(RP, BW),
+nachbar(HE, BW), nachbar(HE, TH), nachbar(HE, BY),
+nachbar(TH, BY),
+nachbar(BW, BY).
\ No newline at end of file
diff --git a/documents/Programmierparadigmen/scripts/prolog/hello-world.pl b/documents/Programmierparadigmen/scripts/prolog/hello-world.pl
index b070ba0..9608394 100644
--- a/documents/Programmierparadigmen/scripts/prolog/hello-world.pl
+++ b/documents/Programmierparadigmen/scripts/prolog/hello-world.pl
@@ -1,2 +1,2 @@
 :- initialization(main).
-main :- write('Hello World!'), nl, halt.
+main :- write('Hello World!'), nl, halt.
\ No newline at end of file
diff --git a/documents/Programmierparadigmen/scripts/prolog/praedikat-farbe.pl b/documents/Programmierparadigmen/scripts/prolog/praedikat-farbe.pl
new file mode 100644
index 0000000..6ea8ba7
--- /dev/null
+++ b/documents/Programmierparadigmen/scripts/prolog/praedikat-farbe.pl
@@ -0,0 +1,4 @@
+farbe(blau).
+farbe(gelb).
+farbe(gruen).
+farbe(rot).
\ No newline at end of file
diff --git a/documents/Programmierparadigmen/scripts/prolog/simple-term.pl b/documents/Programmierparadigmen/scripts/prolog/simple-term.pl
new file mode 100644
index 0000000..2e70dc4
--- /dev/null
+++ b/documents/Programmierparadigmen/scripts/prolog/simple-term.pl
@@ -0,0 +1 @@
+nachbar(X, Y) :- farbe(X), farbe(Y), X \= Y.
\ No newline at end of file