--- a/notes/tex/logic.tex	Mon Jan 06 18:09:07 2014 +0100
+++ b/notes/tex/logic.tex	Wed Jan 08 14:26:02 2014 +0100
@@ -1,7 +1,6 @@
 \defineUnit{aussagenlogiksyntax}{%
 \begin{frame}[c]
     \frametitle{Syntax der Aussagenlogik}
-    \setbeamercovered{dynamic}
 
     \begin{definition}[Syntax der Aussagenlogik]
         Aussagenlogische \structure{Formeln} bestehen aus Konstanten, Variablen und Operatoren. Die Menge \structure{$\mathcal{F}$} aller Formeln ist induktiv definiert.
@@ -24,7 +23,6 @@
 
 \begin{frame}
     \frametitle{Operatorenbindung}
-    \setbeamercovered{dynamic}
 
     \begin{definition}[Bindungsregeln]
         Die \structure{Bindungsstärke} der Operatoren in absteigender Reihenfolge ist
@@ -46,7 +44,6 @@
 
 \begin{frame}
     \frametitle{Syntaxbaum}
-    \setbeamercovered{dynamic}
 
     \begin{block}{Syntaxbaum}
         \structure{Syntaxbäume} visualisieren in welcher Reihenfolge die Regeln zur induktiven Definition angewandt werden müssen, um eine Formel zu erzeugen.
@@ -99,7 +96,6 @@
 \defineUnit{aussagenlogiksemantik}{%
 \begin{frame}
     \frametitle{Belegung}
-    \setbeamercovered{dynamic}
 
     \begin{definition}[Belegung]
         Eine passende \structure{Belegung} $\beta$ zu einer Formel $F$ ordnet jeder Variable in $V$ einen Wahrheitswert aus $\left\{ 0, 1 \right\}$ zu. Es ist
@@ -122,7 +118,6 @@
 
 \begin{frame}
     \frametitle{Semantik der Aussagenlogik}
-    \setbeamercovered{dynamic}
 
     \begin{definition}[Semantik einer Formel]
         Die \structure{Semantik} $[F]$ einer aussagenlogischen Formel $F$ ist eine Funktion, die jeder passenden Belegung $\beta$ einen Wahrheitswert zuordnet.\\
@@ -145,7 +140,6 @@
 
 \begin{frame}
     \frametitle{Wahrheitstabelle}
-    \setbeamercovered{dynamic}
 
     \begin{block}{Wahrheitstabelle}
         Die Semantik einer Formel kann mit Hilfe einer \structure{Wahrheitstabelle} visualisiert werden. Die Tabelle gibt den Wahrheitswert der Formel für jede mögliche Belegung an.
@@ -170,7 +164,6 @@
 
 \begin{frame}
     \frametitle{Äquivalente Formeln}
-    \setbeamercovered{dynamic}
 
     \begin{definition}[Äquivalente Formeln]
         Man nennt zwei Formeln \structure{äquivalent}, wenn sie dieselbe Semantik besitzen.\\
@@ -195,7 +188,6 @@
 
 \begin{frame}
     \frametitle{Eigenschaften von Formeln}
-    \setbeamercovered{dynamic}
 
     \begin{block}{Eigenschaften aussagenlogischer Formeln}
         Sei $F$ eine aussagenlogische Formel mit Variablen $V$ und der Menge der passenden Belegungen $\mathcal{B}$. Man nennt F
@@ -222,7 +214,6 @@
 
     \begin{frame}
         \frametitle{Äquivalenzregeln}
-        \setbeamercovered{dynamic}
 
         \begin{description}[Triviale Kontradiktion\quad]
             \item[Identität] $\F \wedge \true \equiv \F \spc \F \vee \false \equiv \F$
@@ -248,7 +239,6 @@
 
     %\begin{frame}
         %\frametitle{Äquivalenzregeln}
-        %\setbeamercovered{dynamic}
 
         %\vspace{-2em}
         %\begin{align}
@@ -278,7 +268,6 @@
 \defineUnit{aussagenlogiknormalformen}{%
 \begin{frame}[c]
     \frametitle{Literale und Klauseln}
-    \setbeamercovered{dynamic}
 
     \begin{definition}[Literal]
         Ein \structure{Literal} ist eine Variable $v \in V$ oder die Negation $\neg v$ einer Variable.
@@ -304,7 +293,6 @@
     \newcommand{\klausel}[2]{\underbracket{(##2)}_{\text{##1-Klausel}}}
     \begin{frame}
         \frametitle{DNF}
-        \setbeamercovered{dynamic}
 
         \begin{definition}[Disjunktive Normalform]
             Eine \structure{DNF-Klausel} ist eine Konjunktion von Literalen $L_i$.\\
@@ -323,7 +311,6 @@
 
     \begin{frame}
         \frametitle{KNF}
-        \setbeamercovered{dynamic}
 
         \begin{definition}[Konjunktive Normalform]
             Eine \structure{KNF-Klausel} ist eine Disjunktion von Literalen $L_i$.\\
@@ -343,7 +330,6 @@
 
 \begin{frame}
     \frametitle{Konstruktion der NF}
-    \setbeamercovered{dynamic}
 
     \begin{itemize}
         \item \structure{Jede} nicht-triviale Formel ist in DNF und KNF umwandelbar
@@ -377,7 +363,6 @@
     \newcommand{\klausel}[4]{(##2 a ##1 ##3 b ##1 ##4 c)}
     \begin{frame}
         \frametitle{Konstruktion der NF}
-        \setbeamercovered{dynamic}
 
         \begin{example}[]
             Gegeben eine Formel $F$ mit folgender Semantik
@@ -405,7 +390,6 @@
 
     \begin{frame}
         \frametitle{Mengendarstellung der KNF}
-        \setbeamercovered{dynamic}
 
         \begin{block}{Mengendarstellung der KNF}
             Eine Formel $F = \bigwedge \bigvee L_i$ in \structure{KNF} kann in einer \structure{Mengendarstellung} repräsentiert werden.
@@ -428,7 +412,6 @@
 \defineUnit{DPLL}{%
 \begin{frame}
     \frametitle{KNF aus Syntaxbaum}
-    \setbeamercovered{dynamic}
 
     \begin{block}{Idee}
         Erzeuge die KNF aus dem Syntaxbaum
@@ -485,7 +468,6 @@
 
 \begin{frame}
     \frametitle{DPLL}
-    \setbeamercovered{dynamic}
 
     \begin{definition}[DPLL-Belegung]
         Sei $F$ eine Formel in KNF und $p$ eine Variable von $F$.\\
@@ -514,7 +496,6 @@
 \defineUnit{resolution}{%
 \begin{frame}
     \frametitle{Resolution}
-    \setbeamercovered{dynamic}
 
     \begin{definition}[Resolvent]
         Seien $K_1$, $K_2$ und $R$ Klauseln in Mengendarstellung. Dann heißt $R$ \structure{Resolvent} von $K_1$ und $K_2$ wenn $L \in K_1$, $\neg L \in K_2$ und
@@ -543,7 +524,6 @@
 \defineUnit{kalkuele}{%
 \begin{frame}
     \frametitle{Kalküle}
-    \setbeamercovered{dynamic}
 
     \begin{definition}[Kalkül]
         Ein \structure{Logikkalkül} stellt \structure{Inferenzregeln} bereit, mit denen Formeln \alert{syntaktisch} umgeformt werden können.
@@ -562,7 +542,6 @@
 
 \begin{frame}
     \frametitle{Eigenschaften von Kalkülen}
-    \setbeamercovered{dynamic}
 
     \begin{block}{Eigenschaften von Kalkülen}
         \begin{description}[\quad vollständig (complete)]
@@ -610,7 +589,6 @@
 
     \begin{frame}
         \frametitle{Natürliches Schließen}
-        \setbeamercovered{dynamic}
 
         \tabulinesep=4pt
         \begin{tabu} to \textwidth {X[c,m,.5]|[1pt]X[c,b,5]X[c,b,5]}
@@ -688,7 +666,6 @@
 
     \begin{frame}
         \frametitle{Natürliches Schließen}
-        \setbeamercovered{dynamic}
 
         \tabulinesep=4pt
         \begin{tabu} to \textwidth {X[c,m,.5]|[1pt]X[c,b,5]X[c,b,5]}
@@ -753,7 +730,6 @@
     \newcommand{\logic}{\mathcal{L}}
     \begin{frame}[c]
         \frametitle{Syntax der Prädikatenlogik}
-        \setbeamercovered{dynamic}
 
         \begin{definition}[Term]
             Die Menge $\terms$ aller \structure{Terme} ist induktiv definiert.
@@ -775,7 +751,6 @@
 
     \begin{frame}[c]
         \frametitle{Syntax der Prädikatenlogik}
-        \setbeamercovered{dynamic}
 
         \begin{definition}[Syntax der Prädikatenlogik]
             Die Menge \structure{$\logic$} aller \structure{prädikatenlogischen Formeln} ist induktiv definiert.
@@ -806,7 +781,6 @@
 
     \begin{frame}
         \frametitle{Operatorenbindung}
-        \setbeamercovered{dynamic}
 
         \begin{definition}[Bindungsregeln]
             Die \structure{Bindungsstärke} der Operatoren in absteigender Reihenfolge ist
@@ -829,7 +803,6 @@
 \defineUnit{praedikatenlogikstruktur}{%
 \begin{frame}[c]
     \frametitle{Struktur}
-    \setbeamercovered{dynamic}
 
     \begin{definition}[Struktur]
         Eine passende \structure{Struktur} $S = \left( U_s, I_s \right)$ zu einer Formel $F$ besteht aus einem \structure{Universum} $U_s$ und einer \structure{Interpretation} $I_s$.
@@ -881,7 +854,6 @@
 
     \begin{frame}
         \frametitle{Natürliches Schließen}
-        \setbeamercovered{dynamic}
 
         \begin{definition}[Ersetzung]
             Sei $\G$ eine Formel und $a$ eine Konstante.\\
@@ -929,7 +901,6 @@
 \defineUnit{induktion}{%
 \begin{frame}
     \frametitle{Vollständige Induktion}
-    \setbeamercovered{dynamic}
 
     \begin{block}{Vollständige Induktion}
         Die \structure{vollständige Induktion} ist eine Beweistechnik, um zu zeigen, dass alle natürlichen Zahlen ein Prädikat $P$ erfüllen.
@@ -961,7 +932,6 @@
 \defineUnit{wohlfundierteinduktion}{%
 \begin{frame}
     \frametitle{Wohlfundierte Relation}
-    \setbeamercovered{dynamic}
 
     \begin{definition}[Wohlfundierte Relation]
         Eine Relation $\prec \subseteq A \times A$ heißt \structure{wohlfundiert}, wenn keine \alert{unendlichen Folgen} von Elementen $a_1, a_2, a_3, \dots \in A$ existieren, sodass
@@ -985,7 +955,6 @@
 
 \begin{frame}
     \frametitle{Wohlfundierte Induktion}
-    \setbeamercovered{dynamic}
 
     \begin{block}{Wohlfundierte Induktion}
         Die \structure{wohlfundierte Induktion} verallgemeinert die vollständige Induktion.\\