diff --git a/Vorlesungen/lecture-01.tex b/Vorlesungen/lecture-01.tex
index 12e73bf..c7fd346 100644
--- a/Vorlesungen/lecture-01.tex
+++ b/Vorlesungen/lecture-01.tex
@@ -67,7 +67,7 @@
 
 \begin{frame}\frametitle{Prüfung und Prüfungsvorbereitung}
 \begin{itemize}
-\item schritliche Prüfung (90min) am Ende des Sommersemesters, vermutlich online
+\item schriftliche Prüfung (90min) am Ende des Sommersemesters, vermutlich online
 \item prüfungsrelevant:\\
 	kompletter Stoff aus Vorlesung \alert{und} Übung;\\
 	Wiedergeben (Definieren), Anwenden (Rechnen) und Erklären (Beweisen)
@@ -223,7 +223,7 @@
 \begin{itemize}
 \item Was heißt "`berechnen"'?
 \item Welche Probleme kann man auf reellen Computern lösen?
-\item Was wäre wenn wir mächtigere Computer hätten?
+\item Was wäre, wenn wir mächtigere Computer hätten?
 \item Was macht Rechenprobleme "`schwer"' oder "`einfach"'?
 \item Sind alternative Rechenmodelle denkbar?
 \item Welche (mathematischen/physikalischen/biologischen) Systeme können sonst noch rechnen?
@@ -479,7 +479,7 @@
 geschrieben als Wort (Bandinhalt), in dem der Zustand vor der Position des Kopfes eingefügt ist
 \bigskip
 
-\redalert{Übergangsrelation:} Beziehung zwischen zwei Konfigurationen wenn die TM von der ersten in die zweite übergehen kann (deterministisch oder nichtdeterministisch); geschrieben als $\vdash$
+\redalert{Übergangsrelation:} Beziehung zwischen zwei Konfigurationen, wenn die TM von der ersten in die zweite übergehen kann (deterministisch oder nichtdeterministisch); geschrieben als $\vdash$
 \bigskip
 
 \redalert{Lauf:} mögliche Abfolge von Konfigurationen einer TM, beginnend mit der Startkonfiguration; kann endlich oder unendlich sein
@@ -495,7 +495,7 @@
 
 \begin{enumerate}[(1)]
 \item \alert{Transducer:} Ausgabe der TM ist der Inhalt des Bandes, wenn sie hält, oder undefiniert, wenn sie nicht hält (partielle Funktion); Endzustände spielen keine Rolle und können weggelassen werden
-\item \alert{Entscheider:} Ausgabe der TM hat nur zwei Werte: die TM "`akzeptiert"', wenn sie in einem Endzustand hält und sie "`verwirft"' wenn sie in einem Nicht-Endzustand oder gar nicht hält;
+\item \alert{Entscheider:} Ausgabe der TM hat nur zwei Werte: die TM "`akzeptiert"', wenn sie in einem Endzustand hält und sie "`verwirft"' wenn sie in einem Nichtendzustand oder gar nicht hält;
 Bandinhalt beim Halten spielt keine Rolle und kann ignoriert werden
 \end{enumerate}
 
@@ -507,12 +507,12 @@
 
 Wir wissen: {\tiny(aus "`Formale Systeme"', Winter 2020/2021, 19. Vorlesung)}
 
-\theobox{\textbf{Satz:} Jede NTM kann durch eine DTM simuliert werden. Insbesondere akzeptieren deterministische und nichtdeterministische Turingmaschinen die selben Sprachen.}
+\theobox{\emph{Satz:} Jede NTM kann durch eine DTM simuliert werden. Insbesondere akzeptieren deterministische und nichtdeterministische Turingmaschinen dieselben Sprachen.}
 \pause
 
 Allgemeiner gilt: kein bekanntes Berechnungsmodell kann mehr berechnen als TMs
 
-\anybox{purple}{\textbf{Church-Turing-These:} Jede (partielle) Funktion, die intuitiv als berechenbar angesehen werden kann, ist auch mit einer Turingmaschine berechenbar.}
+\anybox{purple}{\emph{Church-Turing-These:} Jede (partielle) Funktion, die intuitiv als berechenbar angesehen werden kann, ist auch mit einer Turingmaschine berechenbar.}
 
 \begin{itemize}
 \item \emph{Lesart 1:} Vorschlag einer mathematischen Definition der intuitiven Idee von Berechenbarkeit
@@ -533,11 +533,11 @@
 \bigskip
 
 \anybox{yellow}{
-Was erwartet uns als nächstes?
+Was erwartet uns als Nächstes?
 \begin{itemize}
 \item Probleme
 \item Paradoxien
-\item Phenomenal große Zahlen
+\item Phänomenal große Zahlen
 \end{itemize}
 }
 
diff --git a/Vorlesungen/lecture-02.tex b/Vorlesungen/lecture-02.tex
index 7629386..341d6f0 100644
--- a/Vorlesungen/lecture-02.tex
+++ b/Vorlesungen/lecture-02.tex
@@ -47,9 +47,9 @@
 	Die Eingabe wird auf das erste Band geschrieben.
 \end{itemize}
 
-\theobox{Satz: Deterministische und nichtdeterministische Turingmaschinen mit einer beliebigen Anzahl von Bändern können die gleichen Berechnungen ausführen.}
+\theobox{\emph{Satz:} Deterministische und nichtdeterministische Turingmaschinen mit einer beliebigen Anzahl von Bändern können die gleichen Berechnungen ausführen.}
 
-Details siehe Vorlesung Formale Systeme (Winter 2017/2018, Vorlesungen 18 und 19)
+Details siehe Vorlesung Formale Systeme (Winter 2020/2021, Vorlesungen 18 und 19)
 
 \end{frame}
 
@@ -78,7 +78,7 @@
 Eine Turingmaschine kann eine Funktion von Eingabewörtern auf Ausgabewörter definieren:\medskip
 
 \defbox{Eine DTM $\Smach{M}$ \redalert{berechnet} eine partielle Funktion $f_{\Smach{M}}:\Sigma^*\to\Sigma^*$ wie folgt.
-Für ein Wort $w\in\Sigma^*$ ist $f_{\Smach{M}}(w)=v$ wenn $\Smach{M}$ bei Eingabe $w$ mit einem Band anhält, auf dem 
+Für ein Wort $w\in\Sigma^*$ ist $f_{\Smach{M}}(w)=v$, wenn $\Smach{M}$ bei Eingabe $w$ mit einem Band anhält, auf dem 
 nur $v$ steht, d.h., wenn der Bandinhalt nach dem Halten die Form $v\blank\blank\blank\cdots$ hat.}\pause
 
 Es gibt also zwei Fälle, in denen $f_{\Smach{M}}(w)$ undefiniert ist:
@@ -122,7 +122,7 @@
 %
 Die \redalert{durch $\Smach{M}$ aufgezählte Sprache} ist die Menge aller Wörter
 aus $\Sigma^*$, die $\Smach{M}$ ausgibt, wenn $\Smach{M}$ auf dem leeren Band gestartet wird.\\
-{\tiny(Anmerkung: Die Definition erlaubt die Ausgabe von Wörtern aus $\Gamma^*\setminus\Sigma^*$. Diese gehören für uns nicht zur aufgezählten Sprache.}
+{\tiny(Anmerkung: Die Definition erlaubt die Ausgabe von Wörtern aus $\Gamma^*\setminus\Sigma^*$. Diese gehören für uns nicht zur aufgezählten Sprache.)}
 }\bigskip
 
 Die durch $\Smach{M}$ aufgezählte Sprache kann unendlich sein, wenn $\Smach{M}$ auf der leeren Eingabe nicht hält.
@@ -161,7 +161,7 @@
 
 \begin{frame}[t]\frametitle{Aufzählbar = semi-entscheidbar (1)}
 
-\theobox{Satz: Eine Sprache $\Slang{L}$ ist genau dann semi-entscheidbar, wenn es
+\theobox{\emph{Satz:} Eine Sprache $\Slang{L}$ ist genau dann semi-entscheidbar, wenn es
 einen Aufzähler für $\Slang{L}$ gibt.
 }\pause
 
@@ -178,7 +178,7 @@
 
 \begin{frame}[t]\frametitle{Aufzählbar = semi-entscheidbar (2)}
 
-\theobox{Satz: Eine Sprache $\Slang{L}$ ist genau dann semi-entscheidbar, wenn es
+\theobox{\emph{Satz:} Eine Sprache $\Slang{L}$ ist genau dann semi-entscheidbar, wenn es
 einen Aufzähler für $\Slang{L}$ gibt.
 }\pause
 
@@ -211,7 +211,7 @@
 \item \alert{Tupel} (Listen) von Wörtern (oder natürlichen Zahlen, \ldots), können kodiert werden, indem man zum Eingabealphabet ein zusätzliches Trennzeichen $\Sterm{\#}$ hinzufügt
 \end{itemize}\bigskip\pause
 
-\examplebox{Beispiel: Mithilfe dieser Kodierungen können wir z.B. von berechenbaren Funktionen $\mathbb{N}\to\mathbb{N}$ oder von
+\examplebox{\emph{Beispiel:} Mithilfe dieser Kodierungen können wir z.B. von berechenbaren Funktionen $\mathbb{N}\to\mathbb{N}$ oder von
 semi-entscheidbaren Teilmengen von $\mathbb{N}\times\mathbb{N}$ sprechen.}\medskip
 
 Anmerkung: Oft gibt es viele denkbare Kodierungen eines Objektes als Wort. Vorerst sollen uns die Details nicht interessieren, solange klar ist, dass eine TM die Kodierung entschlüsseln kann.
@@ -224,14 +224,14 @@
 
 Berechenbarkeit von Funktionen und Sprachen sind eng verwandt.
 
-\theobox{Satz: Eine Sprache $\Slang{L}$ ist genau dann entscheidbar, wenn die folgende Funktion $f:\Sigma^*\to\Sigma^*$ berechenbar ist (o.B.d.A. sei $\{\Sterm{0},\Sterm{1}\}\subseteq\Sigma$):
+\theobox{\emph{Satz:} Eine Sprache $\Slang{L}$ ist genau dann entscheidbar, wenn die folgende Funktion $f:\Sigma^*\to\Sigma^*$ berechenbar ist (o.B.d.A. sei $\{\Sterm{0},\Sterm{1}\}\subseteq\Sigma$):
 \[f(w)= \left\{\begin{array}{ll}
 \Sterm{1} & \text{falls $w\in\Slang{L}$}\\
 \Sterm{0} & \text{falls $w\notin\Slang{L}$}\\
 \end{array}\right.\]}\pause
 
 {\footnotesize
-\emph{Beweisskizze:} "`$\Rightarrow$"' Ein Entscheider für $\Slang{L}$ kann in eine TM für $f$ umgebaut werden. Dazu verwendet man "`Subroutinen"', die den Bandinhalt löschen und mit einem einzelnen Zeichen \Sterm{1} oder \Sterm{0} ersetzten. Diese Routinen werden aufgerufen, wenn der ursprüngliche Entscheider halten würde: die \Sterm{1}-Routine beim Halten in einem Endzustand, die \Sterm{0}-Routine andernfalls.\medskip
+\emph{Beweisskizze:} "`$\Rightarrow$"' Ein Entscheider für $\Slang{L}$ kann in eine TM für $f$ umgebaut werden. Dazu verwendet man "`Subroutinen"', die den Bandinhalt löschen und mit einem einzelnen Zeichen \Sterm{1} oder \Sterm{0} ersetzen. Diese Routinen werden aufgerufen, wenn der ursprüngliche Entscheider halten würde: die \Sterm{1}-Routine beim Halten in einem Endzustand, die \Sterm{0}-Routine andernfalls.\medskip
 
 {\tiny Eventuell muss man den Entscheider außerdem so modifizieren, dass das
 Zeichen $\blank$ nur am Ende des verwendeten Bandinhaltes vorkommen kann (sonst wird das Löschen des gesamten Bandes problematisch!).
@@ -239,7 +239,7 @@
 }
 \smallskip
 
-"`$\Leftarrow$"' Eine TM, die $f$ berechnet, kann in einen Entscheider für $\Slang{L}$ umgebaut werden. Die Idee ist wie zuvor, aber die Subroutinen prüfen jetzt, ob das Band \Sterm{1} oder \Sterm{0} enthält und wechseln entsprechend in einen akzeptierenden oder nicht-akzeptierenden Zustand.\qed
+"`$\Leftarrow$"' Eine TM, die $f$ berechnet, kann in einen Entscheider für $\Slang{L}$ umgebaut werden. Die Idee ist wie zuvor, aber die Subroutinen prüfen jetzt, ob das Band \Sterm{1} oder \Sterm{0} enthält und wechseln entsprechend in einen akzeptierenden oder nichtakzeptierenden Zustand.\qed
 
 }
 
@@ -249,7 +249,7 @@
 
 Für die Umkehrung stellen wir Funktionen als Mengen dar:
 
-\theobox{Satz: Eine partielle Funktion $f$ ist genau dann berechenbar, wenn die Sprache
+\theobox{\emph{Satz:} Eine partielle Funktion $f$ ist genau dann berechenbar, wenn die Sprache
 \[\textsf{Graph}_f=\{\tuple{w,f(w)}\mid w\in\Sigma^*,\; f(w)\text{ definiert}\}\] semi-entscheidbar ist.
 Ist $f$ total, dann ist $\textsf{Graph}_f$ sogar entscheidbar.}
 
@@ -270,7 +270,7 @@
 
 Für die Umkehrung stellen wir Funktionen als Mengen dar:
 
-\theobox{Satz: Eine partielle Funktion $f$ ist genau dann berechenbar, wenn die Sprache
+\theobox{\emph{Satz:} Eine partielle Funktion $f$ ist genau dann berechenbar, wenn die Sprache
 \[\textsf{Graph}_f=\{\tuple{w,f(w)}\mid w\in\Sigma^*,\; f(w)\text{ definiert}\}\] semi-entscheidbar ist.
 Ist $f$ total, dann ist $\textsf{Graph}_f$ sogar entscheidbar.}\pause
 
@@ -297,7 +297,7 @@
 
 \begin{frame}\frametitle{Es gibt unentscheidbare Probleme}
 
-\theobox{Satz: Es gibt Sprachen und Funktionen, die nicht berechenbar sind.}
+\theobox{\emph{Satz:} Es gibt Sprachen und Funktionen, die nicht berechenbar sind.}
 
 \pause
 Dies kann man wie folgt zeigen:
@@ -369,7 +369,7 @@
  \visible<2->{\Slangsub{L}{d} & - & - & \times & \ldots & }
 \end{array}\]\pause
 \item Wir konstruieren eine Sprache $\Slangsub{L}{d}$ durch \alert{Diagonalisierung}.\\
-Formal: $w_i\in \Slangsub{L}{d}$ genau dann wenn $w_i\notin\Slangsub{L}{i}$.\pause
+Formal: $w_i\in \Slangsub{L}{d}$ genau dann, wenn $w_i\notin\Slangsub{L}{i}$.\pause
 \end{itemize}
 Dann kommt $\Slangsub{L}{d}$ in der Tabelle nicht vor. Widerspruch.
 
@@ -382,7 +382,7 @@
 
 Es reicht nicht aus, dass wir nicht wissen, wie ein Problem algorithmisch gelöst werden kann!\bigskip
 
-\examplebox{Beispiel: Sei $\Slang{L}_\pi$ die Menge aller endlichen Ziffernfolgen, die in der Dezimaldarstellung von $\pi$ vorkommen. Zum Beispiel gilt $\Sterm{14159265}\in\Slang{L}_\pi$ und $\Sterm{41}\in\Slang{L}_\pi$. \\[1ex]
+\examplebox{\emph{Beispiel:} Sei $\Slang{L}_\pi$ die Menge aller endlichen Ziffernfolgen, die in der Dezimaldarstellung von $\pi$ vorkommen. Zum Beispiel gilt $\Sterm{14159265}\in\Slang{L}_\pi$ und $\Sterm{41}\in\Slang{L}_\pi$. \\[1ex]
 
 \only<3->{%
 Wir wissen nicht, ob man die Sprache $\Slang{L}_\pi$ entscheiden kann, aber sie könnte dennoch entscheidbar sein (z.B. wenn jede endliche Ziffernfolge irgendwo in $\pi$ vorkommt, was aber bisher nicht bekannt ist).}}
@@ -394,7 +394,7 @@
 Es gibt sogar Fälle, in denen wir sicher sind, dass ein Problem entscheidbar ist,
 aber trotzdem nicht wissen, wie man es löst.\\[1.5ex]\pause
 
-\examplebox{Beispiel: Sei $\Slang{L}_{\pi7}$ die Menge aller Ziffernfolgen der Form $\Sterm{7}^n$, die in der Dezimaldarstellung von $\pi$ vorkommen.\\[1ex]
+\examplebox{\emph{Beispiel:} Sei $\Slang{L}_{\pi7}$ die Menge aller Ziffernfolgen der Form $\Sterm{7}^n$, die in der Dezimaldarstellung von $\pi$ vorkommen.\\[1ex]
 
 \only<3->{
 $\Slang{L}_{\pi7}$ ist entscheidbar:
@@ -422,7 +422,7 @@
 
 \begin{frame}[t]\frametitle{Ein erstes unentscheidbares Problem (2)}
 
-\emph{Frage:} Falls eine TM \alert{mit $n$ Zuständen} und \alert{einem zwei-elementigen Arbeitsalphabet $\Gamma=\{\Sterm{x}, \blank\}$} auf einem \alert{leeren Band} anhält, wie lange kann das im schlimmsten Fall dauern?\\
+\emph{Frage:} Falls eine TM \alert{mit $n$ Zuständen} und \alert{einem zweielementigen Arbeitsalphabet $\Gamma=\{\Sterm{x}, \blank\}$} auf einem \alert{leeren Band} anhält, wie lange kann das im schlimmsten Fall dauern?\\
 \bigskip\pause
 
 \emph{Antwort:} Das kommt auf $n$ an \ldots\bigskip\pause
@@ -484,7 +484,7 @@
 
 % Wie schwer kann das schon sein \ldots?\pause
 
-\theobox{Satz: Die Busy-Beaver-Funktion ist nicht berechenbar.}
+\theobox{\emph{Satz:} Die Busy-Beaver-Funktion ist nicht berechenbar.}
 
 \pause
 \emph{Beweisskizze:} Nehmen wir an, $\bbfunc$ wäre berechenbar.\pause
@@ -578,7 +578,7 @@
 \bigskip
 
 \anybox{yellow}{
-Was erwartet uns als nächstes?
+Was erwartet uns als Nächstes?
 \begin{itemize}
 \item Relevantere Probleme
 \item Reduktionen
diff --git a/Vorlesungen/lecture-03.tex b/Vorlesungen/lecture-03.tex
index 91c0679..dbef2ce 100644
--- a/Vorlesungen/lecture-03.tex
+++ b/Vorlesungen/lecture-03.tex
@@ -256,7 +256,7 @@
 
 \end{frame}
 
-\begin{frame}\frametitle{LOOP-Berechenbare Funktionen}
+\begin{frame}\frametitle{LOOP-berechenbare Funktionen}
 
 \defbox{\emph{Definition:} Eine Funktion $\mathbb{N}^k\to\mathbb{N}$ heißt \redalert{LOOP-berechenbar}, wenn es ein LOOP-Programm gibt, das die Funktion berechnet.}\bigskip
 \pause
@@ -301,7 +301,7 @@
 
 Das ist weniger überraschend, als es vielleicht klingt:\smallskip
 
-\emph{Beweis:} Ein LOOP-Programm terminiert immer. Daher ist jede LOOP-berechenbare Funktion total. Es gibt aber auch nicht-totale Funktionen, die berechenbar sind (z.B. die ``partiellste'' Funktion, die nirgends definiert ist).\qed
+\emph{Beweis:} Ein LOOP-Programm terminiert immer. Daher ist jede LOOP-berechenbare Funktion total. Es gibt aber auch nichttotale Funktionen, die berechenbar sind (z.B. die ``partiellste'' Funktion, die nirgends definiert ist).\qed
 % \bigskip\pause
 % 
 % \theobox{Satz: Es gibt berechenbare totale Funktionen, die nicht LOOP-berechenbar sind.}\pause
@@ -346,7 +346,7 @@
 \end{itemize}\bigskip\pause
 
 \defbox{\emph{Definition:} Die Funktion $\bbfunc_{\textsf{LOOP}}:\mathbb{N}\to\mathbb{N}$ liefert für jede Zahl $\ell$ die größte Zahl $\bbfunc_{\textsf{LOOP}}(\ell)$, die ein LOOP-Programm der Länge $\leq\ell$ für eine leere Eingabe (alle Variablen sind $0$) ausgibt. Dabei sei
-$\bbfunc_{\textsf{LOOP}}(\ell)=0$ falls es kein Programm der Länge $\leq\ell$ gibt.
+$\bbfunc_{\textsf{LOOP}}(\ell)=0$, falls es kein Programm der Länge $\leq\ell$ gibt.
 }\pause
 
 \emph{Beobachtung:} $\bbfunc_{\textsf{LOOP}}$ ist wohldefiniert:
@@ -453,7 +453,7 @@
 }\bigskip\pause
 
 Semantik von $\SStartWhile{\Svar{x}}P~\SEndWhile{}$:\\
-$P$ wird ausgeführt solange der aktuelle Wert von $\Svar{x}$ ungleich $0$ ist.\\
+$P$ wird ausgeführt, solange der aktuelle Wert von $\Svar{x}$ ungleich $0$ ist.\\
 \textcolor{devilscss}{(dies hängt davon ab, wie $P$ den Wert von $\Svar{x}$ ändert)}
 \medskip
 
@@ -490,7 +490,7 @@
 
 \end{frame}
 
-\begin{frame}\frametitle{WHILE-Berechenbare Funktionen}
+\begin{frame}\frametitle{WHILE-berechenbare Funktionen}
 
 \defbox{\emph{Definition:} Eine partielle Funktion $f:\mathbb{N}^k\to\mathbb{N}$ heißt \redalert{WHILE-berechenbar}, wenn es ein WHILE-Programm $P$ gibt, so dass gilt:
 \begin{itemize}
@@ -630,7 +630,7 @@
 % \url{http://www.eugenkiss.com/projects/lgw/}\bigskip
 
 \anybox{yellow}{
-Was erwartet uns als nächstes?
+Was erwartet uns als Nächstes?
 \begin{itemize}
 \item Relevantere Probleme
 \item Reduktionen
diff --git a/Vorlesungen/lecture-04.tex b/Vorlesungen/lecture-04.tex
index 3f0b6b4..1642f54 100644
--- a/Vorlesungen/lecture-04.tex
+++ b/Vorlesungen/lecture-04.tex
@@ -227,7 +227,7 @@
 
 \examplebox{\emph{Beispiel:} Die Goldbachsche Vermutung (Christian Goldbach, 1742) besagt, dass jede gerade Zahl $n\geq 4$ die Summe zweier Primzahlen ist. Zum Beispiel ist $4=2+2$ und $100=47+53$.}\pause
 
-Man kann leicht einen Algorithmus \Smach{A} angeben, der die Goldbachsche Vermuting systematisch verifiziert, d.h., für alle geraden Zahlen ab $4$ testet:
+Man kann leicht einen Algorithmus \Smach{A} angeben, der die Goldbachsche Vermutung systematisch verifiziert, d.h., für alle geraden Zahlen ab $4$ testet:
 \begin{itemize}
 \item Erfolg: teste die nächste gerade Zahl
 \item Misserfolg: terminiere mit Meldung "`Goldbach hat sich geirrt!"'
@@ -264,7 +264,7 @@
 % \alert{Wer rasiert den Barbier?}
 \alert{Akzeptiert $\Smach{D}$ die Eingabe $\textsf{enc}(\Smach{D})$?}\pause\\[1ex]
 
-\narrowcentering{$\Smach{D}$ hält und akzeptiert $\quad$ genau dann wenn $\quad$ $\Smach{D}$ nicht hält}\\[1ex]
+\narrowcentering{$\Smach{D}$ hält und akzeptiert $\quad$ genau dann, wenn $\quad$ $\Smach{D}$ nicht hält}\\[1ex]
 
 Widerspruch.\qed
 
@@ -319,7 +319,7 @@
 
 \begin{frame}\frametitle{Turing-Reduktionen: Beispiel}
 
-\examplebox{\emph{Beispiel:} Das Nicht-Halteproblem $\overline{\Slang{P}}_{\textsf{Halt}}$,
+\examplebox{\emph{Beispiel:} Das Nichthalteproblem $\overline{\Slang{P}}_{\textsf{Halt}}$,
 ist definiert als\\[1ex]
 \narrowcentering{$\overline{\Slang{P}}_{\textsf{Halt}} = \{\textsf{enc}(\Smach{M})\Sterm{\#}\Sterm{\#}\textsf{enc}(w)\mid \text{$\Smach{M}$ hält nicht bei Eingabe $w$}\}$}\\[1ex]
 %
@@ -329,7 +329,7 @@
 
 Daraus ergibt sich:\medskip
 
-\theobox{\emph{Satz:} Das Nicht-Halteproblem $\overline{\Slang{P}}_{\textsf{Halt}}$ ist unentscheidbar.}
+\theobox{\emph{Satz:} Das Nichthalteproblem $\overline{\Slang{P}}_{\textsf{Halt}}$ ist unentscheidbar.}
 
 \end{frame}
 
@@ -390,7 +390,7 @@
 \emph{Idee:} Im letzten Beweis verwendeten wir das $\epsilon$-Halteproblem nicht als Subroutine eines komplexen Programms, sondern wir formten das Halteproblem in ein $\epsilon$-Halteproblem um\bigskip
 
 \defbox{Eine berechenbare totale Funktion $f:\Sigma^*\to\Sigma^*$ ist eine \redalert{Many-One-Reduktion} von einer Sprache \Slang{P} auf eine Sprache \Slang{Q} (in Symbolen: $\Slang{P}\leq_m \Slang{Q}$), wenn für alle Wörter $w\in\Sigma^*$ gilt:\\[1ex]
-\narrowcentering{$w\in\Slang{P}\quad$ genau dann wenn $\quad f(w)\in\Slang{Q}$}}\pause\bigskip
+\narrowcentering{$w\in\Slang{P}\quad$ genau dann, wenn $\quad f(w)\in\Slang{Q}$}}\pause\bigskip
 
 \examplebox{\emph{Beispiel:} Die folgende Funktion definiert eine Many-One-Reduktion vom
 Halteproblem auf das $\epsilon$-Halteproblem:%\\%[-4ex]
@@ -464,7 +464,7 @@
 \bigskip
 
 \anybox{yellow}{
-Was erwartet uns als nächstes?
+Was erwartet uns als Nächstes?
 \begin{itemize}
 \item Mehr zu Semi-Entscheidbarkeit 
 \item Ein unentscheidbares Problem von Emil Post \ldots
diff --git a/Vorlesungen/lecture-05.tex b/Vorlesungen/lecture-05.tex
index 9e11706..f45bf09 100644
--- a/Vorlesungen/lecture-05.tex
+++ b/Vorlesungen/lecture-05.tex
@@ -33,9 +33,9 @@
 
 Ein interessantes Resultat von Henry Gordon Rice bewahrt uns davor, noch hunderte andere Probleme im Detail zu betrachten:\medskip
 
-\theobox{\emph{Satz von Rice (informelle Version):} Jede nicht-triviale Frage über die von einer TM ausgeführte Berechnung ist unentscheidbar.}\bigskip\pause
+\theobox{\emph{Satz von Rice (informelle Version):} Jede nichttriviale Frage über die von einer TM ausgeführte Berechnung ist unentscheidbar.}\bigskip\pause
 
-\theobox{\emph{Satz von Rice (formell):} Sei $E$ eine Eigenschaft von Sprachen, die für manche Turing-erkennbare Sprachen gilt und für manche Turing-erkennbare Sprachen nicht gilt (="`nicht-triviale Eigenschaft"'). Dann ist das folgende Problem unentscheidbar:
+\theobox{\emph{Satz von Rice (formell):} Sei $E$ eine Eigenschaft von Sprachen, die für manche Turing-erkennbare Sprachen gilt und für manche Turing-erkennbare Sprachen nicht gilt (="`nichttriviale Eigenschaft"'). Dann ist das folgende Problem unentscheidbar:
 \begin{itemize}
 \item Eingabe: Turingmaschine $\Smach{M}$
 \item Ausgabe: Hat $\Slang{L}(\Smach{M})$ die Eigenschaft $E$?
@@ -68,7 +68,7 @@
 
 \begin{frame}[t]\frametitle{Der Satz von Rice: Beweis (1)}
 
-\theobox{\emph{Satz von Rice:} Sei $E$ eine nicht-triviale Eigenschaft von Turing-erkennbaren Sprachen. Dann ist das folgende unentscheidbar:%
+\theobox{\emph{Satz von Rice:} Sei $E$ eine nichttriviale Eigenschaft von Turing-erkennbaren Sprachen. Dann ist das folgende unentscheidbar:%
 \begin{itemize}
 \item Eingabe: Turingmaschine $\Smach{M}$
 \item Ausgabe: Hat die Sprache $\Slang{L}(\Smach{M})$ die Eigenschaft $E$?
@@ -81,7 +81,7 @@
 \item Sei $\emptyset\notin E$ 
 	(o.B.d.A.: wir könnten sonst auch Unentscheidbarkeit von $\overline{E}$ beweisen)
 \item Sei $\Smach{M}_{\Slang{L}}$ eine TM, die eine Sprache $\Slang{L}\in E$ akzeptiert\\
-	(muss existieren, da $E$ nicht-trivial ist)
+	(muss existieren, da $E$ nichttrivial ist)
 % \item Sei $\Smach{M}_\emptyset$ eine TM mit $\Slang{L}(\Smach{M}_\emptyset)=\emptyset$
 %%% <- Könnte man als Wert für falsch kodierte Eingaben nutzen, aber das ist nicht nötig
 \end{itemize}
@@ -90,7 +90,7 @@
 
 \begin{frame}[t]\frametitle{Der Satz von Rice: Beweis (2)}
 
-\theobox{\emph{Satz von Rice:} Sei $E$ eine nicht-triviale Eigenschaft von Turing-erkennbaren Sprachen. Dann ist das folgende unentscheidbar:%
+\theobox{\emph{Satz von Rice:} Sei $E$ eine nichttriviale Eigenschaft von Turing-erkennbaren Sprachen. Dann ist das folgende unentscheidbar:%
 \begin{itemize}
 \item Eingabe: Turingmaschine $\Smach{M}$
 \item Ausgabe: Hat die Sprache $\Slang{L}(\Smach{M})$ die Eigenschaft $E$?
@@ -162,7 +162,7 @@
 
 Es gibt einen interessanten Zusammenhang von Komplementierung und Semi-Entscheidbarkeit:\\[1ex]
 
-\theobox{\emph{Satz:} $\Slang{L}$ ist genau dann entscheidbar, wenn $\Slang{L}$ und $\overline{\Slang{L}}$ semi-entscheibar sind.
+\theobox{\emph{Satz:} $\Slang{L}$ ist genau dann entscheidbar, wenn $\Slang{L}$ und $\overline{\Slang{L}}$ semi-entscheidbar sind.
 }\pause
 
 \emph{Beweis:} "`$\Rightarrow$"' Angenommen $\Slang{L}$ ist entscheidbar.\pause
@@ -178,10 +178,10 @@
 
 Es gibt einen interessanten Zusammenhang von Komplementierung und Semi-Entscheidbarkeit:\\[1ex]
 
-\theobox{\emph{Satz:} $\Slang{L}$ ist genau dann entscheidbar, wenn $\Slang{L}$ und $\overline{\Slang{L}}$ semi-entscheibar sind.
+\theobox{\emph{Satz:} $\Slang{L}$ ist genau dann entscheidbar, wenn $\Slang{L}$ und $\overline{\Slang{L}}$ semi-entscheidbar sind.
 }
 
-\emph{Beweis:} "`$\Leftarrow$"' Wenn $\Slang{L}$ und $\overline{\Slang{L}}$ semi-entscheibar sind, dann werden sie durch TMs $\Smach{M}_{\Slang{L}}$ und
+\emph{Beweis:} "`$\Leftarrow$"' Wenn $\Slang{L}$ und $\overline{\Slang{L}}$ semi-entscheidbar sind, dann werden sie durch TMs $\Smach{M}_{\Slang{L}}$ und
 $\Smach{M}_{\overline{\Slang{L}}}$ erkannt.\pause\medskip
 
 Algorithmus: Für Eingabe $w$, iteriere über alle $n=1,2,3,\ldots$
@@ -202,7 +202,7 @@
 
 Wir können unsere Einsichten zusammenfassen:\bigskip
 
-\theobox{\emph{Korrolar:} Wenn $\Slang{L}$ unentscheidbar aber semi-entscheidbar ist, dann
+\theobox{\emph{Korollar:} Wenn $\Slang{L}$ unentscheidbar aber semi-entscheidbar ist, dann
 kann $\overline{\Slang{L}}$ nicht semi-entscheidbar (und auch nicht entscheidbar) sein.
 }\bigskip\pause
 
@@ -233,7 +233,7 @@
 \emph{Anmerkung 1:} Wir haben diese Aussage in der letzten Vorlesung mit "`entscheidbar"' anstelle
 von "`semi-entscheidbar"' gezeigt. Die Idee ist genau die gleiche.
 
-\emph{Anmerkung 2:} Die Aussage gilt analog wenn man "`co-semi-entscheidbar"' anstelle
+\emph{Anmerkung 2:} Die Aussage gilt analog, wenn man "`co-semi-entscheidbar"' anstelle
 von "`semi-entscheidbar"' verwendet. Dies folgt schon deshalb, weil eine Many-One-Reduktion
 $\Slang{P}\leq_m \Slang{Q}$ gleichzeitig auch eine Many-One-Reduktion $\overline{\Slang{P}}\leq_m \overline{\Slang{Q}}$ ist.
 
@@ -563,7 +563,7 @@
 Das \alert{Postsche Korrespondenzproblem} ist ein unentscheidbares Problem, das nicht (direkt) mit TMs zu tun hat -- es ist hilfreich bei vielen Reduktionen\bigskip
 
 \anybox{yellow}{
-Was erwartet uns als nächstes?
+Was erwartet uns als Nächstes?
 \begin{itemize}
 \item Unberechenbare Probleme formaler Sprachen
 \item Abschließende Bemerkungen zu Berechenbarkeit
diff --git a/Vorlesungen/lecture-06.tex b/Vorlesungen/lecture-06.tex
index fc10bf6..321dc66 100644
--- a/Vorlesungen/lecture-06.tex
+++ b/Vorlesungen/lecture-06.tex
@@ -108,7 +108,7 @@
 \item Für eine gegebene PCP-Instanz $P$
 \item konstruieren wir kontextfreie Grammatiken $G_x$ und $G_y$,\\[1ex]
 	so dass gilt:
-\item $P$ hat eine Lösung genau dann wenn $\Slang{L}(G_x)\cap\Slang{L}(G_y)\neq\emptyset$.
+\item $P$ hat eine Lösung genau dann, wenn $\Slang{L}(G_x)\cap\Slang{L}(G_y)\neq\emptyset$.
 \end{itemize}
 
 \end{frame}
@@ -355,7 +355,7 @@
 \emph{Frage:} Hält $\Smach{M}$ auf $w$?
 }
 
-Dies ist sozusagen ein Haltproblem höherer Ordnung.\bigskip\pause
+Dies ist sozusagen ein Halteproblem höherer Ordnung.\bigskip\pause
 
 Ein noch schwereres Problem $\Slang{P}^3_{\text{halt}}$ ist
 das Halteproblem für TMs, die $\Slang{P}^2_{\text{halt}}$ als Subroutine
@@ -380,7 +380,7 @@
 
 Die Situation ist ziemlich kompliziert:
 \begin{itemize}
-\item Es gibt unentscheibare Probleme $\Slang{A}$ und $\Slang{B}$, so dass
+\item Es gibt unentscheidbare Probleme $\Slang{A}$ und $\Slang{B}$, so dass
 \item $\Slang{A}\leq_T \Slang{P}_{\text{halt}}$ und $\Slang{B}\leq_T \Slang{P}_{\text{halt}}$, aber
 \item $\Slang{A}\not\leq_T \Slang{B}$ und $\Slang{B}\not\leq_T \Slang{A}$
 \end{itemize}
@@ -456,7 +456,7 @@
 \alert{Erlaubte Konstruktionsschritte:}
 \begin{enumerate}[(1)]
 \item Ziehen einer beliebig langen Geraden durch zwei verschiedene Punkte
-\item Zeichnen eines Kreises mit einen gegebenen Mittelpunkt, der durch einen gegebenen Punkt verläuft
+\item Zeichnen eines Kreises mit einem gegebenen Mittelpunkt, der durch einen gegebenen Punkt verläuft
 \item Abtragen einer Strecke mit dem Zirkel\\[0.5ex]
 {\tiny Bei Euklid nicht direkt erlaubt, aber Euklid selbst hat bewiesen, dass diese Operation als Makro mithilfe der Operationen (1) und (2) darstellbar ist
 
@@ -610,7 +610,7 @@
 Euklid hätte vielleicht auch Informatiker sein können\bigskip
 
 \anybox{yellow}{
-Was erwartet uns als nächstes?
+Was erwartet uns als Nächstes?
 \begin{itemize}
 \item Methoden, zur Unterteilung entscheidbarer Probleme: Komplexität
 \item Effizienz von Turingmaschinen
diff --git a/Vorlesungen/lecture-07.tex b/Vorlesungen/lecture-07.tex
index 1d31197..b1faefa 100644
--- a/Vorlesungen/lecture-07.tex
+++ b/Vorlesungen/lecture-07.tex
@@ -19,8 +19,8 @@
 
 \node (decback) [draw=nightblue, text depth = 1cm, text width = 1.9cm, fill=white, inner ysep=2.5mm, inner xsep=2.5mm] at (0,0) {\tiny\phantom{~}};
 
-\visible<3->{\node (re) [draw=darkgreen, text depth = 1.0cm, text width = 5.4cm, fill=darkgreen!10,thick,align=right, inner ysep=1mm, inner xsep=1mm,fill opacity=0.5, text opacity=1] at (1.7,0.02) {\footnotesize Co-Semientscheidbare\\ Probleme};}
-\visible<2->{\node (re) [draw=orange, text depth = 1.0cm, text width = 5.4cm, fill=orange!10,thick,align=left, inner ysep=1mm, inner xsep=1mm, fill opacity=0.5, text opacity=1] at (-1.7,-0.02) {\footnotesize Semientscheidbare\\ Probleme};}
+\visible<3->{\node (re) [draw=darkgreen, text depth = 1.0cm, text width = 5.4cm, fill=darkgreen!10,thick,align=right, inner ysep=1mm, inner xsep=1mm,fill opacity=0.5, text opacity=1] at (1.7,0.02) {\footnotesize Co-Semi-Entscheidbare\\ Probleme};}
+\visible<2->{\node (re) [draw=orange, text depth = 1.0cm, text width = 5.4cm, fill=orange!10,thick,align=left, inner ysep=1mm, inner xsep=1mm, fill opacity=0.5, text opacity=1] at (-1.7,-0.02) {\footnotesize Semi-Entscheidbare\\ Probleme};}
 
 
  \node (dec) [draw=strongyellow, text depth = 1cm, text width = 1.9cm, fill=strongyellow!10,thick,align=center, inner ysep=1mm, inner xsep=1mm] at (0,0) {\tiny 
@@ -47,7 +47,7 @@
 
 \begin{frame}\frametitle{Ein klassisches Problem}
 
-Ein populäre Frage der Königsberger:\medskip
+Eine populäre Frage der Königsberger:\medskip
 
 \anybox{strongyellow}{Gibt es einen Weg durch die Stadt, auf dem man jede der sieben Brücken von Königsberg genau einmal überquert?}\bigskip
 
@@ -180,7 +180,7 @@
 zyklischer Hamiltonpfad.}\bigskip\pause
 
 Wie bei Eulerpfaden ist die naive Lösung sehr ineffizient, da man
-alle (exponentiell viele) Pfade systematisch Durchprobieren muss.\bigskip\pause
+alle (exponentiell viele) Pfade systematisch durchprobieren muss.\bigskip\pause
 
 Aber im Gegensatz zu Eulerpfaden hat bislang niemand eine elegante
 einfache Lösung gefunden. Die meisten Experten glauben, dass es prinzipiell
@@ -200,7 +200,7 @@
 
 \anybox{strongyellow}{\emph{Aufgabe:} Gegeben einen Graphen mit zwei Knoten $A$ und $B$, finde einen längsten Weg von $A$ nach $B$.}\pause\bigskip
 
-\alert{Schwer!} Keine sub-exponentielle Lösung bekannt
+\alert{Schwer!} Keine subexponentielle Lösung bekannt
 \bigskip\pause
 
 \medskip
@@ -307,10 +307,10 @@
 \defbox{%
 Sei $f:\mathbb{N}\to\mathbb{R}$ eine Funktion und $\Smach{M}$ eine Turingmaschine.
 \begin{itemize}
-\item $\Smach{M}$ heißt \redalert{$O(f)$-zeitbeschränkt} wenn es eine Funktion $g\in O(f)$ gibt, so
+\item $\Smach{M}$ heißt \redalert{$O(f)$-zeitbeschränkt}, wenn es eine Funktion $g\in O(f)$ gibt, so
 dass $\Smach{M}$ für eine beliebige Eingabe $w\in\Sigma^*$ nach maximal $g(|w|)$ Schritten anhält.
 %
-\item $\Smach{M}$ heißt \redalert{$O(f)$-speicherbeschränkt} wenn es eine Funktion $g\in O(f)$ gibt, so
+\item $\Smach{M}$ heißt \redalert{$O(f)$-speicherbeschränkt}, wenn es eine Funktion $g\in O(f)$ gibt, so
 dass $\Smach{M}$ für eine beliebige Eingabe $w\in\Sigma^*$ hält und zuvor maximal $g(|w|)$ Speicherzellen verwendet.
 \end{itemize}
 }\pause
@@ -447,7 +447,7 @@
 
 {\tiny \emph{Anmerkung:} Wir betrachten hier verschiedene Versionen deterministischer
 Rechenmodelle. Zwischen DTMs und NTMs gibt es vermutlich
-schon große (nicht-polynomielle) Unterschiede.
+schon große (nichtpolynomielle) Unterschiede.
 
 }
 
@@ -463,7 +463,7 @@
 \emph{Antwort:} "`Nein, aber vernünftige Kodierungen unterscheiden sich voneinander
 in der Regel nur polynomiell."'\bigskip
 
-\examplebox{\emph{Beispiel:} Ein Graph kann als Adjazenzmatrix kodiert werden ($O(n^2)$ Speicher) oder z.B. auch als Adjazenliste ($O(e\cdot \log v)$ Speicher für $e$ Kanten und $v$ Knoten). Letzteres ist deutlich effizienter für lichte Graphen, aber der Unterschied bleibt stets polynomiell.}\bigskip
+\examplebox{\emph{Beispiel:} Ein Graph kann als Adjazenzmatrix kodiert werden ($O(n^2)$ Speicher) oder z.B. auch als Adjazenzliste ($O(e\cdot \log v)$ Speicher für $e$ Kanten und $v$ Knoten). Letzteres ist deutlich effizienter für lichte Graphen, aber der Unterschied bleibt stets polynomiell.}\bigskip
 
 \emph{Aber:} Wir werden Fälle sehen, in denen eine (besonders ineffiziente) Kodierung die Komplexität verändert.
 
@@ -471,7 +471,7 @@
 
 \begin{frame}\frametitle{Implementierungsdetails}
 
-Es gibt viele unterschiedliche Arten um ein Problem praktisch zu lösen,
+Es gibt viele unterschiedliche Arten, um ein Problem praktisch zu lösen,
 z.B. unter Verwendung spezifischer Datenstrukturen.\\\smallskip
 
 \anybox{purple}{Sind $\Scomplclass{DTIME}(f)$ und $\Scomplclass{DSPACE}(f)$ für verschiedene Implementierungsdetails gleich?}\pause\bigskip
@@ -500,7 +500,7 @@
 
 \examplebox{\emph{Beispiel:} Ein naiver Algorithmus zur Matrixmultiplikation liegt in
 $\Scomplclass{DTIME}(n^{\redalert{3}})$.
-\only<-2>{~\\~\\~\\}%
+\only<-2>{\\~}%
 \only<3->{\\Seit Jahrzehnten suchen Forscher nach besseren
 Lösungen:
 $\Scomplclass{DTIME}(n^{\redalert{2,808}})$ [\mbox{Strassen}, 1969], 
@@ -538,7 +538,7 @@
 
 \end{frame}
 
-\begin{frame}\frametitle{Wichtige Komplextitätsklassen}
+\begin{frame}\frametitle{Wichtige Komplexitätsklassen}
 
 Die wichtigen deterministischen Komplexitätsklassen fassen jeweils ganze Familien von
 zeit- oder speicherbeschränkten Klassen zusammen. Wir erwähnen hier nur die praktisch wichtigsten:
@@ -598,7 +598,7 @@
 
 {\footnotesize
 Das genügt zur Erkennung von Sprachen. Wenn die TM eine Ausgabe berechnen soll, dann wird dafür ein 
-drittes \redalert{Ausgabeband} verwendet, auf dem man beliebig viele Zeichen einmalig schreiben aber nicht lesen kann.\\
+drittes \redalert{Ausgabeband} verwendet, auf dem man beliebig viele Zeichen einmalig schreiben, aber nicht lesen kann.\\
 }
 
 \end{frame}
@@ -639,7 +639,7 @@
 kann in $\Scomplclass{LogSpace}$ implementiert werden: wir zählen die Kanten jedes Knotens 
 und speichern die Zahl der Knoten ungeraden Grades, jeweils binär.}\pause
 
-\examplebox{\emph{Beispiel:} Die Suche nach Hamilton-Pfaden ist in $\Scomplclass{ExpTime}$ aber auch in $\Scomplclass{PSpace}$.}\pause
+\examplebox{\emph{Beispiel:} Die Suche nach Hamiltonpfaden ist in $\Scomplclass{ExpTime}$ aber auch in $\Scomplclass{PSpace}$.}\pause
 
 \examplebox{\emph{Beispiel:} Ein typisches Problem in $\Scomplclass{P}$ haben wir bereits in
 der Vorlesung Formale Systeme kennengelernt: Erfüllbarkeit von propositionaler Horn-Logik. Unser Resolutionsalgorithmus
@@ -659,7 +659,7 @@
 \[\Scomplclass{L}\subseteq \Scomplclass{P}\subseteq\Scomplclass{PSpace}\subseteq \Scomplclass{Exp}\]
 
 \anybox{yellow}{
-Was erwartet uns als nächstes?
+Was erwartet uns als Nächstes?
 \begin{itemize}
 \item Effizient lösbare Probleme: $\Scomplclass{P}$
 \item Die kleinste "`traditionelle"' Komplexitätsklasse: $\Scomplclass{L}$
diff --git a/Vorlesungen/lecture-08.tex b/Vorlesungen/lecture-08.tex
index 87d9eb1..fea8ed4 100644
--- a/Vorlesungen/lecture-08.tex
+++ b/Vorlesungen/lecture-08.tex
@@ -88,7 +88,7 @@
 \[\Scomplclass{DTIME}(f)\subseteq \Scomplclass{DSPACE}(f).\]
 }
 
-\emph{Beweis:} Die TM benötigt immer mindestens einen Schritt um eine zusätzliche Speicherstelle zu beschreiben.\qed\bigskip
+\emph{Beweis:} Die TM benötigt immer mindestens einen Schritt, um eine zusätzliche Speicherstelle zu beschreiben.\qed\bigskip
 
 \pause Daraus folgt zum Beispiel $\Scomplclass{PTime}\subseteq\Scomplclass{PSpace}$.
 
@@ -126,10 +126,10 @@
 \defbox{%
 Sei $f:\mathbb{N}\to\mathbb{R}$ eine Funktion und $\Smach{M}$ eine nichtdeterministische \ghost{TM.}
 \begin{itemize}
-\item $\Smach{M}$ heißt \redalert{$O(f)$-zeitbeschränkt} wenn es eine Funktion $g\in O(f)$ gibt, so
+\item $\Smach{M}$ heißt \redalert{$O(f)$-zeitbeschränkt}, wenn es eine Funktion $g\in O(f)$ gibt, so
 dass $\Smach{M}$ für eine beliebige Eingabe $w\in\Sigma^*$ \alert{auf jedem Berechnungspfad} nach maximal $g(|w|)$ Schritten anhält.
 %
-\item $\Smach{M}$ heißt \redalert{$O(f)$-speicherbeschränkt} wenn es eine Funktion $g\in O(f)$ gibt, so
+\item $\Smach{M}$ heißt \redalert{$O(f)$-speicherbeschränkt}, wenn es eine Funktion $g\in O(f)$ gibt, so
 dass $\Smach{M}$ für eine beliebige Eingabe $w\in\Sigma^*$ hält und zuvor \alert{auf jedem Berechnungspfad} maximal $g(|w|)$ Speicherzellen verwendet.
 \end{itemize}
 }
@@ -157,7 +157,7 @@
 \end{frame}
 
 
-\begin{frame}\frametitle{Nichtdeterministische Komplextitätsklassen}
+\begin{frame}\frametitle{Nichtdeterministische Komplexitätsklassen}
 
 Auch hier beschränken wir uns auf einige wichtige Fälle:
 
@@ -310,8 +310,8 @@
 
 Aber der Begriff "`linear"' ist nicht robust:
 \begin{itemize}
-\item Abhänging von Details des Maschinenmodells
-\item Abhänging von Details der Kodierung
+\item Abhängig von Details des Maschinenmodells
+\item Abhängig von Details der Kodierung
 \end{itemize}
 \bigskip
 $\leadsto$ Polynomielle Zeit als robuste Verallgemeinerung von Linearzeit:\bigskip
@@ -395,7 +395,7 @@
 \begin{itemize}
 \item Eine \alert{Hornklausel} ist eine aussagenlogische Formel der Form $p_1\wedge\ldots\wedge p_n\to q$ mit $n\geq 0$
 {\tiny (bei $n=0$ ergibt sich einfach $q$ -- ein \alert{Fakt})}
-\item Eine Formel ist \alert{erfüllbar} wenn sie für eine Wertezuweisung auf wahr abgebildet wird
+\item Eine Formel ist \alert{erfüllbar}, wenn sie für eine Wertezuweisung auf wahr abgebildet wird
 \item Eine Menge von Formeln ist erfüllbar, wenn es eine Wert-\\zuweisung gibt, die alle
 ihre Elemente gleichzeitig wahr macht
 \end{itemize}\bigskip
@@ -456,9 +456,9 @@
 \smallskip\pause
 
 \begin{itemize}
-\item \emph{Sub-lineare Zeit} funktioniert mit dem normalen TM-Modell nicht, da man
+\item \emph{Sublineare Zeit} funktioniert mit dem normalen TM-Modell nicht, da man
 in dieser Zeit nicht einmal die Eingabe lesen kann {\tiny (erfordert Rechenmodelle mit einer Form von Parallelverarbeitung \ldots)}
-\item \emph{Sub-linearer Speicher} ist machbar, wenn man ein getrenntes schreibgeschütztes Eingabeband erlaubt (siehe letzte Vorlesung)
+\item \emph{Sublinearer Speicher} ist machbar, wenn man ein getrenntes schreibgeschütztes Eingabeband erlaubt (siehe letzte Vorlesung)
 \end{itemize}
 $\leadsto$ Komplexitätsklassen \Scomplclass{L} und \Scomplclass{NL}
 
@@ -529,7 +529,7 @@
 
 \defbox{Eine polynomiell berechenbare Funktion $f:\Sigma^*\to\Sigma^*$ ist eine \redalert{polynomielle Many-One-Reduktion} von einer Sprache
 \Slang{P} auf eine Sprache \Slang{Q} (in Symbolen: $\Slang{P}\leq_p \Slang{Q}$), wenn für alle Wörter $w\in\Sigma^*$ gilt:\\[1ex]
-\narrowcentering{$w\in\Slang{P}\quad$ genau dann wenn $\quad f(w)\in\Slang{Q}$}}\pause\bigskip
+\narrowcentering{$w\in\Slang{P}\quad$ genau dann, wenn $\quad f(w)\in\Slang{Q}$}}\pause\bigskip
 
 Wir sprechen oft einfach von \redalert{polynomiellen Reduktionen}.
 \bigskip
@@ -591,7 +591,7 @@
 Mit polynomiellen Reduktionen kann man aus der Komplexität eines Problems auf die eines anderen schließen\bigskip
 
 \anybox{yellow}{
-Was erwartet uns als nächstes?
+Was erwartet uns als Nächstes?
 \begin{itemize}
 \item $\Scomplclass{NP}$
 \item $\Scomplclass{NL}$
diff --git a/Vorlesungen/lecture-09.tex b/Vorlesungen/lecture-09.tex
index 88e2dd6..ee79b86 100644
--- a/Vorlesungen/lecture-09.tex
+++ b/Vorlesungen/lecture-09.tex
@@ -28,7 +28,7 @@
 \begin{frame}\frametitle{Warum sollten Reduktionen effizient sein?}
 
 \emph{Intuition:} Eine aufwändige Reduktion kann jedes Problem indirekt lösen, aber dadurch lernt man nichts
-interessantes über dessen Komplexität.\pause
+Interessantes über dessen Komplexität.\pause
 \bigskip
 
 \theobox{\emph{Satz:} Sei $\Slang{L}=\{\Sterm{a}\}$ eine Sprache über dem Alphabet $\{\Sterm{a}\}$.
@@ -156,10 +156,10 @@
 
 Daraus ergibt sich die Definition einer Sprachklasse:
 
-\defbox{Eine Sprache $\Slang{L}$ ist \redalert{nachweis-polynomiell} wenn es für sie einen polynomiellen
+\defbox{Eine Sprache $\Slang{L}$ ist \redalert{nachweis-polynomiell}, wenn es für sie einen polynomiellen
 Verifikator gibt.}\medskip\pause
 
-\examplebox{\emph{Beispiel:} Die Entscheidung, ob ein gegebener Graph einen Hamilton-Pfad zulässt, ist nachweis-polynomiell.
+\examplebox{\emph{Beispiel:} Die Entscheidung, ob ein gegebener Graph einen Hamiltonpfad zulässt, ist nachweis-polynomiell.
 Als Zertifikat dient der entsprechende Pfad.}\bigskip
 
 \end{frame}
@@ -197,9 +197,9 @@
 
 % \emph{Anmerkung:} Mehrere Gegenstände können gleiche Werte haben.\bigskip\pause
 
-\defbox{\Slang{Zusammengesetzte Zahl} (Nicht-Primzahl)\\[1ex]
+\defbox{\Slang{Zusammengesetzte Zahl} (Nichtprimzahl)\\[1ex]
 \emph{Gegeben:} Eine natürliche Zahl $z>1$\\[1ex]
-\emph{Frage:} Gibt es eine natürliche Zahlen $p,q>1$ mit $p\cdot q = z$?\\
+\emph{Frage:} Gibt es natürliche Zahlen $p,q>1$ mit $p\cdot q = z$?\\
 }
 
 \end{frame}
@@ -211,8 +211,8 @@
 \theobox{\emph{Satz:} Die Klasse \Scomplclass{P} ist unter Komplement abgeschlossen.}
 
 \emph{Beweis:} Wenn es für \Slang{L} eine polynomiell-zeitbeschränkte TM \Smach{M}
-gibt, dann erhält man eine TM für $\overline{\Slang{L}}$ indem man akzeptierende
-und nicht-akzeptierende Zustände von \Smach{M} vertauscht.\qed\medskip
+gibt, dann erhält man eine TM für $\overline{\Slang{L}}$, indem man akzeptierende
+und nichtakzeptierende Zustände von \Smach{M} vertauscht.\qed\medskip
 
 \emph{Allgemein gilt:} Jede deterministische Komplexitätsklasse ist unter Komplement abgeschlossen.
 
@@ -242,7 +242,7 @@
 
 \defbox{\Slang{Primzahl} (= $\overline{\Slang{Zusammengesetzte Zahl}}$)\\[1ex]
 \emph{Gegeben:} Eine natürliche Zahl $z>1$\\[1ex]
-\emph{Frage:} Gibt es eine keine natürliche Zahlen $p,q>1$ mit $p\cdot q = z$?\\
+\emph{Frage:} Gibt es keine natürlichen Zahlen $p,q>1$ mit $p\cdot q = z$?\\
 }\pause
 
 Seit 1975 ist bekannt: $\Slang{Primzahl}\in\Scomplclass{NP}$, also
@@ -401,7 +401,7 @@
 
 \emph{Beweis Teil (2):} Clique ist \Scomplclass{NP}-schwer.
 \begin{itemize}
-\item Sei $F$ eine aussagenlogische Formel in CNF:\\
+\item Sei $F$ eine aussagenlogische Formel in KNF:\\
 $F=\left((L^1_1\vee \ldots\vee L^1_{n_1})\wedge \ldots\wedge (L^\ell_1\vee \ldots\vee L^\ell_{n_\ell})\right)$\pause
 %
 \item Wir definieren einen Graphen $G_F$, so dass gilt:\\[1ex]
@@ -490,7 +490,7 @@
 \emph{Beweis:} Die Reduktion auf \Slang{Clique} ist sehr einfach:
 \begin{itemize}
 \item Ein Graph hat eine unabhängige Menge der Größe $k$\\
-genau dann wenn
+genau dann, wenn
 \item sein Komplementgraph eine Clique der Größe $k$ hat
 \end{itemize}
 $\leadsto$ Komplementierung ist polynomiell\qed
@@ -511,7 +511,7 @@
 Es gibt sehr viele bekannte $\Scomplclass{NP}$-vollständige Probleme\bigskip
 
 \anybox{yellow}{
-Was erwartet uns als nächstes?
+Was erwartet uns als Nächstes?
 \begin{itemize}
 \item Mehr $\Scomplclass{NP}$
 \item Pseudopolynomielle Probleme
diff --git a/Vorlesungen/lecture-10.tex b/Vorlesungen/lecture-10.tex
index ac49190..8d73002 100644
--- a/Vorlesungen/lecture-10.tex
+++ b/Vorlesungen/lecture-10.tex
@@ -94,7 +94,7 @@
 \begin{frame}
   \frametitle{\Slang{SAT} $\leq_p$ \Slang{Teilmengen-Summe}}
     \emph{Gegeben: } Formel $F = (C_1 \wedge \dots \wedge C_k)$ in
-  CNF.\\
+  KNF.\\
   (o.B.d.A. mit maximal 9 Literalen pro Klausel)\pause\\[1ex]
   Seien $p_1, \dots, p_n$ die Variablen in $F$.\\
   Für jedes $p_i$ definieren wir Gegenstände $t_i$ und $f_i$:\\[10pt]
@@ -201,7 +201,7 @@
 
   \anybox{lightblue}{
     \emph{Behauptung:}\\ Gibt es $T\subseteq S$ mit $\sum_{a_i\in T}
-    \val{a_i} = z$ dann ist $F$ erfüllbar.}\bigskip\pause
+    \val{a_i} = z$, dann ist $F$ erfüllbar.}\bigskip\pause
 
   Sei $T \subseteq S$ die gesuchte Menge mit $\sum_{s\in T} \val{s} = z$\pause\\[10pt]
 %
@@ -223,7 +223,7 @@
 
 \newcommand{\weight}[1]{g(#1)}
 
-\begin{frame}\frametitle{Das Rucksack-Problem}
+\begin{frame}\frametitle{Das Rucksackproblem}
 
 \defbox{\Slang{Rucksack} (Knapsack)\\[1ex]
 \emph{Gegeben:} Eine Menge von Gegenständen $G=\{a_1,\ldots,a_n\}$, wobei jedem Gegenstand $a_i$ ein Wert $\val{a_i}$ und ein Gewicht $\weight{a_i}$ zugeordnet ist; ein Mindestwert $w$ und ein Gewichtslimit $\ell$\\[1ex]
@@ -347,7 +347,7 @@
 Zusammenfassung:
 \begin{itemize}
 \item \Slang{Rucksack} ist \Scomplclass{NP}-vollständig
-\item \Slang{Rucksack} ist mittels Dynamischer Programmierung in Zeit $O(n\ell)$ lösbar
+\item \Slang{Rucksack} ist mittels dynamischer Programmierung in Zeit $O(n\ell)$ lösbar
 \end{itemize}
 
 \defbox{\Slang{Rucksack} (Knapsack)\\[1ex]
@@ -439,7 +439,7 @@
 
 \anybox{strongyellow}{Wächst der neuartige Computer mit dem Problem?\\ Ist dieses Wachstum exponentiell?}\bigskip
 
-\examplebox{\emph{Beispiel:} DNS-Rechner lösen Optimierunsaufgaben, aber müssen alle (exponentiell viele) mögliche Lösungen als DNS-Sequenz kodieren.}
+\examplebox{\emph{Beispiel:} DNS-Rechner lösen Optimierungsaufgaben, aber müssen alle (exponentiell viele) mögliche Lösungen als DNS-Sequenz kodieren.}
 
 \end{frame}
 
@@ -566,7 +566,7 @@
 Es sollte eigentlich eine Menge Probleme geben, die weder in \Scomplclass{P} liegen, noch \Scomplclass{NP}-vollständig sind\bigskip
 
 \anybox{yellow}{
-Was erwartet uns als nächstes?
+Was erwartet uns als Nächstes?
 \begin{itemize}
 \item $\Scomplclass{NL}$
 \item Komplexität jenseits von $\Scomplclass{NP}$
diff --git a/Vorlesungen/lecture-11.tex b/Vorlesungen/lecture-11.tex
index 3d52fca..1fd517a 100644
--- a/Vorlesungen/lecture-11.tex
+++ b/Vorlesungen/lecture-11.tex
@@ -41,7 +41,7 @@
 
 \examplebox{
 \emph{Beispiel:} Das Rucksackproblem ist nur dann NP-vollständig,
-wenn die Gewichte der Gegenstände über-polynomiell wachsen dürfen. Ein Problem mit
+wenn die Gewichte der Gegenstände überpolynomiell wachsen dürfen. Ein Problem mit
 so schweren Gegenständen ist aber nur dann interessant, wenn auch der Rucksack
 eine sehr große Kapazität hat. Alternativ könnte man mit sehr hoher Genauigkeit wiegen.
 }
@@ -125,7 +125,7 @@
 
 \emph{Beweis (Algorithmus):}
 \begin{itemize}
-\item Wir verweden einen Pointer $p$ auf einen Knoten (in der Eingabe) und einen Zähler $z$
+\item Wir verwenden einen Pointer $p$ auf einen Knoten (in der Eingabe) und einen Zähler $z$
 \item Initialisiere $*p=s$ und $z=1$
 \item Schleife:
 \begin{itemize}
@@ -141,8 +141,8 @@
 
 Man kann NL-Schwere ähnlich wie für NP definieren:
 \begin{itemize}
-\item Statt polynomiellen Reduktionen verwendet man Logspace-Reduktionen
-\item NL-schwer: jedes Problem in NL ist darauf logspace-reduzierbar
+\item Statt polynomiellen Reduktionen verwendet man LogSpace-Reduktionen
+\item NL-schwer: jedes Problem in NL ist darauf LogSpace-reduzierbar
 \item NL-vollständig: in NL und NL-schwer
 \end{itemize}
 Intuition: NL-vollständige Probleme sind die schwersten in NL
@@ -339,7 +339,7 @@
 \begin{frame}\frametitle{PSpace-Schwere}
 
 \defbox{Ein Problem \Slang{Q} ist \redalert{PSpace-schwer} wenn
-für jedes Problem \Slang{P} in PSpace ein polynomielle Reduktion $\Slang{P}\leq_p \Slang{Q}$ existiert. \Slang{Q} ist \redalert{PSpace-vollständig} wenn es PSpace-schwer ist und in PSpace liegt.}\bigskip\pause
+für jedes Problem \Slang{P} in PSpace eine polynomielle Reduktion $\Slang{P}\leq_p \Slang{Q}$ existiert. \Slang{Q} ist \redalert{PSpace-vollständig} wenn es PSpace-schwer ist und in PSpace liegt.}\bigskip\pause
 
 \theobox{\emph{Satz:} \Slang{TrueQBF} ist PSpace-schwer.}\pause
 
@@ -358,7 +358,7 @@
 \item Emilia gewinnt, wenn die Formel nach Entfernen aller Quantoren wahr wird
 \end{itemize}\bigskip\pause
 
-\anybox{strongyellow}{Beobachtung: Emilia hat eine Gewinnstrategie im Formelspiel genau dann wenn die gegebene QBF wahr ist.}
+\anybox{strongyellow}{Beobachtung: Emilia hat eine Gewinnstrategie im Formelspiel genau dann, wenn die gegebene QBF wahr ist.}
 
 \end{frame}
 
@@ -394,7 +394,7 @@
 
 \begin{frame}\frametitle{\Slang{Geography} ist PSpace-vollständig}
 
-\theobox{\emph{Satz:} \Slang{Geography} ist PSpace-vollständig}\pause
+\theobox{\emph{Satz:} \Slang{Geography} ist PSpace-vollständig.}\pause
 
 \emph{Beweis:} nächste Vorlesung
 
@@ -433,13 +433,13 @@
 
 Es gibt schwere Probleme, die keine leicht zu prüfende Lösung haben\bigskip
 
-Quantifizierte Boolesche Formeln verallgmeinern Aussagenlogik\bigskip
+Quantifizierte Boolesche Formeln verallgemeinern Aussagenlogik\bigskip
 
 PSpace ist die Klasse der interessanten Zwei-Spieler-Spiele, die nicht zu lange dauern
 \bigskip
 
 \anybox{yellow}{
-Was erwartet uns als nächstes?
+Was erwartet uns als Nächstes?
 \begin{itemize}
 \item Alternierung
 \item noch mehr Logik
diff --git a/Vorlesungen/lecture-12.tex b/Vorlesungen/lecture-12.tex
index 870450f..1bbeb9b 100644
--- a/Vorlesungen/lecture-12.tex
+++ b/Vorlesungen/lecture-12.tex
@@ -81,8 +81,8 @@
 
 \begin{frame}\frametitle{\PSpace-Schwere}
 
-\defbox{Ein Problem \Slang{Q} ist \redalert{\PSpace-schwer} wenn
-für jedes Problem \Slang{P} in \PSpace ein polynomielle Reduktion $\Slang{P}\leq_p \Slang{Q}$ existiert. \Slang{Q} ist \redalert{\PSpace-vollständig} wenn es \PSpace-schwer ist und in \PSpace liegt.}\bigskip\pause
+\defbox{Ein Problem \Slang{Q} ist \redalert{\PSpace-schwer}, wenn
+für jedes Problem \Slang{P} in \PSpace ein polynomielle Reduktion $\Slang{P}\leq_p \Slang{Q}$ existiert. \Slang{Q} ist \redalert{\PSpace-vollständig}, wenn es \PSpace-schwer ist und in \PSpace liegt.}\bigskip\pause
 
 \theobox{\emph{Satz:} \Slang{TrueQBF} ist \PSpace-schwer.}\pause
 
@@ -490,11 +490,11 @@
 Jenseits von \ExpSpace gibt es nur wenige relevante Probleme.\medskip
 
 \examplebox{\emph{Beispiel:} Der W3C-Standard \alert{Web Ontology Language} (OWL, Version 2)
-definiert die logische Beschreibungsspache OWL~2~DL. Logisches Schließen in dieser Sprache ist \NTwoExpTime-vollständig.
+definiert die logische Beschreibungssprache OWL~2~DL. Logisches Schließen in dieser Sprache ist \NTwoExpTime-vollständig.
 }\pause
 
 Es gibt aber auch entscheidbare Probleme, die durch keine vielfach exponentiell 
-beschränkte TM entschieden werden: Dies sind Probleme \redalert{nicht-elementarer}
+beschränkte TM entschieden werden: Dies sind Probleme \redalert{nichtelementarer}
 Komplexität\medskip
 
 \examplebox{\emph{Beispiel:} Die Äquivalenz von regulären Ausdrücken mit einem zusätzlichen
@@ -575,7 +575,7 @@
 \end{itemize}
 \smallskip
 
-In jedem Fall muss man (nicht-endliche) Verallgemeinerungen der Spiele betrachten,
+In jedem Fall muss man (nichtendliche) Verallgemeinerungen der Spiele betrachten,
 um die "`wahre"' Komplexität zu sehen\\ {\tiny(Menschen spielen nicht, indem sie
 innerlich eine endliche Datenbank aller möglichen Stellungen konsultieren)}
 \smallskip\pause
@@ -611,7 +611,7 @@
 \bigskip
 
 \anybox{yellow}{
-Was erwartet uns als nächstes?
+Was erwartet uns als Nächstes?
 \begin{itemize}
 \item Einführung in die Prädikatenlogik
 \item Entscheidbare logische Probleme
diff --git a/Vorlesungen/lecture-13.tex b/Vorlesungen/lecture-13.tex
index 315cac7..458e29c 100644
--- a/Vorlesungen/lecture-13.tex
+++ b/Vorlesungen/lecture-13.tex
@@ -54,7 +54,7 @@
 \alert{Vorlesung 14}\\
 Modelltheorie $\bullet$ Logisches Schließen\\[1ex]
 \alert{Vorlesung 15}\\
-Gleichheit $\bullet$ Unentscheidbarkeit der Schließens \\[1ex]
+Gleichheit $\bullet$ Unentscheidbarkeit des Schließens \\[1ex]
 \alert{Vorlesung 16}\\
 Ableitungskalküle $\bullet$ syntaktische Umformungen \\[1ex]
 \alert{Vorlesung 17}\\
@@ -201,7 +201,7 @@
 \item "`$\textsf{istMensch}(\textsf{sokrates})$"'
 \end{itemize}\bigskip\pause
 
-Dadurch können mehrere Dinge die selbe Eigenschaft haben:
+Dadurch können mehrere Dinge dieselbe Eigenschaft haben:
 \[ \text{istMensch}(\text{sokrates})\quad \text{istMensch}(\text{emilia})\quad \text{istMensch}(\text{anton})\quad\cdots\]
 
 \pause Für allgemeine Aussagen über die Dinge, die eine Eigenschaft haben, gibt es zwei
@@ -325,7 +325,7 @@
 Wir verzichten hier vorerst darauf, da
 \begin{itemize}
 \item dies die Definition komplexer (und eventuell verwirrender) macht,
-\item man damit keine zusätzliche Ausdruckstärke erhält und
+\item man damit keine zusätzliche Ausdrucksstärke erhält und
 \item wir diese Erweiterung für spezielle Anwendungen leicht auch später noch einführen können.
 \end{itemize}
 
@@ -380,13 +380,13 @@
 \defbox{Die \redalert{freien Vorkommen} von Variablen in einer Formel sind rekursiv wie folgt definiert:
 \begin{itemize}
 \item In einem Atom sind alle Vorkommen von Variablen frei.
-\item Die freien Vorkommen in $\neg F$ sind die selben wie in $F$
+\item Die freien Vorkommen in $\neg F$ sind dieselben wie in $F$
 \item Die freien Vorkommen in $(F\wedge G)$, $(F\vee G)$, $(F\to G)$ und
 $(F\leftrightarrow G)$ sind alle freien Vorkommen aus $F$ und $G$
-\item Die freien Vorkommen in $\forall x.F$ und $\exists x.F$ sind die 
-selben wie in $F$, ohne die Vorkommen von $x$ in $F$
+\item Die freien Vorkommen in $\forall x.F$ und $\exists x.F$ sind dieselben 
+wie in $F$, ohne die Vorkommen von $x$ in $F$
 \end{itemize}
-Damit sind Vorkommen von Variablen $x$ genau dann \redalert{gebunden}
+Damit sind Vorkommen von Variablen $x$ genau dann \redalert{gebunden},
 wenn sie im Bereich eines Quantors auftauchen.
 }\pause
 
@@ -426,7 +426,7 @@
 \alert{Dazu müssen drei Fragen beantwortet werden:}
 \begin{itemize}
 \item Was bedeutet $p$?\\
-	\visible<2->{Prädikatssymbole stehen für Relationen gleicher Stelligkeit}
+	\visible<2->{Prädikatensymbole stehen für Relationen gleicher Stelligkeit}
 \item Was bedeutet $a$?\\
 	\visible<3->{Konstanten stehen für Elemente, die in Relationen stehen \ghost{können}}
 \item Was bedeutet $x$?\\
@@ -630,7 +630,7 @@
 % \bigskip
 
 \anybox{yellow}{
-Was erwartet uns als nächstes?
+Was erwartet uns als Nächstes?
 \begin{itemize}
 \item Logisches Schließen
 \item Entscheidbare logische Probleme
diff --git a/Vorlesungen/lecture-14.tex b/Vorlesungen/lecture-14.tex
index 161867f..84b4ea9 100644
--- a/Vorlesungen/lecture-14.tex
+++ b/Vorlesungen/lecture-14.tex
@@ -488,7 +488,7 @@
 
 \theobox{\emph{Satz:} Semantische Äquivalenz entspricht wechselseitiger logischer Konsequenz:\\[1ex]
 % 
-\narrowcentering{ $F\equiv G$ \hspace{5mm}genau dann wenn\hspace{5mm} $F\models G$ und $G\models F$}
+\narrowcentering{ $F\equiv G$ \hspace{5mm}genau dann, wenn\hspace{5mm} $F\models G$ und $G\models F$}
 }
 
 Die Behauptungen folgen jeweils direkt aus den Definitionen.
@@ -668,7 +668,7 @@
 \bigskip\pause
 
 \examplebox{\emph{Beispiel:} Die De Morganschen Regeln gelten auch in der Prädikatenlogik, z.B.
-$\Inter,\Zuweisung\models \neg(F\wedge G)$ genau dann wenn
+$\Inter,\Zuweisung\models \neg(F\wedge G)$ genau dann, wenn
 $\Inter,\Zuweisung\models (\neg F\vee \neg G)$, das heißt
 $\neg(F\wedge G)\equiv (\neg F\vee \neg G)$.
 }
@@ -682,13 +682,13 @@
 Auch die folgenden Sätze gelten analog zur Aussagenlogik\\ (siehe Formale Systeme, Vorlesung 22):\bigskip
 
 \theobox{\emph{Satz (Deduktionstheorem):} Für jede Formelmenge $\mathcal{F}$ und Formeln $G$ und $H$ gilt\\
-$\mathcal{F}\models G\to H$ genau dann wenn $\mathcal{F}\cup\{G\}\models H$.}\bigskip
+$\mathcal{F}\models G\to H$ genau dann, wenn $\mathcal{F}\cup\{G\}\models H$.}\bigskip
 
-\theobox{\emph{Korollar:} $F\wedge G\models H$ genau dann wenn $F\models G\to H$.}\bigskip
+\theobox{\emph{Korollar:} $F\wedge G\models H$ genau dann, wenn $F\models G\to H$.}\bigskip
 
-\theobox{\emph{Korollar:} $F\equiv G$ genau dann wenn $\models F\leftrightarrow G$.}\bigskip
+\theobox{\emph{Korollar:} $F\equiv G$ genau dann, wenn $\models F\leftrightarrow G$.}\bigskip
 
-\redalert{Dennoch sind $\models$ und $\equiv$ nicht das selbe wie $\to$ und $\leftrightarrow$:}
+\redalert{Dennoch sind $\models$ und $\equiv$ nicht dasselbe wie $\to$ und $\leftrightarrow$:}
 \begin{itemize}
 \item $\models$ und $\equiv$ können sich auch auf (möglicherweise unendliche) Mengen von Formeln beziehen
 \item $\to$ und $\leftrightarrow$ sind syntaktische Operatoren und können (eventuell geschachtelt) in Formeln auftreten
@@ -742,7 +742,7 @@
 F\wedge (F\vee G) & \equiv F\\
 F\vee (F\wedge G) & \equiv F
 \end{split}
-		& \text{\textcolor{devilscss}{Absorbtion}}
+		& \text{\textcolor{devilscss}{Absorption}}
 \end{align*}
 
 \end{frame}
@@ -802,7 +802,7 @@
 	\end{itemize}
 \end{itemize}
 
-Deshalb kann man nullstellige Prädikate wie aussagenlogsiche Atome verwenden
+Deshalb kann man nullstellige Prädikate wie aussagenlogische Atome verwenden
 \bigskip
 
 In diesem Sinne ist die Aussagenlogik ein Teil der Prädikatenlogik
@@ -840,13 +840,13 @@
 % Die Modelltheorie der Prädikatenlogik basiert auf Interpretationen und Zuweisungen, aber bei Sätzen reichen Interpretationen
 % \bigskip
 
-Logisches Schließen ist die Berechnung (Überprüfung) einzelner Beziehungen der Form $\Inter\models F$ (Model checking) bzw. $F\models G$ (Schlussfolgerung)\bigskip
+Logisches Schließen ist die Berechnung (Überprüfung) einzelner Beziehungen der Form $\Inter\models F$ (Model Checking) bzw. $F\models G$ (Schlussfolgerung)\bigskip
 
 Prädikatenlogik verallgemeinert Aussagenlogik und viele der dort gültigen Gesetze
 \bigskip
 
 \anybox{yellow}{
-Was erwartet uns als nächstes?
+Was erwartet uns als Nächstes?
 \begin{itemize}
 \item Logisches Schließen: (Un)Entscheidbarkeit und Komplexität
 \item Resolution für Prädikatenlogik
diff --git a/Vorlesungen/lecture-15.tex b/Vorlesungen/lecture-15.tex
index 9ab74cb..b5c3c61 100644
--- a/Vorlesungen/lecture-15.tex
+++ b/Vorlesungen/lecture-15.tex
@@ -197,7 +197,7 @@
 \emph{Warum ist das nützlich?}
 \begin{itemize}
 \item Logisches Schließen kann auf den Test von Erfüllbarkeit zurückgeführt werden
-\item Erfüllbarkeit bleibt erhalten, wenn man "`eingebaute"' Gleicheit durch eine logische 
+\item Erfüllbarkeit bleibt erhalten, wenn man "`eingebaute"' Gleichheit durch eine logische 
 Beschreibung von Gleichheit ersetzt
 \end{itemize}
 \redalert{$\leadsto$ Schließen wird durch Gleichheit nicht wesentlich komplizierter}
@@ -232,7 +232,7 @@
 \theobox{\emph{Satz:} Sei $\mathcal{T}$ eine Theorie der Prädikatenlogik mit $\approx$
 und weiteren Prädikatensymbolen aus der endlichen Menge $\Slang{R}$.\medskip
 
-Dann ist $\mathcal{T}$ genau dann in der Prädikatenlogik mit Gleichheit erfüllbar wenn $\mathcal{T}_{\eqpred}\cup\mathcal{EQ}_{\Slang{R}}$ in der Prädikatenlogik ohne Gleichheit erfüllbar ist.
+Dann ist $\mathcal{T}$ genau dann in der Prädikatenlogik mit Gleichheit erfüllbar, wenn $\mathcal{T}_{\eqpred}\cup\mathcal{EQ}_{\Slang{R}}$ in der Prädikatenlogik ohne Gleichheit erfüllbar ist.
 }
 
 \emph{Beweis:} "`$\Leftarrow$"' Nehmen wir an, $\mathcal{T}_{\eqpred}\cup\mathcal{EQ}_{\Slang{R}}$ ist erfüllbar.\pause
@@ -267,11 +267,11 @@
 
 Wir wollen zeigen, dass $\Inter\models\mathcal{T}$ in der Prädikatenlogik mit Gleichheit gilt.\footnote{\tiny Verständnischeck: Klingt das plausibel? Sogar offensichtlich? Gut. Warum genau?}\pause\medskip
 
-\alert{Wir zeigen eine allgemeinere Behauptung:}\only<2->{\footnote{\tiny Mathematische Taktik: Scheint ein Beweis zu schwer, dann beweise etwas stärkeres!}}
+\alert{Wir zeigen eine allgemeinere Behauptung:}\only<2->{\footnote{\tiny Mathematische Taktik: Scheint ein Beweis zu schwer, dann beweise etwas Stärkeres!}}
 \begin{itemize}
 \item Für eine Zuweisung $\Zuweisung$ für $\Jnter$ definieren wir eine Zuweisung $\Zuweisung'$ für $\Inter$ wie folgt: $\Zuweisung'(x)\defeq[\Zuweisung(x)]$ für alle $x\in\Slang{V}$
 \item Wir behaupten: Für jede Formel $F$ der Prädikatenlogik mit Gleichheit und jede Zuweisung $\Zuweisung$ für $\Jnter$ gilt
-\[ \Jnter,\Zuweisung\models F_{\eqpred} \text{ genau dann wenn } \Inter,\Zuweisung'\models F \]
+\[ \Jnter,\Zuweisung\models F_{\eqpred} \text{ genau dann, wenn } \Inter,\Zuweisung'\models F \]
 \item Daraus folgt wie gewünscht $\Inter\models\mathcal{T}$, weil $\mathcal{T}$ abgeschlossen ist (Zuweisung irrelevant) und $\Jnter\models\mathcal{T}_{\eqpred}$
 % 
 % \item Wir wollen zeigen, dass $\Inter\models\mathcal{T}$ in der Prädikatenlogik mit Gleichheit gilt\\
@@ -296,19 +296,19 @@
 
 \emph{Beweis:} {\footnotesize(Forts.)}
 Wir behaupten: Für jede Formel $F$ der Prädikatenlogik mit Gleichheit und jede Zuweisung $\Zuweisung$ für $\Jnter$ gilt
-\[ \Jnter,\Zuweisung\models F_{\eqpred} \text{ genau dann wenn } \Inter,\Zuweisung'\models F \]
+\[ \Jnter,\Zuweisung\models F_{\eqpred} \text{ genau dann, wenn } \Inter,\Zuweisung'\models F \]
 Wie kann man so eine Behauptung zeigen?\bigskip\pause
 
 $\leadsto$ \alert{Induktion über den Aufbau von Formeln}\bigskip
 
 \emph{Induktionsanfang:} Für atomare Formeln $F=p(t_1,\ldots,t_n)$ mit $p\neq{\approx}$ gilt die Behauptung,
-weil für all $\delta_1,\ldots,\delta_n\in\Delta^\Jnter$ gilt:
-\[ \tuple{\delta_1,\ldots,\delta_n}\in p^\Jnter \text{ genau dann wenn } \tuple{[\delta_1],\ldots,[\delta_n]}\in p^\Inter \]
+weil für alle $\delta_1,\ldots,\delta_n\in\Delta^\Jnter$ gilt:
+\[ \tuple{\delta_1,\ldots,\delta_n}\in p^\Jnter \text{ genau dann, wenn } \tuple{[\delta_1],\ldots,[\delta_n]}\in p^\Inter \]
 $\Rightarrow$ folgt direkt aus der Definition von $p^\Inter$\\
-$\Leftarrow$ folgt weil $\Jnter\models\mathcal{EQ}_{\Slang{R}}$, so dass $\eqpred^\Jnter$ eine Kongruenzrelation ist
+$\Leftarrow$ folgt, weil $\Jnter\models\mathcal{EQ}_{\Slang{R}}$, so dass $\eqpred^\Jnter$ eine Kongruenzrelation ist
 \bigskip\pause
 
-Für atomare Formeln $F=(t_1\approx t_2)$ gilt die Behauptung ebenfalls, da $[\delta]=[\epsilon]$ genau dann wenn $\tuple{\delta,\epsilon}\in\eqpred^\Jnter$.
+Für atomare Formeln $F=(t_1\approx t_2)$ gilt die Behauptung ebenfalls, da $[\delta]=[\epsilon]$ genau dann, wenn $\tuple{\delta,\epsilon}\in\eqpred^\Jnter$.
 \end{frame}
 
 \begin{frame}[t]\frametitle{Beweis (5)}
@@ -316,7 +316,7 @@
 
 \emph{Beweis:} {\footnotesize(Forts.)}
 Wir behaupten: Für jede Formel $F$ der Prädikatenlogik mit Gleichheit und jede Zuweisung $\Zuweisung$ für $\Jnter$ gilt
-\[ \Jnter,\Zuweisung\models F_{\eqpred} \text{ genau dann wenn } \Inter,\Zuweisung'\models F \]
+\[ \Jnter,\Zuweisung\models F_{\eqpred} \text{ genau dann, wenn } \Inter,\Zuweisung'\models F \]
 % Wie kann man so eine Behauptung zeigen?\bigskip\pause
 
 % $\leadsto$ \alert{Induktion} (über den Aufbau von Formeln)\bigskip
@@ -346,10 +346,10 @@
 Die gezeigte Variante von Induktion heißt \redalert{strukturelle Induktion}
 \begin{itemize}
 \item \alert{Klassische Induktion:} Ist $E$ eine Eigenschaft, so dass gilt:
-(1) die Zahl $0$ hat $E$ und (2) eine natürliche Zahl $n>0$ hat $E$ falls ihr Vorgänger $n-1$ $E$ hat;
+(1) die Zahl $0$ hat $E$ und (2) eine natürliche Zahl $n>0$ hat $E$, falls ihr Vorgänger $n-1$ $E$ hat;
 dann haben alle natürlichen Zahlen die Eigenschaft $E$.
 \item \alert{Strukturelle Induktion auf Formeln:} Ist $E$ eine Eigenschaft, so dass gilt:
-(1) atomare Formeln haben $E$ und (2) eine nicht-atomare Formel $F$ hat $E$ falls ihre maximalen echten Teilformeln $E$ haben;
+(1) atomare Formeln haben $E$ und (2) eine nichtatomare Formel $F$ hat $E$, falls ihre maximalen echten Teilformeln $E$ haben;
 dann haben alle Formeln die Eigenschaft $E$.
 \end{itemize}
 Allgemein kann man Induktion über jede induktiv definierte syntaktische Struktur durchführen (Formeln, Terme, Programme, \ghost{\ldots)}\medskip\pause
@@ -644,7 +644,7 @@
 es entspricht verschiedenen konkreten Fragen (Folgerung, Erfüllbarkeit, Allgemeingültigkeit)
 \bigskip
 
-Logisches Schließen über logischen Aussagem mit Gleichheit kann
+Logisches Schließen über logischen Aussagen mit Gleichheit kann
 auf logisches Schließen ohne Gleichheit reduziert werden\bigskip
 
 Strukturelle Induktion ist eine wichtige Beweismethode, um mit wenigen (endlich vielen) Schritten zu zeigen, dass eine Eigenschaft für alle (unendlich vielen) Formeln gilt\bigskip
@@ -655,7 +655,7 @@
 % (noch zu zeigen)
 
 \anybox{yellow}{
-Was erwartet uns als nächstes?
+Was erwartet uns als Nächstes?
 \begin{itemize}
 \item Unentscheidbarkeit des logischen Schließens
 \item Ein konkretes Verfahren zum logischen Schließen
diff --git a/Vorlesungen/lecture-16.tex b/Vorlesungen/lecture-16.tex
index c99ba5f..9bc6899 100644
--- a/Vorlesungen/lecture-16.tex
+++ b/Vorlesungen/lecture-16.tex
@@ -13,7 +13,7 @@
 
 \emph{Erinnerung:} $F$ ist logische Konsequenz von $G$, wenn alle Modelle von $F$ auch Modelle von $G$ sind.
 \begin{itemize}
-\item Es ist nicht offensichtlich, wie man das überprüfen sollte, denn es gibt unendliche viele Modelle
+\item Es ist nicht offensichtlich, wie man das überprüfen sollte, denn es gibt unendlich viele Modelle
 \item Ebenso schwer erscheinen die gleichwertigen Probleme der Erfüllbarkeit und Allgemeingültigkeit
 \end{itemize}\pause
 \emph{Intuition:} prädikatenlogisches Schließen ist unentscheidbar
@@ -183,7 +183,7 @@
 \item Für jedes Terminalsymbol $\Sterm{a}$:
 \[\forall x.\exists y. p_{\Sterm{a}}(x,y)\]
 \end{itemize}
-Dann gilt $\mathcal{T}\models\exists x,y. (p_{\Sntermsub{S}{1}}(x,y)\wedge p_{\Sntermsub{S}{2}}(x,y))$ genau dann wenn es ein Wort $w\in\Slang{L}(G_1)\cap\Slang{L}(G_2)$ gibt.
+Dann gilt $\mathcal{T}\models\exists x,y. (p_{\Sntermsub{S}{1}}(x,y)\wedge p_{\Sntermsub{S}{2}}(x,y))$ genau dann, wenn es ein Wort $w\in\Slang{L}(G_1)\cap\Slang{L}(G_2)$ gibt.
 \bigskip
 
 Die Unentscheidbarkeit von Erfüllbarkeit und Allgemeingültigkeit folgt, weil man logische Konsequenz auf diese Probleme reduzieren kann.
@@ -200,7 +200,7 @@
 
 Umgekehrt kann man aus dem Beweis noch stärkere Ergebnisse folgern, z.B.:
 
-\theobox{\emph{Korollar:} Logisches Schließen (Erfüllbarkeit, Allgemeingültigkeit, logische Konsequenz) in der Prädikatenlogik ist unentscheidbar, selbst dann, wenn nur binäre Prädikatssymbole verwendet werden.}\bigskip
+\theobox{\emph{Korollar:} Logisches Schließen (Erfüllbarkeit, Allgemeingültigkeit, logische Konsequenz) in der Prädikatenlogik ist unentscheidbar, selbst dann, wenn nur binäre Prädikatensymbole verwendet werden.}\bigskip
 
 \end{frame}
 
@@ -299,11 +299,11 @@
 
 \begin{frame}\frametitle{Theorie und Praxis}
 
-Gödel zeigte damit auch die Semientscheidbarkeit des logischen Schließens:
+Gödel zeigte damit auch die Semi-Entscheidbarkeit des logischen Schließens:
 \begin{itemize}
 \item Man kann systematisch alle möglichen Ableitungen neuer Tautologien
 bilden
-\item Eine Formel ist eine Tautologie genau dann wenn sie irgendwann abgeleitet wird
+\item Eine Formel ist eine Tautologie genau dann, wenn sie irgendwann abgeleitet wird
 \item Ist eine Formel keine Tautologie, dann werden wir es auf diese Art nie erfahren
 \end{itemize}\pause
 
@@ -313,7 +313,7 @@
 
 \alert{Geht es besser?}\pause
 \begin{itemize}
-\item Logischen Schließens ist unentscheidbar: kein Verfahren kann die Frage nach Allgemeingültigkeit sicher beantworten
+\item Logisches Schließen ist unentscheidbar: kein Verfahren kann die Frage nach Allgemeingültigkeit sicher beantworten
 \item Aber: Es gibt effizientere, zielgerichtetere Methoden
 \end{itemize}
 
@@ -345,7 +345,7 @@
 \begin{enumerate}[(1)]
 \item Umformung in Klauselform
 \item Durchführung von Resolutionsschritten, bei denen jeweils zwei Klauseln kombiniert werden
-\item Terminierung wenn leere Klausel auftritt oder keine neuen Klauseln mehr entstehen
+\item Terminierung, wenn leere Klausel auftritt oder keine neuen Klauseln mehr entstehen
 \end{enumerate}
 \bigskip
 
@@ -365,7 +365,7 @@
 Wir haben bereits gelernt (Vorlesung 14):
 \begin{itemize}
 \item In prädikatenlogischen Formeln darf man Teilformeln durch semantisch äquivalente
-Formeln ersetzten (Ersetzungstheorem)
+Formeln ersetzen (Ersetzungstheorem)
 \item Für die aussagenlogischen Junktoren gelten die gleichen Äquivalenzen wie in der Aussagenlogik
 \end{itemize}
 $\leadsto$ damit kann man schon viele Umformungen vornehmen
@@ -377,7 +377,7 @@
 
 \begin{frame}\frametitle{Äquivalenzen mit Quantoren}
 
-Es gelten die folgenen Beziehungen:
+Es gelten die folgenden Beziehungen:
 \begin{align*}
 \begin{split}
 \neg\exists x.F &\equiv \forall x.\neg F\\
@@ -391,8 +391,8 @@
 \end{split}
 & \text{\textcolor{devilscss}{Kommutativität}}\\[1ex]
 %
-\exists x.(F\vee G) &\equiv (\exists x.F\vee \exists x.G) & \text{\textcolor{devilscss}{Distributitivität $\exists$/$\vee$}}\\
-\forall x.(F\wedge G) &\equiv (\forall x.F\wedge \forall x.G) & \text{\textcolor{devilscss}{Distributitivität $\forall$/$\wedge$}}
+\exists x.(F\vee G) &\equiv (\exists x.F\vee \exists x.G) & \text{\textcolor{devilscss}{Distributivität $\exists$/$\vee$}}\\
+\forall x.(F\wedge G) &\equiv (\forall x.F\wedge \forall x.G) & \text{\textcolor{devilscss}{Distributivität $\forall$/$\wedge$}}
 \end{align*}
 
 \pause\emph{Beweis:} Die Beweise ergeben sich direkt aus der Semantik, z.B.:\bigskip
@@ -408,7 +408,7 @@
 
 \end{frame}
 
-\begin{frame}\frametitle{Nicht-Äquivalenzen mit Quantoren}
+\begin{frame}\frametitle{Nichtäquivalenzen mit Quantoren}
 
 Andere ähnliche Beziehungen gelten \redalert{nicht}.\bigskip\pause
 
@@ -436,7 +436,7 @@
 \end{enumerate}
 }\medskip
 
-Formeln, die negierte oder nicht-negierte Atome sind, nennt man \redalert{Literale}.
+Formeln, die negierte oder nichtnegierte Atome sind, nennt man \redalert{Literale}.
 In NNF darf Negation also nur in Literalen auftauchen.
 \medskip\pause
 
@@ -455,7 +455,7 @@
 Es ist möglich, eine Formel rekursiv in NNF umzuformen.
 \medskip
 
-Dazu ersetzten wir zunächst alle Vorkommen von $\to$ und $\leftrightarrow$ 
+Dazu ersetzen wir zunächst alle Vorkommen von $\to$ und $\leftrightarrow$ 
 unter Verwendung der bekannten Äquivalenzen:
 %
 \begin{align*}
@@ -704,7 +704,7 @@
 Mithilfe semantischer Äquivalenzen kann man beliebige Formeln in einheitliche Normalformen überführen.\bigskip
 
 \anybox{yellow}{
-Was erwartet uns als nächstes?
+Was erwartet uns als Nächstes?
 \begin{itemize}
 \item Funktionen
 \item Resolution
diff --git a/Vorlesungen/lecture-17.tex b/Vorlesungen/lecture-17.tex
index b44a05f..1764fa3 100644
--- a/Vorlesungen/lecture-17.tex
+++ b/Vorlesungen/lecture-17.tex
@@ -34,7 +34,7 @@
 
 \begin{frame}\frametitle{Bereinigte Formeln}
 
-\defbox{Eine Formel $F$ ist \redalert{bereinigt} wenn sie die folgenden beiden Eigenschaften hat:
+\defbox{Eine Formel $F$ ist \redalert{bereinigt}, wenn sie die folgenden beiden Eigenschaften hat:
 \begin{enumerate}[(1)]
 \item Keine Variable in $F$ kommt sowohl frei als auch gebunden vor
 \item Keine Variable in $F$ wird in mehr als einem Quantor gebunden
@@ -232,7 +232,7 @@
 Daraus folgt insbesondere auch, dass jeder einen Vater hat.
 }\medskip
 
-Um das zu formalisieren müssen wir zunächst Funktionssymbole in die Logik einführen.
+Um das zu formalisieren, müssen wir zunächst Funktionssymbole in die Logik einführen.
 
 \end{frame}
 
@@ -251,7 +251,7 @@
 
 Mit Funktionssymbolen lassen sich komplexere Terme konstruieren:
 \defbox{Ein \redalert{Term} der Prädikatenlogik mit Funktionen ist jeder Ausdruck $t$, der
-eine der folgenden rekursiven Bedinungen erfüllt:
+eine der folgenden rekursiven Bedingungen erfüllt:
 \begin{itemize}
 \item $t\in\Slang{V}\cup\Slang{C}$, d.h. $t$ ist eine Variable oder eine Konstante
 \item $t=f(t_1,\ldots,t_n)$, wobei $f\in\Slang{F}$ ein $n$-stelliges Funktionssymbol ist
@@ -431,7 +431,7 @@
 \begin{frame}\frametitle{Zusammenfassung: Funktionen}
 
 Die folgenden Varianten von Prädikatenlogik haben also in gewissem Sinne die \alert{gleiche
-Ausdruckstärke:}
+Ausdrucksstärke:}
 \begin{itemize}
 \item Prädikatenlogik (ohne Funktionssymbole)
 \item Prädikatenlogik mit Funktionssymbolen
@@ -484,7 +484,7 @@
 wobei die Formeln $L_{i,j}$ Literale sind. Eine Disjunktion von Literalen heißt \redalert{Klausel}.
 }\medskip
 
-(Zur Erinnerung: \redalert{Literale} = negierte oder nicht-negierte Atome)
+(Zur Erinnerung: \redalert{Literale} = negierte oder nichtnegierte Atome)
 \bigskip
 
 $\leadsto$ Die gleiche Form kann für den quantorenfreien inneren Teil jeder Formel in Pränexform hergestellt werden.
@@ -505,7 +505,7 @@
 \end{align*}
 \end{enumerate}\pause
 
-\theobox{\emph{Satz:} Die so aus einer Formel $F$ gebildete KNF ist erfüllbar genau dann wenn $F$ erfüllbar ist.}
+\theobox{\emph{Satz:} Die so aus einer Formel $F$ gebildete KNF ist erfüllbar genau dann, wenn $F$ erfüllbar ist.}
 
 \emph{Beweis:} Schritte (1)--(3) liefern semantisch äquivalente Formeln. Schritt (4) liefert eine erfüllbarkeitsäquivalente Formel. Schritt (5) liefert eine zu dieser semantisch äquivalente Formel.\qed\medskip
 
@@ -589,7 +589,7 @@
 \bigskip
 
 \anybox{yellow}{
-Was erwartet uns als nächstes?
+Was erwartet uns als Nächstes?
 \begin{itemize}
 \item Herbrand, genialer Mathematiker aber unglücklicher Bergsteiger
 \item Unifikation und Resolution
diff --git a/Vorlesungen/lecture-18.tex b/Vorlesungen/lecture-18.tex
index 043b927..f833dc7 100644
--- a/Vorlesungen/lecture-18.tex
+++ b/Vorlesungen/lecture-18.tex
@@ -216,7 +216,7 @@
 }
 \]
 Passen $\textsf{hatVater}(x,f(x))$ und $\neg\textsf{hatVater}(z,v)$ zusammen?\\\pause
-\redalert{Ja}, wenn wir $z$ durch $x$ ersetzten und $v$ durch $f(x)$, denn es gilt:
+\redalert{Ja}, wenn wir $z$ durch $x$ ersetzen und $v$ durch $f(x)$, denn es gilt:
 
 ~\hspace{-1cm}%
 \begin{minipage}{8cm}
@@ -237,11 +237,11 @@
 
 \begin{frame}\frametitle{Zusammenfassung und Verallgemeinerung}
 
-Für die Anwendung von Resolution benötigt man jeweils zwei gleiche Atome\\ (einmal negiert und einmal nicht-negiert)\medskip
+Für die Anwendung von Resolution benötigt man jeweils zwei gleiche Atome\\ (einmal negiert und einmal nichtnegiert)\medskip
 
 Wir erreichen das in Prädikatenlogik durch folgende Methoden:
 \begin{itemize}
-\item Wir ersetzten (universell quantifizierte) Variablen durch andere Terme $\leadsto$~\redalert{Substitution}
+\item Wir ersetzen (universell quantifizierte) Variablen durch andere Terme $\leadsto$~\redalert{Substitution}
 \item Damit wollen wir erreichen, dass Terme (und letztlich Atome) gleich werden $\leadsto$~\redalert{Unifikation}
 \end{itemize}
 
@@ -298,7 +298,7 @@
 \defbox{Ein \redalert{Unifikationsproblem} ist eine endliche Menge von Gleichungen
 der Form \mbox{$G=\{s_1\unieq t_1,\ldots,s_n\unieq t_n\}$}.\medskip
 
-Eine Substitution $\sigma$ ist ein \redalert{Unifikator} für $G$ falls
+Eine Substitution $\sigma$ ist ein \redalert{Unifikator} für $G$, falls
 $s_i\sigma=t_i\sigma$ für alle $i\in\{1,\ldots,n\}$ gilt.
 }\pause 
 
@@ -342,7 +342,7 @@
 (ohne Beweis)\medskip\pause
 
 \examplebox{\emph{Beispiel:} Das Problem $\{f(x)\unieq f(z)\}$ hat die allgemeinsten Unifikatoren
-$\{x\mapsto z\}$ und $\{z\mapsto x\}$, aber auch z.B. $\{x\mapsto v,z\mapsto v\}$ ($v\in\Slang{V}$). Dagegen ist $\{x\mapsto a,z\mapsto a\}$ mit $a\in\Slang{C}$ ein nicht-allgemeinster Unifikator.}\bigskip\pause
+$\{x\mapsto z\}$ und $\{z\mapsto x\}$, aber auch z.B. $\{x\mapsto v,z\mapsto v\}$ ($v\in\Slang{V}$). Dagegen ist $\{x\mapsto a,z\mapsto a\}$ mit $a\in\Slang{C}$ ein nichtallgemeinster Unifikator.}\bigskip\pause
 
 \theobox{\emph{Satz:} Wenn ein Unifikationsproblem lösbar ist (d.h., einen Unifikator hat), dann hat es auch einen allgemeinsten Unifikator.}
 
@@ -432,7 +432,7 @@
 % \theobox{Satz: Der Unifikationsalgorithmus berechnet für jedes Unifikationsproblem
 % einen allgemeinsten Unifikator, falls es einen Unifikator gibt, und liefert "`nicht unifizierbar"' wenn es keinen gibt.}
 
-\emph{Beweis (Fortsetz.):} Als erstes zeigen wir eine Hilfsaussage ($\ddagger$):\\[1ex]
+\emph{Beweis (Fortsetz.):} Als Erstes zeigen wir eine Hilfsaussage ($\ddagger$):\\[1ex]
 Wenn ein Unifikationsproblem $G_1$ in einem Ersetzungsschritt in ein Problem $G_2$
 umgewandelt werden kann, dann haben $G_1$ und $G_2$ die gleichen Unifikatoren.
 \bigskip\pause
@@ -660,7 +660,7 @@
 \bigskip
 
 \anybox{yellow}{
-Was erwartet uns als nächstes?
+Was erwartet uns als Nächstes?
 \begin{itemize}
 \item Der Resolutionsalgorithmus und seine Korrektheit
 \item Herbrand, genialer Mathematiker aber unglücklicher Bergsteiger
diff --git a/Vorlesungen/lecture-19.tex b/Vorlesungen/lecture-19.tex
index d1bb50b..02d218b 100644
--- a/Vorlesungen/lecture-19.tex
+++ b/Vorlesungen/lecture-19.tex
@@ -85,7 +85,7 @@
 \emph{Beobachtungen:}
 \begin{itemize}
 \item Eine Menge von Atomen $\mathcal{A}$ ist nur dann unifizierbar, wenn alle Atome das gleiche Prädikat verwenden, d.h. wenn es ein $\ell$-stelliges Prädikatensymbol $p$ gibt, so dass $A_i=p(t_{i,1},\ldots,t_{i,\ell})$ für alle $i\in\{1,\ldots,n\}$.
-\item Dann ist $\sigma$ genau dann ein Unifikator für $\mathcal{A}$ wenn
+\item Dann ist $\sigma$ genau dann ein Unifikator für $\mathcal{A}$, wenn
 $\sigma$ Unifikator für das folgende Unifikationsproblem $G_{\mathcal{A}}$ ist: 
 \[ \{ t_{1,1}\unieq t_{2,1},\ldots,t_{n-1,1}\unieq t_{n,1},\ldots,t_{1,\ell}\unieq t_{2,\ell},\ldots,t_{n-1,\ell}\unieq t_{n,\ell} \} \]
 \item Insbesondere ist der allgemeinste Unifikator für $G_{\mathcal{A}}$ auch der allgemeinste Unifikator für $\mathcal{A}$
@@ -159,8 +159,8 @@
 \redalert{Problem:}\hspace{-2mm}%
 \begin{minipage}[t]{8.5cm}\footnotesize\vspace{-2ex}
 \begin{itemize}
-\item $\neg L(f_7(x_1,x_2,x_3,x_4,a))$ bedeutet "`es gibt Nicht-Lügner"' (bezeichnet mit Termen der Form $f_7(x_1,x_2,x_3,x_4,a)$)\\[-2ex]
-\item Dies sollte z.B. mit (1) "`Jeder Nicht-Lügner ist Wahrheitssager"' resolvieren\\[-2ex]
+\item $\neg L(f_7(x_1,x_2,x_3,x_4,a))$ bedeutet "`es gibt Nichtlügner"' (bezeichnet mit Termen der Form $f_7(x_1,x_2,x_3,x_4,a)$)\\[-2ex]
+\item Dies sollte z.B. mit (1) "`Jeder Nichtlügner ist Wahrheitssager"' resolvieren\\[-2ex]
 \item Aber $\{L(f_7(x_1,x_2,x_3,x_4,a)), L(x_1)\}$ hat keinen Unifikator
 \end{itemize}
 \end{minipage}
@@ -185,7 +185,7 @@
 Daher darf man die Variablen jeder Klausel einheitlich umbenennen, unabhängig von jeder anderen Klausel, z.B.
 \[ \{\neg L(f_7(x_1,x_2,x_3,x_4,a))\} \quad\leadsto\quad \{\neg L(f_7(x'_1,x'_2,x'_3,x'_4,a))\} \]
 Klauseln, die durch eineindeutige Umbenennung von Variablen entstanden sind, nennt man \redalert{Varianten} (einer Klausel)\\[0.5ex]
-\alert{$\leadsto$ Wir bilden bei der Resolution Varianten um Konflikte von Variablen zu vermeiden}
+\alert{$\leadsto$ Wir bilden bei der Resolution Varianten, um Konflikte von Variablen zu vermeiden}
 
 \end{frame}
 
@@ -314,7 +314,7 @@
 \item \emph{Fall 2:} $\Inter,\Zuweisung\not\models A_1\sigma$ ($=A_2\sigma=\ldots=A'_m\sigma)$.\\ Dann gilt $\Inter,\Zuweisung\models L_1\sigma\vee\ldots\vee L_k\sigma$, und damit $\Inter,\Zuweisung\models K$\pause
 \item Also gilt $\Inter\models\forall K$.
 \end{itemize}
-Da $\Inter$ beliebig ist gilt also $\forall K_1\wedge\forall K_2\models \forall K$.\\
+Da $\Inter$ beliebig ist, gilt also $\forall K_1\wedge\forall K_2\models \forall K$.\\
 Das heißt, jede Resolvente ist logische Konsequenz der resolvierten Klauseln.
 
 \end{frame}
@@ -395,11 +395,11 @@
 
 \end{frame}
 
-\begin{frame}\frametitle{Herbranduniversum}
+\begin{frame}\frametitle{Herbrand-Universum}
 
 Der Kern von Herbrands Idee ist eine "`syntaktische"' Domäne:\medskip
 
-\defbox{Sei $a$ eine beliebige Konstante. Das \redalert{Herbranduniversum} $\Delta_F$ für eine Formel $F$ ist die
+\defbox{Sei $a$ eine beliebige Konstante. Das \redalert{Herbrand-Universum} $\Delta_F$ für eine Formel $F$ ist die
 Menge aller variablenfreien Terme, die man mit Konstanten und Funktionssymbolen in $F$ und der zusätzlichen Konstante $a$ bilden kann:
 \begin{itemize}
 \item $a\in\Delta_F$
@@ -410,22 +410,22 @@
 
 \emph{Anmerkung:} Das Herbrand-Universum ist immer abzählbar, manchmal endlich und niemals leer.\pause
 
-\examplebox{Beispiel: Für die Formel $F=p(f(x),y,g(z))$ ergibt sich das Herbranduniversum
+\examplebox{Beispiel: Für die Formel $F=p(f(x),y,g(z))$ ergibt sich das Herbrand-Universum
 $\Delta_F=\{a,f(a),g(a),f(f(a)),f(g(a)),g(f(a)),g(g(a)),\ldots\}$.
 }
 
 \end{frame}
 
-\begin{frame}\frametitle{Herbrandinterpretationen}
+\begin{frame}\frametitle{Herbrand-Interpretationen}
 
 Mit dem Herbrand-Universum als Domäne kann man Interpretationen definieren, die Terme "`durch sich selbst"' interpretieren:\medskip
 
-\defbox{Eine \redalert{Herbrandinterpretation} für eine Formel $F$ ist eine Interpretation $\Inter$ für die gilt:
+\defbox{Eine \redalert{Herbrand-Interpretation} für eine Formel $F$ ist eine Interpretation $\Inter$ für die gilt:
 \begin{itemize}
 \item $\Delta^\Inter=\Delta_F$ ist das Herbrand-Universum von $F$
 \item Für jeden Term $t\in\Delta_F$ gilt $t^\Inter=t$
 \end{itemize}
-$\Inter$ ist ein \redalert{Herbrandmodell} für $F$ wenn zudem gilt $\Inter\models F$.}
+$\Inter$ ist ein \redalert{Herbrand-Modell} für $F$, wenn zudem gilt $\Inter\models F$.}
 
 \emph{Anmerkung:} Die Definition stellt Bedingungen an Grundbereich und Terminterpretation, aber sie lässt auch viele Freiheiten (z.B. die Interpretation von Prädikatensymbolen)
 
@@ -435,22 +435,22 @@
 
 Betrachten wir wieder die (skolemisierte) Formel $F=\forall x.\textsf{hatVater}(x,f(x))$.\bigskip
 
-Herbranduniversum: $\Delta_F=\{a,f(a),f(f(a)),\ldots\}$\medskip
+Herbrand-Universum: $\Delta_F=\{a,f(a),f(f(a)),\ldots\}$\medskip
 
-Alle Herbrandinterpretationen stimmen auf der Domäne und (dem relevanten Teil) der Terminterpretation überein.
+Alle Herbrand-Interpretationen stimmen auf der Domäne und (dem relevanten Teil) der Terminterpretation überein.
 \begin{itemize}
-\item $\Inter_1$ mit $\textsf{hatVater}^{\Inter_1}=\emptyset$ ist kein Herbrandmodell
-\item $\Inter_2$ mit $\textsf{hatVater}^{\Inter_2}=\{\tuple{t,f(t)}\mid t\in\Delta_F\}$ ist ein Herbrandmodell
-\item $\Inter_3$ mit $\textsf{hatVater}^{\Inter_3}=\Delta_F\times\Delta_F$ ist ein Herbrandmodell
+\item $\Inter_1$ mit $\textsf{hatVater}^{\Inter_1}=\emptyset$ ist kein Herbrand-Modell
+\item $\Inter_2$ mit $\textsf{hatVater}^{\Inter_2}=\{\tuple{t,f(t)}\mid t\in\Delta_F\}$ ist ein Herbrand-Modell
+\item $\Inter_3$ mit $\textsf{hatVater}^{\Inter_3}=\Delta_F\times\Delta_F$ ist ein Herbrand-Modell
 \end{itemize}
 
 \end{frame}
 
 \begin{frame}\frametitle{Syntax vs. Semantik}
 
-Bei Herbrandinterpretationen kann man semantische Elemente (wie sie in Zuweisungen vorkommen) durch syntaktische Elemente (wie sie in Substitutionen vorkommen) ausdrücken:\medskip
+Bei Herbrand-Interpretationen kann man semantische Elemente (wie sie in Zuweisungen vorkommen) durch syntaktische Elemente (wie sie in Substitutionen vorkommen) ausdrücken:\medskip
 
-\theobox{\emph{Lemma:} Für jede Herbrandinterpretation $\Inter$, jede Zuweisung $\Zuweisung$ für $\Inter$, jeden Term $t\in\Delta^\Inter$ und jede Formel $F$ gilt:
+\theobox{\emph{Lemma:} Für jede Herbrand-Interpretation $\Inter$, jede Zuweisung $\Zuweisung$ für $\Inter$, jeden Term $t\in\Delta^\Inter$ und jede Formel $F$ gilt:
 \[ \Inter,\Zuweisung\{x\mapsto t\} \models F \qquad \text{gdw.}\qquad \Inter,\Zuweisung \models F\{x\mapsto t\}\]}
 
 (ohne Beweis; einfach)
@@ -463,22 +463,22 @@
 \begin{frame}\frametitle{Erfüllbar + Skolem = Erfüllbarkeit bei Herbrand}
 
 \theobox{\emph{Satz:} Ein Satz $F$ in Skolemform ist genau dann erfüllbar, wenn $F$ ein
-Herbrandmodell hat.}\pause
+Herbrand-Modell hat.}\pause
 
-\emph{Beweis:} $(\Leftarrow)$ ist klar, da Herbrandmodelle auch Modelle sind.\bigskip\pause
+\emph{Beweis:} $(\Leftarrow)$ ist klar, da Herbrand-Modelle auch Modelle sind.\bigskip\pause
 
-$(\Rightarrow)$ Sei $\Inter\models F$ ein Modell für $F$. Wir definieren eine Herbrandinterpretation $\Jnter$ indem wir festlegen:
+$(\Rightarrow)$ Sei $\Inter\models F$ ein Modell für $F$. Wir definieren eine Herbrand-Interpretation $\Jnter$ indem wir festlegen:
 \begin{itemize}
 \item $p^\Jnter=\{\tuple{t_1,\ldots,t_n}\mid\tuple{t_1^\Inter,\ldots,t_n^\Inter}\in p^\Inter\}$\\
 {\footnotesize Anm.: $t_i$ sind variablenfrei, daher ist $t_i^\Inter$ wohldefiniert}
 \end{itemize}
-Behauptung: \alert{$\Jnter$ ist ein Herbrandmodell von $F$}
+Behauptung: \alert{$\Jnter$ ist ein Herbrand-Modell von $F$}
 
 \end{frame}
 
 \begin{frame}\frametitle{Beweis (Fortsetzung)}
 
-\emph{Behauptung:} \alert{$\Jnter$ ist ein Herbrandmodell von $F$}\bigskip
+\emph{Behauptung:} \alert{$\Jnter$ ist ein Herbrand-Modell von $F$}\bigskip
 
 $F$ hat die Form $\forall x_1,\ldots, x_n.G$, wobei $G$ quantorenfrei ist.\pause
 \begin{itemize}
@@ -731,7 +731,7 @@
 
 Die prädikatenlogische Resolution ist ein Semi-Entscheidungsverfahren für die Unerfüllbarkeit logischer Formeln\bigskip
 
-Man kann Erfüllbarkeit auf Erfüllbarkeit über "`syntaktisch definierten"' Herbrandmodellen reduzieren
+Man kann Erfüllbarkeit auf Erfüllbarkeit über "`syntaktisch definierten"' Herbrand-Modellen reduzieren
 (Fortsetzung folgt)
 % \bigskip
 % 
@@ -741,7 +741,7 @@
 \bigskip
 
 \anybox{yellow}{
-Was erwartet uns als nächstes?
+Was erwartet uns als Nächstes?
 \begin{itemize}
 \item Beweis der Vollständigkeit der Resolution
 \item Logik über endlichen Modellen und ihre praktische Anwendung
diff --git a/Vorlesungen/lecture-20.tex b/Vorlesungen/lecture-20.tex
index b5f0cf5..786b788 100644
--- a/Vorlesungen/lecture-20.tex
+++ b/Vorlesungen/lecture-20.tex
@@ -36,7 +36,7 @@
 \begin{enumerate}[(1)]
 \item Bilde Klauselform
 \item Bilde systematisch Resolventen durch Resolution von Varianten bereits abgeleiteter Klauseln
-\item Wiederhole (2), bis entweder $\bot$ erzeugt wird ("`unerfüllbar"') oder keine neuen Klauseln mehr entstehen\footnote{Dieser Fall ist eher ungewöhnlich: Meist entstehen bei erfüllbaren Theorien immer mehr neue Klauseln ohne dass das Verfahren terminiert.}
+\item Wiederhole (2), bis entweder $\bot$ erzeugt wird ("`unerfüllbar"') oder keine neuen Klauseln mehr entstehen\footnote{Dieser Fall ist eher ungewöhnlich: Meist entstehen bei erfüllbaren Theorien immer mehr neue Klauseln, ohne dass das Verfahren terminiert.}
 \end{enumerate}
 
 \end{frame}
@@ -84,9 +84,9 @@
 
 \begin{frame}\frametitle{Syntax vs. Semantik}
 
-Bei Herbrandinterpretationen kann man semantische Elemente (wie sie in Zuweisungen vorkommen) durch syntaktische Elemente (wie sie in Substitutionen vorkommen) ausdrücken:\medskip
+Bei Herbrand-Interpretationen kann man semantische Elemente (wie sie in Zuweisungen vorkommen) durch syntaktische Elemente (wie sie in Substitutionen vorkommen) ausdrücken:\medskip
 
-\theobox{\emph{Lemma:} Für jede Herbrandinterpretation $\Inter$, jede Zuweisung $\Zuweisung$ für $\Inter$, jeden Term $t\in\Delta^\Inter$ und jede Formel $F$ gilt:
+\theobox{\emph{Lemma:} Für jede Herbrand-Interpretation $\Inter$, jede Zuweisung $\Zuweisung$ für $\Inter$, jeden Term $t\in\Delta^\Inter$ und jede Formel $F$ gilt:
 \[ \Inter,\Zuweisung\{x\mapsto t\} \models F \qquad \text{gdw.}\qquad \Inter,\Zuweisung \models F\{x\mapsto t\}\]}
 
 (ohne Beweis; einfach)
@@ -95,7 +95,7 @@
 {\color{devilscss}\footnotesize \emph{Anmerkung:} Man kann ein entsprechendes Resultat auch für Nicht-Herbrand-Interpretationen zeigen. Dann muss man einfach den Term auf der linken Seite durch $t^{\Inter,\Zuweisung}$ ersetzen.}\bigskip
 
 \theobox{\emph{Satz:} Ein Satz $F$ in Skolemform ist genau dann erfüllbar, wenn $F$ ein
-Herbrandmodell hat.}
+Herbrand-Modell hat.}
 
 \end{frame}
 
@@ -141,7 +141,7 @@
 \[ HE(F)\defeq\big\{ G\{x_1\mapsto t_1,\ldots,x_n\mapsto t_n\}\mid t_1,\ldots,t_n\in\Delta_F\big\}\]
 }
 
-$HE(F)$ ist also die (möglicherweise unendliche) Menge von \ghost{variablen-}\\ freien Sätzen, die in Herbrandmodellen von $F$ gelten müssten.
+$HE(F)$ ist also die (möglicherweise unendliche) Menge von \ghost{variablen-}\\ freien Sätzen, die in Herbrand-Modellen von $F$ gelten müssten.
 \pause\bigskip
 
 \redalert{Quantorenfreie Sätze = aussagenlogische Formeln:}
@@ -159,10 +159,10 @@
 
 \theobox{\emph{Satz von Gödel, Herbrand \& Skolem:} Eine Formel $F$ in Skolemform ist genau dann erfüllbar, wenn $HE(F)$ aussagenlogisch erfüllbar ist.}\pause
 
-\emph{Beweis:} Wir zeigen, dass $F=\forall x_1,\ldots,x_n.G$ genau dann ein Herbrandmodell hat, wenn $HE(F)$ aussagenlogisch erfüllbar ist:\pause
+\emph{Beweis:} Wir zeigen, dass $F=\forall x_1,\ldots,x_n.G$ genau dann ein Herbrand-Modell hat, wenn $HE(F)$ aussagenlogisch erfüllbar ist:\pause
 
 \begin{itemize}
-\item $\Inter$ ist ein Herbrandmodell von $F$\pause
+\item $\Inter$ ist ein Herbrand-Modell von $F$\pause
 \item gdw. $\Inter,\{x_1\mapsto t_1,\ldots,x_n\mapsto t_n\}\models G$ für alle $t_1,\ldots,t_n\in\Delta_F$\pause
 \item gdw. $\Inter\models G\{x_1\mapsto t_1,\ldots,x_n\mapsto t_n\}$ für alle $t_1,\ldots,t_n\in\Delta_F$ (Lemma)\pause
 \item gdw. für alle $H\in HE(F)$ gilt $\Inter\models H$\pause
@@ -178,14 +178,14 @@
 \theobox{\emph{Satz:} Eine Formel $F$ in Skolemform ist genau dann unerfüllbar, wenn
 eine endliche Teilmenge von $HE(F)$ aussagenlogisch unerfüllbar ist.}
 
-\pause\emph{Beweis:} Das Kontrapositiv des Satzes von Gödel, Herbrand \& Skolem besagt:\medskip
+\pause\emph{Beweis:} Die Kontraposition des Satzes von Gödel, Herbrand \& Skolem besagt:\medskip
 
 Eine Formel $F$ in Skolemform ist genau dann unerfüllbar, wenn $HE(F)$ aussagenlogisch unerfüllbar ist.\bigskip
 
 Der Satz folgt nun, weil jede unerfüllbare aussagenlogische Formelmenge eine endliche
 Teilmenge hat, die unerfüllbar ist: \alert{Kompaktheit der Aussagenlogik}, ohne Beweis\\[1ex]
 {\tiny
-\textcolor{devilscss}{Das Ergebnis kann aus der Vollständigkeit der Verallgemeinerung aussagenlogischer Resolution auf unendliche Modelle gefolgert werden (siehe Formale Systeme, WS 2017/2018, Vorlesung 23): wenn die leere Klausel endlich abgeleitet werden kann, dann nutzt man dazu nur endlich viele Klauseln der Eingabe; wenn die leere Klausel nicht endlich abgeleitet werden kann, dann erhält man aus der unendlichen Menge aller möglichen Ableitungen ein Modell, analog zum endlichen Fall.}
+\textcolor{devilscss}{Das Ergebnis kann aus der Vollständigkeit der Verallgemeinerung aussagenlogischer Resolution auf unendliche Modelle gefolgert werden (siehe Formale Systeme, WS 2020/2021, Vorlesung 23): wenn die leere Klausel endlich abgeleitet werden kann, dann nutzt man dazu nur endlich viele Klauseln der Eingabe; wenn die leere Klausel nicht endlich abgeleitet werden kann, dann erhält man aus der unendlichen Menge aller möglichen Ableitungen ein Modell, analog zum endlichen Fall.}
 
 }\qed
 
@@ -221,7 +221,7 @@
 \begin{itemize}
 \item Unerfüllbarkeit einer Klauselmenge zeigt sich in der Unerfüllbarkeit ihrer Herbrand-Expansion
 \item Die Unerfüllbarkeit der Herbrand-Expansion kann man mit aussagenlogischer Resolution beweisen
-\item Prädikatenlogische Resolution verallgemeinert aussagenlogische Resolution indem wir direkt mit Klauseln arbeiten, die noch Variablen enthalten
+\item Prädikatenlogische Resolution verallgemeinert aussagenlogische Resolution, indem wir direkt mit Klauseln arbeiten, die noch Variablen enthalten
 \end{itemize}\pause
 
 \emph{Frage:} Kann man alle Schlüsse, die man auf expandierten Formeln aussagenlogisch erzeugen kann, auch direkt prädikatenlogisch (mit Variablen) erhalten?
@@ -240,7 +240,7 @@
 }
 
 \color{devilscss}
-{\footnotesize ${^1}$ Die Verwendung der selben Substitution für $K'_1$ und $K'_2$ ist keine Einschränkung, da wir durch Variantenbildung sicherstellen können, dass $K_1$ und $K_2$ keine Variablen gemein haben.
+{\footnotesize ${^1}$ Die Verwendung derselben Substitution für $K'_1$ und $K'_2$ ist keine Einschränkung, da wir durch Variantenbildung sicherstellen können, dass $K_1$ und $K_2$ keine Variablen gemein haben.
 
 }
 
@@ -266,7 +266,7 @@
 Dann enthalten $R'$ und $R$ Instanzen der gleichen Literale, d.h. sie sind von der Form
 $R'=\{L_1\sigma,\ldots,L_n\sigma\}$ und $R=\{L_1\theta,\ldots,L_n\theta\}$\smallskip\pause
 
-Da $\theta$ allgemeinster Unifikator ist gibt es $\lambda$ mit $\sigma=\theta\circ\lambda$
+Da $\theta$ allgemeinster Unifikator ist, gibt es $\lambda$ mit $\sigma=\theta\circ\lambda$
 und es gilt: $R\lambda=\{L_1\theta\lambda,\ldots,L_n\theta\lambda\}=\{L_1\sigma,\ldots,L_n\sigma\}=R'$\qed
 
 
@@ -303,7 +303,7 @@
 \emph{Beweis (Vollständigkeit):} \alert{Behauptung:} Jede Klausel $K_i'$ ist Grundinstanz einer Klausel $K_i$ die in $\mathcal{K}_\ell$ vorkommt für ein $\ell\geq 0$.
 \medskip\pause
 
-Aussage klar für $K'_i\in HE(F)$: in diesem Fall ist $K'_i$ ist Grundinstanz einer Klausel $K_i$ in der Klauselform von $F$ und in $\mathcal{K}_0$\medskip\pause
+Aussage klar für $K'_i\in HE(F)$: in diesem Fall ist $K'_i$ Grundinstanz einer Klausel $K_i$ in der Klauselform von $F$ und in $\mathcal{K}_0$\medskip\pause
 
 Restlicher Beweis durch Induktion über $i$:
 \begin{itemize}
@@ -369,7 +369,7 @@
 % Auswertungsproblem auf endlichen Modellen = Anfragebeantwortung in Datenbanken
 
 \anybox{yellow}{
-Was erwartet uns als nächstes?
+Was erwartet uns als Nächstes?
 \begin{itemize}
 \item Endliche Modelle und Datenbanken
 \item Datalog
diff --git a/Vorlesungen/lecture-21.tex b/Vorlesungen/lecture-21.tex
index 5bee665..0e316c4 100644
--- a/Vorlesungen/lecture-21.tex
+++ b/Vorlesungen/lecture-21.tex
@@ -141,7 +141,7 @@
 
 \begin{frame}\frametitle{Wozu endliche Modelle}
 
-In gewisser Weise ist Schließen mit endlichen Modellen also schwerer als mit unendlichen, weil man statt logischer Konsequenz nunmehr nur Nicht-Konsequenz semi-entscheiden kann
+In gewisser Weise ist Schließen mit endlichen Modellen also schwerer als mit unendlichen, weil man statt logischer Konsequenz nunmehr nur Nichtkonsequenz semi-entscheiden kann
 \bigskip
 
 Trotzdem sind endliche Interpretationen in der Informatik praktisch relevant:\medskip
@@ -214,7 +214,7 @@
 \begin{frame}\frametitle{Formeln = Anfragen}
 
 Benannt oder nicht -- sofern die Parameter eine definierte Reihenfolge haben,
-kann man sie mit normalen prädikatenlogischen Atomen addressieren.\medskip
+kann man sie mit normalen prädikatenlogischen Atomen adressieren.\medskip
 
 \examplebox{\emph{Beispiel:} Die Formel \[Q=\exists z_{\text{Linie}}.(\textsf{verbindung}(x_\text{Von},x_\text{Zu}, z_{\text{Linie}})\wedge \textsf{linien}(z_{\text{Linie}},x_{\text{Typ}}))\]
 hat drei freie Variablen. Für eine gegebene Datenbankinstanz (endliche Interpretation) $\Inter$ bedeutet $\Inter,\{x_\text{Von}\mapsto\delta_1,x_\text{Zu}\mapsto\delta_2,x_\text{Typ}\mapsto\delta_3\}\models Q$, dass es in der Datenbank eine Verbindung von $\delta_1$ nach $\delta_2$ vom Typ $\delta_3$ gibt.
@@ -224,7 +224,7 @@
 \begin{center}
 \large
 \redalert{Formeln (ev. mit freien Variablen) = Datenbankanfragen}\\[1ex]
-\redalert{Erfüllende Zuweisungen = Anfrage-Ergebnisse}\\
+\redalert{Erfüllende Zuweisungen = Anfrageergebnisse}\\
 \end{center}
 \end{frame}
 
@@ -232,7 +232,7 @@
 
 \alert{Relationale Datenbankinstanzen = Endliche Interpretationen}
 \begin{itemize}
-\item Tabellen(namen) entsprechen Prädikatssymbolen
+\item Tabellen(namen) entsprechen Prädikatensymbolen
 \item Kleinere syntaktische Unterschiede (benannte vs. geordnete Parameter)
 \end{itemize}
 
@@ -249,7 +249,7 @@
 
 \begin{frame}\frametitle{Prädikatenlogik $\approx$ SQL}
 
-\redalert{Was ist eine Datenbank-Anfrage?}
+\redalert{Was ist eine Datenbankanfrage?}
 \begin{itemize}
 \item Syntax: Eine Anfrage $Q$ ist ein Wort aus einer Anfragesprache
 \item Semantik: Jede Anfrage $Q$ definiert eine Anfragefunktion $f_Q$, \ghost{die}\\ für jede Datenbankinstanz $\Inter$ eine Ergebnisrelation $f_Q(\Inter)$ liefert
@@ -330,7 +330,7 @@
 \emph{Anmerkung:} Wenn Konstanten $c$ in der Anfrage vorkommen, dann nimmt man
 in der Regel an, dass $c^\Inter=c$ ist.\medskip
 
-\emph{Anmerkung 2:} In der Praxis stimmt das nicht ganz. Insbesondere bei Verwendung von Datentypen haben DB-Systeme normalerweise eingebaute Interpretationsfunktionen. Zum Beispiel würden die Konstanten $\Scodelit{\quoted{42}}$ und $\Scodelit{\quoted{+42}}$ die selbe Ganzzahl bezeichnen.
+\emph{Anmerkung 2:} In der Praxis stimmt das nicht ganz. Insbesondere bei Verwendung von Datentypen haben DB-Systeme normalerweise eingebaute Interpretationsfunktionen. Zum Beispiel würden die Konstanten $\Scodelit{\quoted{42}}$ und $\Scodelit{\quoted{+42}}$ dieselbe Ganzzahl bezeichnen.
 
 \end{frame}
 
@@ -508,7 +508,7 @@
 % \]\pause
 % 
 
-\alert{``Haltestellen, die von Helmholtzstr. aus mit einem Kurzstreckentticket erreichbar sind:''}
+\alert{``Haltestellen, die von Helmholtzstr. aus mit einem Kurzstreckenticket erreichbar sind:''}
 \[
 	Q_0[x]\vee Q_1[x]\vee Q_2[x]\vee Q_3[x]\vee Q_4[x]
 \]
@@ -553,7 +553,7 @@
 
 \redalert{Wie kann man solche Anfragen logisch ausdrücken?}\bigskip\pause
 
-\emph{Idee:} Um beliebig weit zu schauen muss man Rekursion einführen.\bigskip
+\emph{Idee:} Um beliebig weit zu schauen, muss man Rekursion einführen.\bigskip
 
 \examplebox{\emph{Beispiel:} Eine Haltestelle ist von Helmholtzstr. aus erreichbar, wenn
 \begin{enumerate}[(1)]
@@ -568,7 +568,7 @@
 Beschränkt man Prädikatenlogik auf endliche Modelle, so gibt es kein vollständiges und korrektes Verfahren zum logischen Schließen -- dafür wird Erfüllbarkeit semi-entscheidbar\bigskip
 
 Auswertungsproblem auf endlichen Modellen = Anfragebeantwortung in Datenbanken\\
-(\PSpace-vollständig, aber sub-polynomiell bzgl. Datenbankgröße)\bigskip
+(\PSpace-vollständig, aber subpolynomiell bzgl. Datenbankgröße)\bigskip
 
 Prädikatenlogik hat Grenzen: 
 \begin{itemize}
@@ -577,7 +577,7 @@
 \end{itemize}\bigskip
 
 \anybox{yellow}{
-Was erwartet uns als nächstes?
+Was erwartet uns als Nächstes?
 \begin{itemize}
 \item Datalog und Logik höherer Ordnung
 \item Gödel
diff --git a/Vorlesungen/lecture-22.tex b/Vorlesungen/lecture-22.tex
index 426dc02..43eeab6 100644
--- a/Vorlesungen/lecture-22.tex
+++ b/Vorlesungen/lecture-22.tex
@@ -78,7 +78,7 @@
 
 \redalert{Wie kann man solche Anfragen logisch ausdrücken?}\bigskip\pause
 
-\emph{Idee:} Um beliebig weit zu schauen muss man Rekursion einführen.\bigskip
+\emph{Idee:} Um beliebig weit zu schauen, muss man Rekursion einführen.\bigskip
 
 \examplebox{\emph{Beispiel:} Eine Haltestelle ist von Helmholtzstr. aus erreichbar, wenn
 \begin{enumerate}[(1)]
@@ -306,7 +306,7 @@
 $\leadsto$ Datalog-Programme sind syntaktische Varianten skolemisierter Klauseln\\
 $\leadsto$ Für die Inferenz von Fakten kann man sich auf Herbrand-Modelle beschränken\bigskip\pause
 
-\emph{Beobachtung 2:} Die Berechnung eines Fakts $H\theta$ durch Anwendung einer solchen Regel entspricht einer (Hyper)-Resolution der Klausel $H\vee\neg B_1\vee\ldots\vee\neg B_n$ mit den Fakten $B_1\theta$, \ldots, $B_n\theta$, wobei $\theta$ der allgemeinste Unifikator ist.\medskip\pause
+\emph{Beobachtung 2:} Die Berechnung eines Fakts $H\theta$ durch Anwendung einer solchen Regel entspricht einer (Hyper-)Resolution der Klausel $H\vee\neg B_1\vee\ldots\vee\neg B_n$ mit den Fakten $B_1\theta$, \ldots, $B_n\theta$, wobei $\theta$ der allgemeinste Unifikator ist.\medskip\pause
 
 $\leadsto$ Abgeleitete Fakten sind logische Konsequenzen (Korrektheit)\bigskip\pause
 
@@ -370,12 +370,12 @@
 \begin{itemize}
 \item Für jedes Nichtterminal $\Snterm{A}\in V$, sei $A$ ein zweistelliges Prädikat
 \item Für jedes Terminal $\Sterm{b}\in \Sigma$, sei $b$ ein zweistelliges Prädikat
-\item Für jede Produktionsregel $\Snterm{A}\to v$ mit $v=v_1\ldots v_n\in(\Sigma\cup V)^*$ sei $A(x_0,x_n)\leftarrow v_1(x_0,x_1)\wedge\ldots\wedge v_n(x_{n-1},x_n)$ eine Datalogregel
+\item Für jede Produktionsregel $\Snterm{A}\to v$ mit $v=v_1\ldots v_n\in(\Sigma\cup V)^*$ sei $A(x_0,x_n)\leftarrow v_1(x_0,x_1)\wedge\ldots\wedge v_n(x_{n-1},x_n)$ eine Datalog-Regel
 \item Die Menge aller entsprechenden Regel bezeichnen wir mit $P_G$
 \end{itemize}
 Wir betrachten Datenbanken, die nur Prädikate aus $\Sigma$ enthalten\bigskip\pause
 
-Dann gilt: $P_G\models S(a,b)$ genau dann wenn es zwischen $a$ und $b$ einen
+Dann gilt: $P_G\models S(a,b)$ genau dann, wenn es zwischen $a$ und $b$ einen
 Pfad $w_1(a,c_1),w_2(c_1,c_2),\ldots,w_\ell(c_{\ell-1},b)$ gibt, wobei $\Sterm{w_1}\cdots \Sterm{w_\ell}\in\Slang{L}(G)$
 
 % briefly discuss use of Datalog derivation trees in pumping-lemma like constructions ...
@@ -388,7 +388,7 @@
 \begin{itemize}
 \item Intuitive Darstellung der Ableitungsschritte
 \item Umformungsoperationen auf Bäumen erlauben die Erzeugung neuer Ableitungen $\leadsto$ hilfreiche Beweistechnik
-\examplebox{\emph{Beispiel:} Wir haben Ableitungsbäume kontextfreier Grammatiken verwendet um das Pumpinglemma für kontextfrei Sprachen zu zeigen. Damit konnte man zeigen, dass manche Sprachen nicht kontextfrei sind.\medskip
+\examplebox{\emph{Beispiel:} Wir haben Ableitungsbäume kontextfreier Grammatiken verwendet, um das Pumpinglemma für kontextfreie Sprachen zu zeigen. Damit konnte man zeigen, dass manche Sprachen nicht kontextfrei sind.\medskip
 
 Analoge Techniken kann man auch für Datalog anwenden, zum Beispiel um zu zeigen, dass kein Datalog-Programm Paare von Elementen finden kann, zwischen denen es einen Pfad aus einem binären Prädikat $p$ gibt, dessen Länge eine Primzahl ist.}
 \item Zur Analyse von Datalogprogrammen werden oft (allgemeinere) endliche Automaten verwendet, welche auf Ableitungsbäumen arbeiten (Verallgemeinerung regulärer Sprachen von Wörtern auf Bäumen).
@@ -403,7 +403,7 @@
 
 \emph{Worst Case?}
 \begin{itemize}
-\item Sei $p$ die Anzahl der Prädikatensmbole, $a$ deren maximale Arität, $x$ die maximale Zahl an Variablen pro Regel und $n$ die Zahl der Konstanten
+\item Sei $p$ die Anzahl der Prädikatensymbole, $a$ deren maximale Arität, $x$ die maximale Zahl an Variablen pro Regel und $n$ die Zahl der Konstanten
 \item Dann gibt es insgesamt $\leq p\cdot n^a$ variablenfreie Fakten, die abgeleitet werden könnten
 \item Für eine Regel gibt es maximal $n^x$ Substitutionen, die bei der Ableitung eine Rolle spielen könnten
 \end{itemize}\pause
@@ -464,8 +464,8 @@
 
 \begin{frame}\frametitle{Logik höherer Ordnung: Syntax und Semantik}
 
-\emph{Syntax:} Wie in Prädikatenlogik, aber mit quantifizierten Prädikaten-Variablen.\\
-\textcolor{devilscss}{(Die Stelligkeit einer Prädikaten-Variablen muss jeweils klar festgelegt werden)}\medskip
+\emph{Syntax:} Wie in Prädikatenlogik, aber mit quantifizierten Prädikatenvariablen.\\
+\textcolor{devilscss}{(Die Stelligkeit einer Prädikatenvariablen muss jeweils klar festgelegt werden)}\medskip
 
 \examplebox{\emph{Beispiel:} ``Für jede Menge $M$ gilt: Enthält $M$ die Zahl $0$ und mit jeder natürlichen Zahl $n$ auch stets deren Nachfolger $s(n)$, so enthält $M$ alle natürlichen Zahlen.''
 %
@@ -474,7 +474,7 @@
 Wir verwenden hier ein Funktionssymbol $s$ zur Darstellung von Nachfolgern.
 }\bigskip\pause
 
-\emph{Semantik:} wie erwartet (gleiche Interpretationen wie in erster Stufe; Interpretation von Prädikaten-Variablen mit Zuweisungen wie bei Objektvariablen in erster Stufe)\medskip
+\emph{Semantik:} wie erwartet (gleiche Interpretationen wie in erster Stufe; Interpretation von Prädikatenvariablen mit Zuweisungen wie bei Objektvariablen in erster Stufe)\medskip
 
 \textcolor{devilscss}{(Intuition: zweite Stufe/erste Stufe = QBF/Aussagenlogik)}
 
@@ -505,8 +505,8 @@
  &\hspace{-5mm}(\forall x,y,z.\text{Erreichbar}(x)\wedge \text{verbindung}(x,y,z)\to \text{Erreichbar}(y)) )\to \text{Erreichbar}(v)
 \Big)
 \end{align*}
-Die Formel hat eine freie Variable $v$ und stellt $\text{Erreichbar}$ als Prädikaten-Variable dar.
-Ein Fakt $\text{Erreichbar}(a)$ folgt aus dem ursprünglichen Programm über einer Datenbank $\Inter$ genau dann wenn $\Inter$ die Formel mit Variablenbelegung $v\mapsto a$ erfüllt.
+Die Formel hat eine freie Variable $v$ und stellt $\text{Erreichbar}$ als Prädikatenvariable dar.
+Ein Fakt $\text{Erreichbar}(a)$ folgt aus dem ursprünglichen Programm über einer Datenbank $\Inter$ genau dann, wenn $\Inter$ die Formel mit Variablenbelegung $v\mapsto a$ erfüllt.
 }
 
 \end{frame}
@@ -540,7 +540,7 @@
 \end{itemize}\bigskip
 
 \anybox{yellow}{
-Was erwartet uns als nächstes?
+Was erwartet uns als Nächstes?
 \begin{itemize}
 \item Gödel
 \item Konsultation, Probeklausur und Prüfung
diff --git a/Vorlesungen/lecture-23.tex b/Vorlesungen/lecture-23.tex
index ef77d61..979816a 100644
--- a/Vorlesungen/lecture-23.tex
+++ b/Vorlesungen/lecture-23.tex
@@ -157,7 +157,7 @@
 \begin{itemize}
 \item Konstante $\Sterm{0}$
 \item Funktionssymbole $s$ (unär, "`Nachfolger"'), $+$ und $\times$ (binär, infix)
-\item Prädikatssymbol $\approx$ (binär, infix)
+\item Prädikatensymbol $\approx$ (binär, infix)
 \end{itemize}
 
 Darstellung natürlicher Zahlen als Nachfolger von 0:\\[0.5ex]
@@ -270,12 +270,12 @@
 
 Es gibt Mengen (Sprachen), die nicht semi-entscheidbar sind
 \begin{itemize}
-\item Zum Beispiel das Nicht-Halteproblem von Turingmaschinen
+\item Zum Beispiel das Nichthalteproblem von Turingmaschinen
 \end{itemize}
 \bigskip\pause
 
 \alert{
-$\leadsto$ Falls man Instanzen des Wortproblems einer nicht-semientscheidbaren Sprache auf die Wahrheit arithmetischer Sätze reduzieren könnte, dann würde daraus schon Unvollständigkeit folgen}
+$\leadsto$ Falls man Instanzen des Wortproblems einer nicht-semi-entscheidbaren Sprache auf die Wahrheit arithmetischer Sätze reduzieren könnte, dann würde daraus schon Unvollständigkeit folgen}
 
 \end{frame}
 
@@ -357,10 +357,10 @@
 \item Wäre es entscheidbar, dann könnte man jede diophantische Menge entscheiden (Kontrollfrage: Wie?)
 \item Wir wissen aber bereits, dass es rekursiv aufzählbare Mengen natürlicher Zahlen gibt, die nicht entscheidbar sind
 \end{itemize}\pause
-\item \alert{Nicht-Lösbarkeit diophantischer Gleichungen ist nicht semi-entscheidbar:}
+\item \alert{Nichtlösbarkeit diophantischer Gleichungen ist nicht semi-entscheidbar:}
 \begin{itemize}
 \item Lösbarkeit ist bereits semi-entscheidbar
-\item Wenn Nicht-Lösbarkeit auch semi-entscheidbar wäre, dann wäre beides entscheidbar
+\item Wenn Nichtlösbarkeit auch semi-entscheidbar wäre, dann wäre beides entscheidbar
 \end{itemize}
 \end{itemize}
 
diff --git a/Vorlesungen/lecture-24.tex b/Vorlesungen/lecture-24.tex
index c7f7ed9..6bcfad0 100644
--- a/Vorlesungen/lecture-24.tex
+++ b/Vorlesungen/lecture-24.tex
@@ -406,7 +406,7 @@
 \emph{Komplexität:} NP, PSpace, Many-One-Reduktionen, Übersicht weiterer wichtiger Klassen
 \bigskip
 
-\emph{Logik:} Aussagenlogik (SAT), QBF, Prädikatenlogik, Resolution (mit vielen Teilschritten), Herbrandmodelle, Datalog
+\emph{Logik:} Aussagenlogik (SAT), QBF, Prädikatenlogik, Resolution (mit vielen Teilschritten), Herbrand-Modelle, Datalog
 \bigskip
 
 \emph{Bonusmaterial:} Gödel, Metamathematik, SQL, Geschichte und Geschichten